Rtm to tm - #14
Draft
crei wants to merge 16 commits into
Draft
Conversation
Introduce the RoseTreeMachine module: `Data`, a rose-tree structure for encoding Lean data (with decidable equality, size measure, and recursion/ induction principles), `DataEncode` instances for encoding `Bool`, `List`, and other types into `Data`, and `Prog`/`ProgSem` defining the RTM programming language along with its time/space complexity notions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add `Complexitylib.Models.RoseTreeMachine.Compile`, the first verified slice of the InPlace rose tree machine to Turing machine compiler. It relates the RTM `ProgSem` cost model to Turing-machine time and space up to a constant factor (the notion the RTM's own `ComputableInOTime`/`ComputableInOSpace` already use). Provides: - `InPlaceRealizedByTM`, the per-program correspondence predicate: same binary function, with TM time/space bounds dominated by the program's RTM bounds. - `dataSize_encode_listBool`, the reusable bridge showing the binary encoding of a `List Bool` has `Data.size` linear in the list length. - `emptyOutputTM` plus its time and space correctness, and `empty_realized`: the `empty` program is realized with matching time and space. - `identity_time_matches`: the `var 0` program and `copyInputToOutputTM` both compute the identity, with matching linear time. The inductive constructors remain tracked as future work in ROADMAP.md. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add `inPlace_compilesToTM`: for every InPlace rose tree machine program `p` there is a single Turing machine `M` (with constants `a`, `b` depending only on `p`) that, whenever `p` computes a binary function `f` within RTM time `tR`/space `sR`, computes the same `f` within TM time `a*tR+a` and auxiliary space `b*sR+b`. The `ComputesInTime`/`ComputesInSpace` certificates make `M` usable as a subroutine (e.g. via `seqTM`/`compositionTM`). The statement is provided now to fix the subroutine interface; the proof is a `sorry` pending the inductive constructors' data-manipulation subroutines (tracked in ROADMAP.md). Note: this makes `lake build --wfail` and the axiom guard report the declaration until the proof lands. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Introduce the internal, layout-relative compiler contract so an InPlace program's multiple arguments map to distinct Turing-machine work tapes, while keeping the public inPlace_compilesToTM theorem on the standard single-input / single-output subroutine interface. - Data.toBits / toBitsList: balanced-parenthesis serialization of a Data value to List Bool, with Data.toBits_length : length = Data.size (bridges RTM Data.size space to physical tape cells). - LoadedStart: multi-tape analogue of Cfg.init placing argument j on work tape slot j via Data.toBits. - CompilesUnder M slot res p a b: the layout-relative correctness-and-resource contract the InPlace recursion is proved against (time a*t+a, work-head space b*s+b). - compilesUnder_of_inPlace: internal recursion statement (sorry); the public inPlace_compilesToTM is its m=1 wrapper (prologue unpacks input tape onto the argument tape, epilogue copies the result tape to output; renumbering via the existing Lift/RetargetCompute/Placement combinators). Both headline statements remain sorry, so lake build --wfail and the axiom guard report them until proved. Style lint, full build, and env linter pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Split the monolithic compilesUnder_of_inPlace obligation into one lemma per InPlace constructor, and complete the recursion assembly with no sorry. - Compiled m p: shared codomain (exists a machine + layout satisfying CompilesUnder at argument arity m). - compiled_var, compiled_empty, compiled_cons, compiled_elim, compiled_ifEq, compiled_while, compiled_app: the individual compiler parts, each turning compiled sub-programs into the compiled composite. Arities follow the operational semantics' environment extension (elim body at m+2, while/app body at m+1). Statements only (sorry). - compilesUnder_of_inPlace: now proved by induction on the InPlace derivation, dispatching each case to its part. This assembly is sorry-free. Only the seven compiled_* parts (and the public inPlace_compilesToTM wrapper) remain sorry. Style lint, build, and env linter pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the `sorry` in `compiled_empty` with a full, machine-checked proof. Introduce `emptyNodeTM`, a 4-state multi-tape machine that materializes the empty node's serialization `[false, true]` on the result tape in three rightward steps, and prove it satisfies the layout-relative `CompilesUnder` contract for `Prog.empty`: the run has length 3 ≤ 2·2+2 and every reachable work head stays within 2·2+2, matching `ProgSem.empty` (time/space 2). Add supporting helpers `emptyStepOut`/`emptyStep` (one-step characterization), the write-and-move tape lemmas `writeAndMove_right_head`/`_cells` and `write_cells_of_ne_zero`, and `Γ.toΓwId` (write-back symbol map). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Restate `inPlace_compilesToTM` to quantify over source values `d : Data` and use their balanced-parenthesis serialization `d.toBits` as the physical tape I/O encoding, constraining only well-formed inputs. This makes the Turing-machine space charge coincide exactly with the RTM `Data.size` measure via `Data.toBits_length` (no constant blow-up) and aligns the public statement with the internal `LoadedStart`/`CompilesUnder` layer, which already serializes via `Data.toBits`. Drop the obsolete encode-based framing: the `DataEncode`-bridge lemmas `dataSize_encode_bool`/`dataSize_encode_listBool`, the `InPlaceRealizedByTM` correspondence predicate, and its base cases `empty_realized`/ `var0_computesBoolFun_id`/`identity_time_matches`. Update the module docstring accordingly. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Reframe `inPlace_compilesToTM` in the style of the binary-arithmetic subroutines (`binaryAddIntoTM` etc.): the caller runs the compiled program at tape indices of their choosing rather than on the dedicated input/output tapes. The theorem now exposes a scratch-tape count `sc` and constants `a`, `b` (all depending only on the program and arity `m`), then quantifies over a caller-owned tape bank `Fin k` with: - `argIdx : Fin m → Fin k` — variable `j` read from tape `argIdx j`; - `resIdx : Fin k` — result tape; - `scratchIdx : Fin sc → Fin k` — the auxiliary tapes to reserve; required pairwise disjoint. Inputs sit on the argument work tapes as their `Data.toBits` serialization (the input tape stays blank). Correctness/resources are stated as a `HoareTimeSpace` contract: the machine halts within `a·t + a` steps with `HasOutput result.toBits` on `resIdx`, leaves every other tape exactly as it started (arguments preserved read-only, scratch restored blank, untouched tapes untouched), and stays within `b·s + b` auxiliary space. Add the `Hoare.Space.Defs` import and update the module docstring. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Simplify the public `inPlace_compilesToTM` statement, which had grown to a deeply nested block of index arguments, disjointness hypotheses, loading premises, and inline Hoare pre/post predicates. Factor it into two named, individually documented abstractions so the theorem collapses to one line: - `SubroutineLayout m sc k` — bundles the caller-chosen argument/result/scratch tape indices together with their pairwise-distinctness proofs, plus a `SubroutineLayout.Loaded` predicate for the expected starting tapes. - `Prog.RunsAsSubroutine p m` — the full subroutine correctness-and-resource contract (scratch count, time/space constants, per-layout machine, and the `HoareTimeSpace` frame). `inPlace_compilesToTM` is now `p.RunsAsSubroutine m`. Behaviour is unchanged; this is purely a readability refactor. Update the module docstring. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the three separate tape maps (`argIdx`/`resIdx`/`scratchIdx`) and five pairwise-distinctness fields of `SubroutineLayout` with a single injective placement `place : SubroutineSlot m sc → Fin k`, where `SubroutineSlot m sc := Fin m ⊕ Unit ⊕ Fin sc` enumerates the argument, result, and scratch slots. The five distinctness conditions are exactly injectivity of `place`. Role accessors `argIdx`/`resIdx`/`scratchIdx` and the derived distinctness lemmas (`argIdx_inj`, `scratchIdx_inj`, `arg_ne_res`, `scratch_ne_res`, `arg_ne_scratch`) are recovered from `place_inj`, so `Loaded` and `Prog.RunsAsSubroutine` are unchanged. Update the module docstring. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Build the Turing machine that the rose tree `empty` constructor compiles to, targeting a caller-chosen work tape. - `emitBitsWorkTM idx w` — a reusable work-tape analogue of the output-tape `emitBitsTM`, appending a fixed word `w` to work tape `idx` one cell per step. Comes with `HoareTime` and `IsTransducer` contracts. - `emptyTM idx` — clears work tape `idx` first (so it works from any prior canonical Boolean content) then writes the empty node's serialization `[false, true]`. Proven `HoareTime` (linear time), `HoareTimeSpace` (additive space) and `IsTransducer` contracts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Reorganize the RTM → TM simulation code into a `Compile/` directory following the repo's three-layer architecture: - `Compile.lean` (surface) — keeps only the final theorem `inPlace_compilesToTM`. - `Compile/Defs.lean` — the human-auditable contract: `SubroutineSlot`, `SubroutineLayout` (+ accessors/distinctness lemmas, `Loaded`) and `Prog.RunsAsSubroutine`. - `Compile/Internal.lean` — all proof machinery (`Γ.toΓwId`, `emptyOutputTM`, `LoadedStart`/`CompilesUnder`/`Compiled`, the concrete per-constructor machines and `compiled_*` parts, `compilesUnder_of_inPlace`). - `Compile/Internal/EmptyTM.lean` — the empty-constructor machine (`emitBitsWorkTM`/`emptyTM`), moved from `RoseTreeMachine/EmptyTM.lean`. No definitions change; `Models.lean` now imports `Compile` transitively. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Switch the RTM->TM subroutine contract to the head-1 parked convention. A TM step applies a direction to every tape and idleDir moves a head reading the start marker rightward, so a head-0 Tape.init tape cannot be required to stay unchanged across a step. Loaded now places every layout tape parked at cell 1, and RunsAsSubroutine frames the (unused) input and output tapes as Parked and literally unchanged (inp = inp0, out = out0), with the input head at cell 1 so it fits the input-space allowance. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Prove the var-read compiler part of the RTM->TM compiler. When the de Bruijn index is in range (i < m) the argument value is already serialized on tape i, so the identity layout with res = slot i lets the trivial emptyOutputTM halt immediately with the value in place; when i >= m the read falls off the environment and yields the empty node, produced by emptyNodeTM. Factor the empty-node machine's run into a shared emptyNode_compilesUnder lemma (generalized to time/space bounds t,s >= 2 via ProgSem.size_le) now used by both compiled_empty and compiled_var, and add hasOutput_init_map (a tape initialized from w.map Γ.ofBool holds w as output). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Retarget the InPlace RTM to TM compiler recursion at the composable public subroutine contract `Prog.RunsAsSubroutine`, replacing the reaches-based `CompilesUnder`/`LoadedStart` machinery. `Compiled` is now a thin alias for `RunsAsSubroutine`, so the per-constructor part signatures and the recursion `compilesUnder_of_inPlace` are unchanged, and the surface theorem `inPlace_compilesToTM` is now wired to that recursion instead of an independent `sorry`. Prove `compiled_empty` in the new contract via `TM.emptyTM` (the parked-tape layout subroutine), with `HoareTimeSpace.consequence` fitting its constant time/additive space into the `a*t+a` / `b*s+b` budget. Strengthen `SubroutineLayout.Loaded` so every bank tape is parked at head 1 (`Parked ∧ head ≤ 1`), not just the layout tapes: parkedness is required for the "every non-result tape is preserved" frame to hold across idle steps, and the head-1 bound keeps non-layout tapes inside the `b*s+b` space budget from the initial configuration. Layout tapes already sit at head 1, so this only pins down the caller's spare tapes. `compiled_var`/`cons`/`elim`/`ifEq`/`while`/`app` remain `sorry` pending the `Data`-manipulation subroutines (copy-with-rewind, merge, equality comparator). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Prove the `var i` case of the RTM→TM compiler. For `i < m` the machine copies argument tape `i` to the result tape via `copyWorkToWorkTM` and restores the argument tape with `rewindWorkTM`; for `i ≥ m` it falls back to `emptyTM` to materialize the empty node. The copy/rewind pair adds only linear time and no extra space beyond the copied value, so the composed Hoare time/space contract fits the `a·t + a` / `b·s + b` subroutine budget with `a = clearWorkTimeBound 0 + 5`, `b = a + 1`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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.
No description provided.