feat: Hoare logic, TM combinators, encoding, and subroutines#7
Merged
Conversation
…roof infrastructure Add three new TM combinators for compositional machine construction: - seqTM: sequential composition (tm₁ then tm₂), time t₁ + 1 + t₂ - ifTM: conditional branching (test → rewind → branch), with then/else - loopTM: loop until test condition, with body + test + rewind cycle Refactor proof internals into modular structure: - Internal/Generic.lean: reusable simulation_reachesIn and generic_rewind_loop infrastructure - Internal/Union.lean: unionTM-specific proofs (extracted from Internal.lean) - SeqInternal, IfInternal, LoopInternal: per-combinator proof modules All proofs are sorry-free. The generic rewind loop pattern captures the recurring output-head-rewind used by complement, if, and loop combinators.
Introduce a Hoare triple framework for Turing machines:
- TapePred: predicates on (input, work, output) tape configurations
- HoareTime: time-bounded Hoare triple {pre} tm {post} [≤ bound]
- Hoare: unbounded variant for pure correctness
- Structural rules: consequence, weakening, strengthening, monotonicity
Composition rules for all combinators:
- seqTM_hoareTime: sequential composition with intermediate predicate
- complementTM_hoareTime: output bit flipping with head bound
- ifTM_hoareTime: conditional branching with AllTapesWF tracking
- loopTM_hoareTime: loop invariant rule with variant-based termination
AllTapesWF tracks well-formedness (cell 0 = ▷, cells ≥ 1 ≠ ▷) as a
stability invariant preserved through tape transitions.
…suppression - Extract `transitionTape`/`transitionInput` and their property lemmas (`_cells`, `_head_ge`, `_head_bound`) into Generic.lean as the single source of truth. These were previously duplicated as `seqTransitionTape`, `ifTransitionTape`, and `loopTransitionTape`. - Remove `set_option linter.unusedSimpArgs false` from Hoare.lean (the underlying simp calls were already clean). - Rename `AllTapesWF.ifTransition` → `AllTapesWF.transition` since the property is combinator-agnostic. Net: -64 lines, zero duplication of the phase-transition tape operations.
… and TM building blocks Extract general-purpose infrastructure from the UTM development: **Encoding.lean**: State normalization and binary encoding primitives. - `TM.normalize`: convert any TM to use `Fin (Fintype.card Q)` states, with full behavioral equivalence (`normalize_decidesInTime`) - `Γ.encode`/`Γ.decode`, `Γw.encode`, `Dir3.encode`: 2-bit symbol/direction encodings with roundtrip correctness - `Nat.toBits`/`Nat.fromBits`: fixed-width big-endian binary - `allΓ`, `allΓFuncs`: canonical enumeration of tape symbols **Subroutines.lean**: Five composable TM building blocks. - `writeTM sym`: write symbol to output cell 1 and halt - `rewindWorkTM idx`: rewind work tape to cell 1 - `scanRightTM idx`: scan work tape right until blank - `copyInputToWorkTM idx`: copy input tape to work tape - `compareWorkTapesTM i j`: compare two work tapes cell by cell **Subroutines/Internal.lean**: HoareTime specifications. - `writeTM_hoareTime`: time B+3, postcondition output cell 1 = sym.toΓ - `rewindWorkTM_hoareTime`: time B+2, postcondition head = 1 - `rewindWorkTM_rich_hoareTime`: preserves arbitrary predicate P through rewind **Generic.lean additions**: Frame rules for composition. - `transitionTape_id`: transitionTape is identity when tape reads non-▷ - `transitionInput_id`: same for input tape - `rightOfStart_allIdle` made public (needed by subroutines)
- Add time-bound formulas and tape transition explanation to Hoare.lean module docstring - Add docstrings to all config wrapping functions (phase1Wrap, phase2Wrap, ifTestWrap, ifThenWrap, ifElseWrap, loopBodyWrap, loopTestWrap)
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.
Summary
Compositional framework for building and verifying Turing machines, extracted and refined from the UTM development branch.
HoareTime/Hoare) with composition rules forseqTM,ifTM,loopTM,complementTMsimulation_reachesIn), rewind loops (generic_rewind_loop), frame rules (transitionTape_id)TM.normalize): convert any TM to useFin (Fintype.card Q)states with full behavioral equivalenceΓ.encode/Γ.decode,Nat.toBits/Nat.fromBitswith roundtrip correctnessHoareTimespecs:writeTM,rewindWorkTM,scanRightTM,copyInputToWorkTM,compareWorkTapesTMAll proofs are sorry-free. Only standard Lean axioms (
propext,Quot.sound,Classical.choice).New files
Hoare/Defs.leanTapePred,HoareTime,Hoare, structural rulesHoare.leanCombinators/Internal/Generic.leanCombinators/Internal/Union.leanunionTMsimulation proofs (refactored from Internal.lean)Combinators/SeqInternal.leanseqTMsimulation proofsCombinators/IfInternal.leanifTMsimulation proofsCombinators/LoopInternal.leanloopTMsimulation proofsEncoding.leanSubroutines.leanSubroutines/Internal.leanTime bounds
seqTM_hoareTimeb₁ + 1 + b₂complementTM_hoareTimeb + p_bound + 4ifTM_hoareTimeb_test + p_bound + max b_then b_else + 5loopTM_hoareTime(k + 1) * b_iterwriteTM_hoareTimeB + 3rewindWorkTM_hoareTimeB + 2Test plan
lake buildpasses with zero errors and zero warningslean_verifyconfirms only standard axioms on all key theoremssorry's across entire codebaseset_optionlinter suppressions