Implement milestone 2 vanilla STARK proofs

Author: AbdelStark

Cargo.lock

@@ -14,19 +14,22 @@ path = "src/bin/tvm.rs"
 
 [features]
 default = []
-burn-model = ["dep:burn", "dep:serde_json"]
-onnx-export = ["dep:onnx-protobuf", "dep:protobuf", "dep:serde_json", "dep:tract-onnx"]
+burn-model = ["dep:burn"]
+onnx-export = ["dep:onnx-protobuf", "dep:protobuf", "dep:tract-onnx"]
 full = ["burn-model", "onnx-export"]
 
 [dependencies]
+ark-ff = "0.5"
+blake2 = "0.10"
 burn = { version = "=0.20.1", features = ["ndarray"], optional = true }
 clap = { version = "4.5.38", features = ["derive"] }
 crossterm = "0.28.1"
 onnx-protobuf = { version = "0.2.3", optional = true }
 protobuf = { version = "=3.4.0", optional = true }
 ratatui = "0.29.0"
 serde = { version = "1.0.219", features = ["derive"] }
-serde_json = { version = "1.0.140", optional = true }
+serde_json = "1.0.140"
+sha3 = "0.10"
 thiserror = "2.0.12"
 tract-onnx = { version = "0.23.0-dev.2", optional = true }
 
@@ -40,3 +43,7 @@ proptest = "1.6"
 [[bench]]
 name = "hull_benchmark"
 harness = false
+
+[[bench]]
+name = "vanillastark_benchmark"
+harness = false

Cargo.toml

@@ -63,7 +63,10 @@ A working implementation of the Percepta architecture in Rust:
 
 ### Milestone 2: Vanilla STARK Proof
 
-*Status: planned.*
+*Status: implemented for the average-hard execution path and the current arithmetic / control-flow VM subset. Unsupported instructions are rejected explicitly.*
+
+The in-repo prototype now lives under `src/vanillastark/` and is exposed as
+`transformer_vm_rs::vanillastark`.
 
 Build a minimal, self-contained STARK prover from scratch over the execution trace. No dependencies on production proving systems --- the goal is to understand and validate the proof construction end to end.
 
@@ -139,6 +142,12 @@ cargo run --bin tvm -- run programs/counter.tvm --max-steps 128 --trace
 # Verify transformer matches the native interpreter
 cargo run --bin tvm -- run programs/fibonacci.tvm --layers 3 --verify-native
 
+# Produce a standalone vanilla STARK proof for a program execution
+cargo run --bin tvm -- prove-stark programs/fibonacci.tvm -o fibonacci.proof.json
+
+# Verify a saved vanilla STARK proof without re-running the program
+cargo run --bin tvm -- verify-stark fibonacci.proof.json
+
 # Interactive TUI
 cargo run --bin tvm -- tui programs/fibonacci.tvm --layers 3 --max-steps 128
 
@@ -389,9 +398,9 @@ This is what makes long execution traces tractable. At step 1,000,000, each memo
 
 This is an MVP. Intentionally narrow, intentionally correct.
 
-**Implemented:** compact ISA, transformer execution, hull-backed memory, multiple attention modes, native interpreter, differential verification, CLI, TUI, benchmarks.
+**Implemented:** compact ISA, transformer execution, hull-backed memory, multiple attention modes, native interpreter, differential verification, CLI, TUI, benchmarks, vanilla STARK proofs for the current average-hard arithmetic / control-flow subset.
 
-**Not implemented:** WASM frontend, learned/trained weights, GPU acceleration, shared-address attention, STARK proof generation.
+**Not implemented:** WASM frontend, learned/trained weights, GPU acceleration, shared-address attention, full-ISA STARK AIR (bitwise / compare), non-average-hard proof paths, production STWO prover integration.
 
 The narrowness is the point. The semantics are small enough to inspect, strong enough to test, and structured enough to prove over.