From 72843f70a5a54c1ed42b608bfb8ff2a48dfd1a92 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:57:24 -0400 Subject: [PATCH] doc(abstracts): name the allowlisted modules in three abstracts The Shamir, Toda and cryptography abstracts said the audit permits "the listed" foundational program and machine modules. The rendered PDFs drop the `#check_abstract ... allowing [...]` command, so a reader never saw that list. The Shamir abstract also said "seven", but #732 added `Languages.Probabilistic.Sum` and its allowlist now has eight library modules. Name the eight modules in each docstring with a one-line meaning, as the GSW FHE abstract already does. This makes abstracts/README.md's claim that each abstract names its allowlisted modules true. Statements, allowlists and audits are unchanged. Found by auditor-claude-e6cf7b0d-11 (misformalization audit, round 11). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../ComplexityAbstracts/CryptographyAbstract.lean | 13 +++++++++++-- abstracts/ComplexityAbstracts/ShamirAbstract.lean | 12 ++++++++++-- abstracts/ComplexityAbstracts/TodaAbstract.lean | 14 +++++++++++--- 3 files changed, 32 insertions(+), 7 deletions(-) diff --git a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean index 190bc1d12..55285f463 100644 --- a/abstracts/ComplexityAbstracts/CryptographyAbstract.lean +++ b/abstracts/ComplexityAbstracts/CryptographyAbstract.lean @@ -25,8 +25,17 @@ finite-control machines with strict polynomial bounds and independent fair coins conventions, `Randomized.StrictPPT`, `Randomized.Negligible` and `Randomized.Indistinguishable`, are the shared foundations displayed in the appendix. The definitions and theorem statements below specify the claim; Lean checks their proofs through -`CryptographyBridge`. The audit allows only the listed foundational program, interpretation and -machine modules across the implementation boundary, without importing a security definition. +`CryptographyBridge`. Besides the shared foundations, the audit allows only the following eight +foundational program, interpretation and machine modules across the implementation boundary, +without importing a security definition: +* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels + have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as + a typed program), `Probabilistic` (one fresh fair coin per live instruction) and + `Probabilistic.Oracle` (fair-coin runs with external oracle calls); +* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only + randomness is uniform choice from a finite range), `Oracle` (private coins beside external + calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful + randomized oracle). ## References diff --git a/abstracts/ComplexityAbstracts/ShamirAbstract.lean b/abstracts/ComplexityAbstracts/ShamirAbstract.lean index 91a0f288f..53f2caf7d 100644 --- a/abstracts/ComplexityAbstracts/ShamirAbstract.lean +++ b/abstracts/ComplexityAbstracts/ShamirAbstract.lean @@ -24,8 +24,16 @@ bounds and correctness apply to encoded instances. The explicit foundational mod distinguishes finite-uniform requests in program syntax from their efficient fair-coin realization. The definitions and theorem statement below specify the claim. Lean checks the bridge, and the -audit permits only the seven listed foundational program and machine modules, with no -complexity-class or headline-result allowance. +audit permits only the following eight foundational program and machine modules, with no +complexity-class or headline-result allowance: +* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels + have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as + a typed program), `Probabilistic` (one fresh fair coin per live instruction) and + `Probabilistic.Oracle` (fair-coin runs with external oracle calls); +* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only + randomness is uniform choice from a finite range), `Oracle` (private coins beside external + calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful + randomized oracle). ## References diff --git a/abstracts/ComplexityAbstracts/TodaAbstract.lean b/abstracts/ComplexityAbstracts/TodaAbstract.lean index 21c5570ca..d57d93675 100644 --- a/abstracts/ComplexityAbstracts/TodaAbstract.lean +++ b/abstracts/ComplexityAbstracts/TodaAbstract.lean @@ -27,9 +27,17 @@ extension of valid bit answers to words outside the query encoding's image. The is deterministic. Its resource bound is expressed by exact realization on a clocked fair-coin machine; the same interaction interface also supports randomized programs. -The definitions and theorem statement below specify the claim. Lean checks the bridge, and the -audit permits only the listed foundational program and machine modules, with no complexity-class -or Toda-theorem allowance. +The definitions and theorem statement below specify the claim. Lean checks the bridge, and +besides the shared foundations the audit permits only the following eight foundational program and +machine modules, with no complexity-class or Toda-theorem allowance: +* under `Computability.Machines.Turing.MultiTape`: `Machine` (machines whose oracle channels + have a write-only query buffer and a read-only reply tape), `Machine.Program` (a clocked run as + a typed program), `Probabilistic` (one fresh fair coin per live instruction) and + `Probabilistic.Oracle` (fair-coin runs with external oracle calls); +* under `Languages.Probabilistic`: `Basic` (terminating programs with typed calls, whose only + randomness is uniform choice from a finite range), `Oracle` (private coins beside external + calls), `Sum` (sums of oracle interfaces) and `Oracle.Interaction` (runs against a stateful + randomized oracle). ## References