feat(classes): add cryptographic primitives#5
Closed
SamuelSchlesinger wants to merge 61 commits into
Closed
Conversation
…re framework, and UTM Phase 1-2 Add TM composition operators (seqTM, ifTM, loopTM) with full δ_right_of_start proofs, Hoare-style specification framework with sequential composition rule, and UTM infrastructure including state normalization, binary encoding, helper machines (writeTM, rewindWorkTM, scanRightTM, copyInputToWorkTM, compareWorkTapesTM) with HoareTime proofs, and simulation config (SimConfig, stateOnTape). Zero sorry's, 1471 build jobs, zero errors, zero warnings.
Adds a Hoare-style loop invariant rule for loopTM that enables compositional reasoning about loops via a decreasing variant.
- complementTM_hoareTime: lifts original TM Hoare triple through complement, flipping output cell 1. Fully compositional. - ifTM_hoareTime: composes test Hoare triple with branch completion. The user proves branching via existing per-phase simulation lemmas. - Make compCfg, complementTM_simulation, complementTM_rewind_and_flip public for use in Hoare composition.
Extend ifTM_hoareTime to compose test, then-branch, and else-branch Hoare triples without the user ever seeing reachesIn. The theorem handles all internal phases (transition, rewind, check, branch routing) automatically. New infrastructure in IfInternal.lean: - tape_writeAndMove_stable, tape_move_idleDir_stable: one-step identity for stable tapes during readBackWrite/idleDir phases - ifTransitionTape_cells, ifTransitionInput_cells: cells preservation - ifTransitionTape_head_ge, ifTransitionInput_head_ge: head bounds - ifTM_rewind_loop_full: extended rewind tracking all tapes - ifTM_check_step_then_full, ifTM_check_step_else_full: check steps tracking all tapes
…frastructure Add Combinators/Internal/Generic.lean with shared proof tools: - simulation_reachesIn: generic simulation lifting (wrap commutes with step) - generic_rewind_loop / generic_rewind_loop_full: generic output-tape rewind - Shared tape stability lemmas (deduplicated from 4 Internal files) Restructure Combinators/Internal.lean into Internal/Union.lean (original content, byte-identical) + Internal/Generic.lean, with Internal.lean as aggregation. Refactor all combinator Internal files to use the generic tools: - 8 simulation proofs replaced with one-liner simulation_reachesIn calls - 3 rewind loop proofs (complement, if, loop) delegate to generic_rewind_loop - ~15 duplicated private tape lemmas removed Add AllTapesWF.ifTransition and ifTransitionTape_head_bound helpers to Hoare.lean, simplifying ifTM_hoareTime tape invariant threading. All public theorem signatures preserved; only proof bodies changed.
Add the full UTM sub-machine scaffolding and prove the hardest piece of readCurrentTM: the scan induction over super-cells with modular arithmetic for the position counter. Proved: - copyState_simulation: Phase 1 copy loop (induction on k) - scan base + inductive case: Phase 2 sim tape scanning - readHi single-step: transition after marker found - rewindSim_simulation: sim tape rewind (new theorem) - rewindState_simulation, rewindScratch_simulation: Phase 3 rewinds - checkHaltTM_hoareTime: full CheckHalt composition (1767 lines) - per_tape_simulation composition skeleton New files: ReadCurrent, ReadCurrentInternal, CheckHalt, CheckHaltInternal, SimConfig/Defs, Init, Lookup, ApplyTransition, ExtractOutput, UTM. 12 sorry's remain across 6 UTM files (down from ~20+ at session start).
Add InitInternal module with sub-machines for UTM initialization: Copy, Rewind, SetupState, SetupSim. Fix all non-sorry lint warnings in CheckHaltInternal and ReadCurrentInternal (unused variables, unused simp args, redundant intro).
Add tape helper lemmas (idle_tape_preserved, writeAndMove_*, etc.). Fix theorem signatures: add desc/state head hypotheses, scratch head = n+1. Partial phase1_loop proof: base case complete, inductive case needs hreach3.
Fill in the 3-step reachesIn proof (hreach3) completing the phase1_loop theorem. Uses writeAndMove_cells_at_head/ne for sim tape cell tracking and readBackWrite_cells for scratch tape preservation.
Extend phase1_loop postconditions with scratch cell preservation. Prove setupSim_phase12 by composing phase1_loop (3n+1 steps) with 6 simWriteRight extras and 1 advanceInput step (3n+8 total).
Revert broken phase12 merge. Clean state: phase1_loop fully proved, 3 sorry's remaining (phase12, phase3, hoareTime).
Compose phase1_loop(done=0) with 6 simWriteRight extras and 1 advanceInput step. Generic simwr_step helper handles all 6 extra steps uniformly. Extended phase1_loop postconditions with scratch cell preservation. Verified: lake env lean produces only sorry warnings for phase3/hoareTime.
- Complete proof of rewindScratch_loop (induction on scratch head h, h+1 steps from .rewindScratch to .bounceScratch with head 1) - Stub stride_loop helper (sorry'd body) - setupSim_phase3: suffices skeleton with generalized induction on remaining bits (processed counter), nil/cons cases sorry'd - setupSimTM_hoareTime still sorry'd - Other UTM files: upstream changes from prior sessions
…ear sim_head/ones/rest
…_hoareTime remain
…nitEnvelope + head bounds)
…_hoareTime' has unprovable bound (B universally quantified)
UTM sorry elimination
…me' sig - Add `rewindWorkTM_rich_hoareTime` to HelpersInternal.lean as public shared infrastructure. This preserves an arbitrary predicate P through rewindWorkTM, enabling data threading (descOnTape, stateOnTapeAt, superCellsCorrect) through rewind steps in seqTM compositions. - Add `tape_idle_preserve` to HelpersInternal.lean (public). - Remove duplicate private copies from CheckHaltInternal.lean. - Fix `readCurrentTM_hoareTime'` signature: change universally quantified `B : ℕ` (unprovable for small B) to existential `∃ B`. - Add `all_tapes_simulation` stub and helpers for Phase 2 iteration.
Close the Phase 2 iteration sorry: `all_tapes_simulation` iterates `per_tape_simulation` over all n+2 simulated tapes by induction on remaining tapes. `extract_sim_conditions` extracts per-tape marker/hi/lo conditions from `superCellsCorrect` via case analysis on the tape index (input/work/output). Remaining sorry in ReadCurrentInternal: `readCurrentTM_hoareTime'` (main composition of all 4 phases).
…lpers - Prove `extract_sim_conditions`: extracts per-tape marker/hi/lo conditions from superCellsCorrect for any target tape index. - Prove `all_tapes_simulation`: iterates per_tape_simulation over all n+2 tapes by induction, composing via reachesIn_trans. - Add simHeadPos, simCellsFn helpers for tape iteration. - readCurrentTM_hoareTime' still sorry'd (composition + scratchHasInputPattern).
…e sig Build the seqTM_hoareTime composition infrastructure for initTM_hoareTime': - Define copyData and setupStateData predicates for data-preserving rewinds - Prove preservation lemmas: copyData_preserved, setupStateData_preserved - Prove bridge lemmas: postCopy_to_copyData, postCopy_to_rewind0Pre, setupStatePost_to_rewind3Pre, postSetupSim_to_rewindAll (with initData) - Sketch main composition via 5 nested seqTM_hoareTime calls - Fix initTM_hoareTime signature: universal B→∃B, add full precondition Remaining sorry's in InitInternal.lean: rewind0/3 HoareTime specs, copyDataHead1/setupStateDataHead1 bridge lemmas, main composition.
…served Fully prove: - setupStateData_preserved: data survives rewind of tape 3 - rewind3_setupStateData_hoareTime: rich rewind for phase 4 Remaining sorry's: rewind0 pre-adaptation (read conditions), copyDataHead1/setupStateDataHead1 bridges, main composition.
Fully prove: - copyDataHead1_to_setupStatePre: InitEnvelope + setupState pre from copyData - rewind3_setupStateData_hoareTime: rich rewind for phase 4 - setupStateData_preserved: data survives tape 3 rewind - h_copyData_env partially addressed (head ≥ 1 added to copyData) Remaining sorry's in InitInternal: rewind0 read conditions (4 sub-goals), setupStateDataHead1_to_setupSimPre, h_copyData_env.
…etupStatePre Close 4 more sorry's in InitInternal.lean: - rewind0_copyData_hoareTime: rich rewind for phase 2 (tape 0), including initTape cell analysis for read conditions - copyDataHead1_to_setupStatePre: fully proved with InitEnvelope reconstruction - h_copyData_env: uses copyDataHead1_to_setupStatePre bridge Remaining sorry's in InitInternal.lean: setupStateDataHead1_to_setupSimPre (inp layout bridge) and h_copyData_env (InitEnvelope from copyData).
…analysis Close the rewind0 sorry including all 4 read-condition sub-goals: - inp.read ≠ Γ.start via initTape + encodeUTMInput_ne_start - out.read ≠ Γ.start via initTape [] at position 1 - Work tape reads via initTape [] at position 1 - Bound omega Remaining: 2 sorry's in InitInternal (h_copyData_env, setupStateDataHead1).
…ucture Major progress on initTM_hoareTime' composition: - Extract shared initTape_cells_ne_start and copyData_to_initEnvelope helpers - Fully prove h_copyData_env (InitEnvelope from copyData) - Prove setupStateDataHead1_to_setupSimPre structure with sorry's for fields not in setupState postcondition - Strengthen setupStateData with sim head, state head bound, inp layout - Fix setupStateData_preserved for new fields Remaining sorry's are well-localized: - setupStatePost_to_rewind3Pre: 4 sorry's (sim head=1, state head≤k+1, inp.cells, inp.head) — need setupStateTM_hoareTime postcondition strengthening (setupState preserves sim/inp, bounds state head) - setupStateDataHead1_to_setupSimPre: 3 sorry's (encodeUTMInput structure at specific positions — separator, x data, sentinel)
Close 4 more sorry's: - setupStateTM_simulation/hoareTime: add state head = k+1 / ≤ k+1 to postcondition (trivially from existing hst_h4 in phase4 claim) - setupStateDataHead1_to_setupSimPre: prove all 3 encodeUTMInput layout facts (separator, x data, end sentinel) via List.getElem?_append_right + List.getElem?_cons_succ Remaining: 3 sorry's in setupStatePost_to_rewind3Pre for sim head/inp preservation through setupState (need step-level idle tape preservation).
Major milestone: initTM_hoareTime' composition is fully proved (modulo upstream sorry's in SetupState/SetupSim sub-machine proofs). Changes to SetupState.lean: - Add state head ≤ k+1, sim tape preservation, input preservation to setupStateTM_simulation and setupStateTM_hoareTime postconditions - sim/input preservation sorry'd (need step-level idle tape analysis: setupState writes blank to blank sim cells with stay direction = identity, and input tape only moves with idleDir = stay when read ≠ ▷) Changes to InitInternal.lean: - Close all 7 sorry's: encodeUTMInput layout facts, InitEnvelope reconstruction, h_copyData_env bridge, setupStatePost bridge, setupStateDataHead1 bridge - Full composition structure proven via 5 nested seqTM_hoareTime calls with rich rewind specs and data-preserving predicates
Prove that setupStateTM preserves sim tape (tape 2) and input tape through any execution: - idle_tape_initTape: writeAndMove blank/stay on blank cell = identity - idle_input: move stay on input = identity - setupStateTM_sim_tape_idle: transition writes blank with idleDir to sim - setupStateTM_inp_dir_idle: transition uses idleDir for input direction - setupStateTM_step_sim_preserved: one step preserves sim tape - setupStateTM_step_inp_preserved: one step preserves input tape - setupStateTM_reachesIn_sim_preserved: full execution preserves sim - setupStateTM_reachesIn_inp_preserved: full execution preserves input Both InitInternal.lean and SetupState.lean now have ZERO sorry's. The initTM_hoareTime' composition proof is complete.
…nd sub-machine definitions - Strengthen all_tapes_simulation with hsc_vals₂ conjunct exposing per-cell encoded symbol values written to scratch tape for each simulated tape - Add hsc_above conjunct to per_tape_simulation for cells above written range - Add reachesIn_toReaches' helper for reachesIn → reaches conversion - Compose readCurrentTM_hoareTime' proof structure with all 4 phases (copyState → all_tapes → rewindState → rewindScratch); 3 sorry's remain: bound B value, t ≤ B, and scratchHasInputPattern postcondition - Expand lookupTM/applyTransitionTM definitions with proper state machines - Extract initTM definition to Init/Defs.lean to break circular import - Add extractOutputTM proper definition with rewind + scan + decode
…lyTransition Close all 4 ExtractOutput sorry's: - sim_cells_ne_start_of_scc: super-cell cells ≥ 1 are never ▷ - rewind_output_phase: output tape rewind by induction on head position - scanSim_phase: sim tape scan by induction on remaining count - extractOutputTM_hoareTime: 6-phase composition (rewind → rightOut → scanSim → readHi → readLo → writeOut → done) Added inp.read ≠ Γ.start to extractOutputTM_hoareTime precondition (valid in UTM context where input has been processed). Expand Lookup/ApplyTransition Fintype instances and δ_right_of_start (fully proved, no sorry's). Lookup/ApplyTransition HoareTime proofs remain sorry'd (Tier B). 4 sorry's remain: lookupTM_hoareTime, applyTransitionTM_hoareTime, utm_simulates, utm_correct.
Replace all `.blank` work writes with `readBackWrite (wHeads i)` and `.blank` output writes with `readBackWrite oHead` for non-halt state transitions. The previous `allIdle`-based transitions wrote `Γ.blank` at all tape head positions, corrupting data on desc/scratch/state/sim tapes. Also fix matchRewindR to advance desc past the separator bit (Dir3.right for utmDescTape), so copyOutput starts reading from the first output bit rather than the separator. Strengthen lookupTM_hoareTime precondition with `desc = encodeTM tm`, per-tape head bounds, and input/output tape conditions.
Create LookupInternal.lean with: - Tape helper lemmas (readBackWrite, idle preserve, write_head) - Encoding lemmas (input pattern, trans output, entry lengths) - skipHeader_loop — fully proved (induction on remaining header bits) - skipRest_loop — fully proved (induction on remaining entry bits) - rewindScratchFinal_loop — fully proved (induction on head position) - Phase simulation stubs for: compare_match_loop, compare_mismatch, rewindScratch_loop, process_nonmatch_entry, entry_scan_to_match, matchRewind_loop, matchRewindR_step, copyOutput_loop, rewindDesc_loop - lookupTimeBound time bound definition
Close rewindScratch_loop, matchRewind_loop, rewindDesc_loop, rewindScratchFinal_loop, matchRewindR_step, and skipRest_loop. Remaining sorry's: compare_match_loop, compare_mismatch, process_nonmatch_entry, entry_scan_to_match, copyOutput_loop.
…condition 5 sorry's remain: compare_match_loop, compare_mismatch, process_nonmatch_entry, entry_scan_to_match, copyOutput_loop. Key blocker: dite reduction in compare state δ transition.
Use split_ifs to handle nested if/dite in compare state transitions. This resolves the core blocker for compare_match_loop proof.
Close all sorry's except copyOutput_loop. Proved: - compare_match_loop via generalized induction on ipw-pos - compare_mismatch via generalized induction on mismatchPos - process_nonmatch_entry via composition - entry_scan_to_match via induction on numBefore Key technique: split_ifs handles nested if/dite in compare δ. Used simp [Nat.add_assoc] to fix Fin equality with dependent proofs.
Complete phase decomposition proofs for lookupTM: - skipHeader_loop: skip header bits on desc tape - compare_match_loop: compare all ipw bits, full match - compare_mismatch: compare with mismatch at given position - skipRest_loop: skip remaining entry bits after mismatch - rewindScratch_loop: rewind scratch after mismatch - process_nonmatch_entry: compose mismatch phases - entry_scan_to_match: scan past non-matching entries - matchRewind_loop: rewind scratch after match - matchRewindR_step: advance desc past separator - copyOutput_loop: copy output bits from desc to scratch - rewindDesc_loop: rewind desc to cell 1 - rewindScratchFinal_loop: final scratch rewind and halt Key techniques: - split_ifs for nested if/dite in compare transitions - suffices with generalized induction for compare/mismatch loops - Function.update reasoning for copyOutput cell tracking
…sorry's Add lookupTM_hoareTime_proof in LookupInternal.lean with the full phase composition structure. The proof chains all 12 phase lemmas via reachesIn_trans and verifies the postcondition. 7 sorry's remain, all in encoding-level facts: - Transition table structure from desc = encodeTM tm - Entry matching/non-matching conditions - Time bound calculation - Output bits correctness The phase simulation proofs (2034 lines) are complete. The encoding connection is the remaining work.
…dition - Extend copyOutput_loop postcondition with desc cells preservation, scratch head position (= ow + 1), and scratch cells beyond ow preserved - Close scratch head sorry: (c₅.work utmScratchTape).head ≥ 1 - Close desc cells sorry: chain cells preservation through all 7 phases - Close blank sentinel sorry: trace cell ow+1 back through phases - Add encoding helpers: allΓ_complete, allΓFuncs_complete, Γ_ofBool_injective - Add preconditions: desc head = 1, scratch sentinel cell = blank - Update Lookup.lean public spec to match Remaining sorry's: encoding connection (henc_connection) and time bound.
- Add encodeTransTable_eq_allTuples_flatMap: connects transTable to allTuples.flatMap - Add allTuples_entryFn and allTuples_entryFn_width: entry function with constant width - Close matching entry (refine_2): chain desc tape → table bits → entry bits → scratch - Close output bits (refine_3): same chain with encodeEntry_output_getElem - Remaining: non-matching entries (needs allTuples_nodup) and time bound
- Add allΓ_nodup: allΓ has no duplicates (by decide) - Add allTuples_nodup scaffold: levels 1-2 proved (pairwise disjoint by tuple component), level 3 needs allΓFuncs_nodup (sorry) - Clean up non-matching entries proof to document approach - 3 sorry's remain in LookupInternal: allΓFuncs_nodup (in allTuples_nodup), non-matching entries (blocked on nodup), time bound
…TComputable) Add foundational infrastructure for cryptographic formalization: - BitEncodable: specification-level typeclass for encoding types as bit strings, with instances for Unit, List Bool, Option, and Prod. - unpair: left inverse of pair, with roundtrip proof. - PPTComputable: predicate asserting a randomized function (List Bool → PMF (List Bool)) is computable by a PPT NTM, bridging NTM output distributions to Mathlib's PMF via ENNReal. - Make pair_nil_eq and pair_cons_eq public @[simp] lemmas.
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
2 participants
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.
Summary
BitEncodable: Specification-level typeclass for encoding types as bit strings (List Bool). Instances forUnit,List Bool,Option (List Bool), andProd. Used to state that a TM's bit-string I/O corresponds to a Lean function on abstract types — carries no computational obligation.unpair: Left inverse ofpairwith roundtrip proofunpair (pair x y) = (x, y). Returns([], [])for strings not in the image ofpair.PPTComputable: Predicate asserting a randomized functionList Bool → PMF (List Bool)is computable by a PPT NTM, bridging NTM output distributions (outputCount) to Mathlib'sPMFviaENNReal.pair_nil_eqandpair_cons_eqpublic@[simp]lemmas (needed byunpair_pair).Motivation
These are foundational building blocks for formalizing computational cryptography (KL Chapter 3). The cryptolib project will use
BitEncodableandPPTComputableto define encryption schemes where algorithms are Lean functions with PPT realizability asserted via existential TM witnesses.Test plan
lake buildpasses with no new errors or warnings