Maximus Gorog bd2e14214d Add 'tsm-lean/' from commit '2e9061abead6f2daa464b39a79c17a949db30785'

git-subtree-dir: tsm-lean
git-subtree-mainline: 6592cd058d
git-subtree-split: 2e9061abea

2026-05-12 02:59:14 -06:00

2.4 KiB

Raw Permalink Blame History

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

lake build

Run the demo

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.

2.4 KiB Raw Permalink Blame History