Repository navigation
Systems: probabilistic automata, attaching programs to them, memoryless systems - #22
Merged
Merged
Conversation
MarcIlunga
force-pushed
the
memoryless-systems
branch
from
October 6, 2026 11:06
3255005 to
d95b24f
Compare
5 tasks
MarcIlunga
force-pushed
the
memoryless-probability
branch
from
October 13, 2026 09:20
9036503 to
8846092
Compare
MarcIlunga
force-pushed
the
memoryless-systems
branch
2 times, most recently
from
October 13, 2026 11:07
1bd07a1 to
d66856f
Compare
…ss systems Random systems (RandomSystems): - `ProbStep`, its outcome, transition and state laws (`belief`), and `RandomSystem.ofProbAutomaton`, which replies at the queried port. - Simulations: `ProbStep.SimulatesAt`, `belief_simulation` and `RandomSystem.ofProbAutomaton_eq_of_simulation`. - Deterministic automata as point steps (`ProbStep.ofDeterministic`, `RandomSystem.ofProbAutomaton_ofDeterministic_apply`). - Programs against probabilistic steps (`Program.probInvoke`, `Program.probCombine`), which respect simulations (`RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation`). - The attachment theorem (#11): `PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton`, attaching the converter of a bounded program to a probabilistic automaton is the program run against its step, with the hypotheses of the deterministic case. Proof: the automaton is a random automaton (Maurer 2002, Def. 2) reading a table of pre-sampled draws (`ofProbAutomaton_eq_drawStep`, two simulations through the step that records its draws); the deterministic inlining theorem applies to each table; the program respects both simulations. - Memoryless systems (CR18 Def. 3.1, §3.6.1): `RandomSystem.memoryless`, its chain rule and converse, `portLaw`, `ProbStep.Memoryless`, `ofProbAutomaton_eq_memoryless`, `Program.replyLaw`, `memoryless_probCombine`, and the composition law `PDCBehavior.attach_ofDDC_ofProgramOn_memoryless`. Typed systems (ConstructiveCryptography.Memoryless): sources are memoryless, memoryless resources side by side are memoryless, and the composition law for `ofProgram`, `ofPreservingProgram` and `ofPreservingProgram ≫ rightContext`, as equalities of random systems. Commons: `MemorylessSource` and `MemorylessSource.memoryless_eq`. Examples: PRG length extension, each hop one rewrite with these laws. Tests: axiom audits of the new endpoints. THEORY.md and README updated. Part of #14. Closes #11. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…gths The typed corollaries are about systems on interfaces, so their docs and THEORY.md say "memoryless systems" instead of "memoryless resources"; the source in THEORY.md is a memoryless source (CR18, Definition 3.1), since the sources of Maurer 2002, Definition 1 may have memory. Steps of the new modules are lemmas (#18); root docs, the Examples doc and two Tests lines are wrapped to 100 characters; the Examples doc names the Games class and conditional equivalence instead of the former solver class. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
GitHub does not render a formula inside link text, so the reply law ν of a memoryless step now follows its link. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9
Memoryless systems side by side are memoryless at the systems level: `RandomSystem.parallel_memoryless` states it for the parallel composition of two random systems, with `RandomSystem.twoLaw`, the reply laws on the alphabets of that composition. The typed `Interface.parallel_eq_memoryless` now follows from it by relabelling the ports of the tensor, instead of redoing the chain rule in the CC file. THEORY.md §1.2 states the systems law. ProbAutomaton.lean, ProbProgramAttachment.lean, System/Memoryless.lean and ConstructiveCryptography/Memoryless.lean no longer open `Classical`: the definitions and statements that decide a domain admission or an equality are under `open scoped Classical in`, and the proofs that decide one start with `classical`. A `show` becomes `change`. The README table and the module doc of ConstructiveCryptography.lean say "memoryless systems", as the rest of the PR does. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9
Comments for every proof of the probabilistic automata, the programs run against them, the table of draws, memoryless systems, their typed forms and PRG length extension: numbered plans for the long proofs (the simulations, the table of draws, the attachment theorems, the two typed laws), drawings of the systems, simulation squares and equality chains, and a line for each paper-level step. Comment lines only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9
- The docs claimed more than the theorems: simulations give equal random systems on an input domain; a deterministic automaton's theorem is the probability of its transcripts; a program replies memorylessly when its reply law is the same from every program state (module docs, the main-results list, THEORY.md). - `hκ` quantifies over the program states as `s'`, so it no longer shadows the start state `s` in the composition law and its typed forms. - PRG length extension uses `cc_calc quantitative`: its chain has no statistical step, so the domination argument of `cc_calc mixed` was unused. - Keywords follow the style of #18: `source_eq_memoryless`, `RandomSystem.ofProbAutomaton_ofDeterministic_apply` and `MemorylessSource.memoryless_eq` are corollaries, so `lemma`. - Comment wording: a repeated plan line removed, a chain realigned, two comments made exact. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9
MarcIlunga
force-pushed
the
memoryless-systems
branch
from
October 13, 2026 12:31
d66856f to
f357fa5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds probabilistic automata and the systems-level law for attaching a program's converter to one: the attachment is the program run against the automaton's step (
PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton, Maurer 2002 §3.3). The proof goes through the automaton as a random automaton reading a table of pre-sampled draws (Maurer 2002, Definition 2).Memoryless systems follow as a corollary (CR18 Definition 3.1, §3.6.1): attaching a program to a memoryless system gives a memoryless system. The PR also adds their typed forms, the memoryless source in Commons, and PRG length extension (Boneh–Shoup §3.4.2) as an example.
Closes #11. Part of #14.