58 lines
2.4 KiB
Markdown
58 lines
2.4 KiB
Markdown
# tsm-lean
|
|
|
|
A Lean 4 formalization of a Tiny Stack Machine — third concrete kernel parallel to `golang-lean` (TGC) and `octive-lean` (TOC).
|
|
|
|
The substrate-level asymmetry: TGC and TOC have *named variables*. TSM has values living *by position* on a stack. Forces the cross-language abstraction to factor over "operand-access mechanism" instead of baking name-lookup into the framework. Maps directly to real bytecode targets — WebAssembly, JVM, CPython, .NET CIL, SECD.
|
|
|
|
## Build
|
|
|
|
```sh
|
|
lake build
|
|
```
|
|
|
|
## Run the demo
|
|
|
|
```sh
|
|
lake exe tsm-lean
|
|
# → final stack: [TsmLean.Core.Value.vInt 16] ((5 + 3) * 2)
|
|
# → final pc: 5
|
|
```
|
|
|
|
## Layout
|
|
|
|
| Path | What's there |
|
|
| --- | --- |
|
|
| `TsmLean/Core/Syntax.lean` | `Instr`, `Value`, `Code` |
|
|
| `TsmLean/Core/Semantics.lean` | `State`, `step` (function), `MultiStep` (relation) |
|
|
| `TsmLean/Core/Determinism.lean` | `step_deterministic`, `MultiStep.deterministic` |
|
|
| `TsmLean/Core/Eval.lean` | fuel-bounded `run` + `run_sound` |
|
|
| `TsmLean/Core/Types.lean` | `Ty`, `StackTy`, `HasTypeInstr` |
|
|
| `TsmLean/Core/TypeSoundness.lean` | `HasTypeV`, `HasTypeStack` |
|
|
| `TsmLean/Core/Preservation.lean` | `stack_preservation`, `progress` |
|
|
| `Main.lean` | demo program |
|
|
|
|
## Theorems proven
|
|
|
|
- **`step_deterministic`** — single-step is functional.
|
|
- **`MultiStep.deterministic`** — multi-step paths to halted states are unique.
|
|
- **`run_sound`** — successful fuel-bounded execution corresponds to a `MultiStep` derivation ending at a halted state.
|
|
- **`stack_preservation`** — if the stack matches an instruction's input type and the step succeeds, the post-stack matches its output type.
|
|
- **`progress`** — well-typed non-halt instructions always make a step.
|
|
|
|
The first three are the operational counterparts of the big-step theorems in TGC and TOC. The last two are the small-step type-soundness theorems (Pierce-style), which TGC/TOC's big-step formulations don't have direct analogues for.
|
|
|
|
Zero sorries, axioms, or admits.
|
|
|
|
## Status
|
|
|
|
**v0.1**: per-instruction (local) preservation. Global program-level type soundness — the JVM-style stackmap that ensures all reachable PCs have consistent stack types — is the next layer up.
|
|
|
|
## Instruction set
|
|
|
|
```
|
|
push n pushB b pop dup swap
|
|
add sub mul eq lt
|
|
jmp k jmpFalse k halt
|
|
```
|
|
|
|
Twelve instructions. No call / ret yet — direct jumps only. Adding function-call frames is a future extension.
|