Skip to content

doc(abstracts): name the allowlisted modules in three abstracts #1926

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 31, 2026
Merged

doc(abstracts): name the allowlisted modules in three abstracts #1926

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 11 additions & 2 deletions abstracts/ComplexityAbstracts/CryptographyAbstract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
12 changes: 10 additions & 2 deletions abstracts/ComplexityAbstracts/ShamirAbstract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
14 changes: 11 additions & 3 deletions abstracts/ComplexityAbstracts/TodaAbstract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading