Alchemist — Master Tracker

Autonomous C/C++ → verified safe Rust, on a local model (Gemma 4 31B, US-origin).

The one document for the whole climb: ~285 concrete milestones across 8 vertical phases (integration checkpoints — prove the stack on a bigger target) and 6 capability tracks (reusable capabilities, built once, applied everywhere). Each item has a definition-of-done and a difficulty tag. Finish every item and the project is genuinely complete: point it at a C/C++ codebase, walk away, come back to verified safe Rust.

Interactive, checkable version: docs/master-tracker.html (progress persists in-browser).

Progress at a glance (as of 2026-07-12)

Phase / Track	Done	Status
F · Foundations	12/12	✅ complete
P0 · Reliability Floor	14/14	✅ complete (+P0.8a)
P1 · Whole Small/Mid C Library	11/20 items	🔨 EXIT = CONVERGENCE (new-fixes/library → 0), not a lib count. real-library gate 1/5 (jsmn 1/2). parson 0 after 3 runs (fill wall); http-parser cold surfaced 2 new general blockers → generality is the front line. See re-orientation banner.
P1.5 · Generality gate (NEW)	0/5	🔨 the real bottleneck — general API-seq differential engine · coherence linter · per-shape e2e fixtures · decomposition · fill-scaffolding. Gates P2+.
P2 · Scale — Large Single Codebase	0/12	⬜ gated on P1.5 (scaling a non-general converter = the grind ×100)
P3 · C++ Frontier	0/8	⬜ gated on P1.5
P4 · Embedded & Unsafe Boundary	0/8	⬜ gated on P1.5
P5 · ArduPilot	0/22	⬜ frontier · gated on P1.5
P6 · Autonomy — Point & Walk Away	0/12	🔨 NOW, not a finale — the generality work IS P6, started 2026-07-14
Track · SEM (semantics)	0/70	⬜ *
Track · VER (verification)	0/25	🔨 2 active *
Track · MODEL	0/21	🔨 1 active *
Track · IDIOM	0/12	⬜ *
Track · PERF	0/8	⬜ *
Track · INFRA	0/20	⬜ *
TOTAL	34/261 (13%)

* Track vs phase counts overlap and are honest by design. The 6 capability Tracks are the reusable-capability backlog; when a track capability is delivered, it is recorded against the phase item that demanded it (e.g. the struct-carry, type-unifier, e2e-oracle, and decomposition capabilities live as F.7–F.9 and the shape system as P0.8/P0.8a/P0.9 + P1.15), not double-checked in the Track list. So the Track checkboxes read low even though much of their machinery is built and verified — they track remaining capability, phases track delivered capability. The reliability floor (F+P0 = 26 items) is 100% done; the current front is P1.

Where we sit in the field (researched, not guessed)

DARPA TRACTOR (2024) — a DoD program to translate all C to idiomatic, safe Rust. Validates the vision at the national-security level and is a funding lane. Our edge: verification-gated, model-writes-every-line, fail-closed.
c2rust (Galois/Immunant) — the mature mechanical transpiler, but it emits unsafe, unidiomatic Rust. Turning that into safe idiomatic Rust is the open problem we attack.
Laertes (OOPSLA'21) — automated unsafe→safe refactoring; its bounded success is the evidence this is genuinely hard.
LLM-translation studies — LLMs translate plausibly but unreliably; correctness demands an oracle. That finding is our thesis: the differential gate, not the model, is the source of truth.
Verification ladder — Miri (UB) → Kani (bounded model checking) → Prusti/Creusot/Verus (deductive) → Aeneas (functional translation validation). Climbed in the VER track.

Honest bottom line (REVISED 2026-07-14 after the http-parser cold test): the machinery is built but not yet general — that was the over-claim. A cold run of http-parser (a fresh, different-family library) surfaced 2 new general blockers before it could mint a single vector (&'staticstr lifetime-emit bug that breaks every &'static str/str_lookup return; the pipeline's own C-DLL build failed though the C compiles standalone). The blockers were general (not domain-overfit), which is good — but they existed because shapes/fixes are validated in isolation, not end-to-end on a real library, so every new library is the first real test and surfaces the latent bugs. The true gate to the product is therefore capability GENERALITY (a new unseen library needs ~0 human touches), not climbing to bigger targets. The phase ladder past P1 (scale → C++ → embedded → ArduPilot) is correct in content but must be gated on the generality bar — scaling a non-general converter just scales the per-library grind. "Perfect safe Rust for all of ArduPilot" is impossible as literally stated (hardware code is irreducibly unsafe); the real target is verified safe logic + a thin, audited unsafe shim.

🧭 Re-orientation (2026-07-14): generality is the gate, not target size

The product is "point it at a codebase, walk away, get verified safe Rust." This session's evidence (parson: 3 runs, 0 verified; http-parser: 2 new blockers on a fresh lib) says the bottleneck is generality, not scale. Re-sequencing, without discarding the ladder's content:

P1 exit = CONVERGENCE, not a lib count. The bar is "the Nth unseen library needs ≤1 human touch," measured by new-fixes-per-library → 0 (parson ~8 → http-parser 2 is the right slope; exit at ~0). A lib count alone just measures our patience.

Pull the generality capabilities forward as P1's real content (today buried in the Tracks at "0/70 someday"): the general API-sequence differential engine (collapse the per-family shape zoo into one engine); a coherence linter (catch &'staticstr-class bugs statically in <1s, not a 30-min run); an end-to-end fixture per shape (no shape ships un-exercised on a real function); decomposition for the deep tail; fill-scaffolding for novel structs (the parson wall).

Gate P2+ on the convergence bar — scale/domain phases start only once a new library is ~zero-touch.

P6 (autonomy / "walk away") is NOW, not a finale — the generality work above is P6, started today.

Legend

eng engineering · wire wire existing-but-dead code · research research-hard/open problem · model model-dependent · infra infrastructure · product product/GTM · unsafe irreducible unsafe boundary

Status: [ ] to-do · [~] active · [x] done · [!] blocked

Architecture — how the machine works, and where every item lives

Read this once and the whole tracker becomes navigable: each phase/track item below is a change to one of the components described here. Every item's note names the component and commit; this section says what that component IS and where its code lives. Paths are relative to the repo root (alchemist/…). Line counts are approximate load-bearing sizes, not limits.

0. The one idea

The oracle, not the model, is the source of truth. A local model (Gemma 4 31B, US-origin, on the box at :8086) writes every line of Rust. Nothing it writes is trusted until a byte-exact differential oracle — the compiled C reference, fuzzed through FFI and compared against the Rust — agrees on every input. No oracle ⇒ refuse (fail-closed). We never hand-write translation output; we build, run, and sharpen the converter. A refusal is an honest "we can't prove this yet," never a silent stub.

1. The 6-stage pipeline (`pipeline.py` orchestrates; `cli.py translate` is the entry point)

   C source dir
       │
  [1] analyze   analyzer/         parse C, build call graph, detect algorithmic modules
       │                          → parser.py, call_graph.py, module_detector.py, preprocessor.py
  [2] extract   extractor/        per-fn spec: signature, Rust-lifted types, test vectors, category
       │                          → spec_extractor.py, normalizer.py, function_classifier.py, schemas.py
  [3] architect architect/        design the crate/trait/type layout across modules
       │                          → crate_designer.py, trait_extractor.py, type_unifier.py, validator.py
  [4] implement implementer/      TDD fill: skeleton → emit tests → model fills each fn → in-loop verify
       │                          → tdd_generator.py (the heart), skeleton.py, test_generator.py
  [5] verify    verifier/         the 5-gate final differential proof (see §3)
       │                          → auto_config.py, adapter_gen.py, proptest_gen.py, differential_tester.py
  [6] report    reporter/         refusal ledger, metrics, perf, signed receipt
                                   → refusal_ledger.py, metrics.py, perf.py; receipt in verifier/receipt.py

Specs are checkpointed to <subject>/.alchemist/specs/; a run is resumable. solo.py runs a scoped single-/few-function translate for fast iteration; lib_orchestrator.py runs whole libraries.

2. The shape system — the central abstraction (this is what most items touch)

A C function is classified into a shape by its signature. The shape determines how the oracle mints inputs, compares outputs, and what tolerance applies. This is the extensibility surface: adding support for a new kind of function = adding a new shape.

Shape catalog (each is a classify_* + fuzz_* pair in verifier/auto_config.py, plus emitters):

Shape	C signature (archetype)	Rust lift	Oracle
`checksum`	`u32 f(const u8*, len[, seed])`	`fn(&[u8][,seed])->u32`	scalar compare, fold boundaries
`hash`/`digest`	`void f(const u8, len, u8 out)`	`fn(&[u8])->Vec<u8>`	digest bytes + NIST/FIPS catalog KATs
`scalar`	`T f(scalars…)`	`fn(scalars)->T`	scalar compare
`inplace`	`void f(u8* buf, len)`	`fn(&mut[u8])`	mutated-buffer compare
`buf_transform`	`int f(in,inlen,out,outlen)`	`fn(&[u8])->Vec<u8>`	out[0..ret]; decoder→roundtrip via `_paired_encoder_name`
`cbuf_out`	`char* f(char*)` (text→text, e.g. NMEA)	`fn(&str)->String`	result-string compare
`cstr_out`	`char* f(char*)` (text encoder)	`fn(&[u8]\|&str)->String`	NUL-terminated string compare
`cstr_scalar`	`T f(const char* s, scalars…)`	`fn(&str,…)->T`	scalar compare
`iarray_reduce`	`T f(const int* a, n)`	`fn(&[int])->T`	scalar reduce
`buf_gen`	`u8* f(size n,…)`	`fn(n,…)->Vec<u8>`	generated-buffer compare
`cstr_roundtrip`	`char* f(char)` binary-out decoder*	`fn(&str)->Result<Vec<u8>,E>`	P1.15: mint via paired C encoder, `decode(encode(p))==p`
`cipher_seq` / `alloc_seq` / `hash_seq`	init+op sharing a struct	struct-carried	sequence differential (state observer)
`scalar_mutator`	`void f(&mut State, scalars)`	struct-carried	state-mutation differential

⚠️ The N-site wiring rule (the single most important thing to know when adding/reading a shape). A shape is not one function — it is wired at 5–7 sites that must all agree, and there are TWO independent vector-dispatch paths that both need the shape or the fill loop silently sees "no test vectors":

classify_<shape>() + fuzz_<shape>_vectors() — verifier/auto_config.py
Dispatch A — synthesize_c_vectors() per-fn dispatch — verifier/auto_config.py (the pipeline calls this)
Dispatch B — the TDDGenerator fuzz backfill dispatch — implementer/tdd_generator.py (~line 2416). The generator clears machine-tagged vectors and re-mints via its own dispatch; a shape missing here dies even if Dispatch A produced vectors. (This bit us on P1.15.)
build_diff_config() harness branch — verifier/auto_config.py (feeds the final gate; must be checked before more-general shapes)
proptest block _proptest_<shape>_block() + VALID_CATEGORIES — verifier/proptest_gen.py
FFI adapter branch — verifier/adapter_gen.py (emits rust_<fn> and c_<fn> wrappers)
fill-loop test emitter _emit_<shape>_test() + the cargo-test name filter in _test_filters_for_fn() — implementer/test_generator.py + tdd_generator.py. (A missing filter ⇒ 0 tests run ⇒ false "no test vectors". Also bit us on P1.15.)

Canonical worked example of all 7 sites: P1.15 cstr_roundtrip (commits 07020fd→c8bff85). Simpler examples: P0.8a cstr_out, P0.8 iarray_reduce/cstr_scalar, P1-baseline buf_gen.

3. The verification gate stack (stage 5; the fail-closed proof)

Emitted by auto_config.build_diff_config() → adapter_gen + proptest_gen into a throwaway verify_gen/ crate, run by differential_tester.py:

gate 1 cargo check --workspace — it compiles.
gate 2 anti-stub scan (implementer/anti_stub.py) — no todo!()/unimplemented!()/trivial-constant returns.
gate (structural) no-unsafe proof — the output is safe Rust.
gate 3 semantic lints (implementer/semantic_lints.py) — no oracle-evading shortcuts.
gate 4 cargo test --workspace — the spec/KAT vectors (C-minted) pass.
gate 5 differential proptest — fresh fuzzed inputs, Rust vs C live, byte-exact.

Vector minting & crash isolation (synthesize_c_vectors): the C reference is compiled to a DLL and called via ctypes; because fuzzed inputs hit real C undefined behavior, minting runs in a forked child — a segfault returns 0 vectors (fail-closed) instead of killing the translator. A signed receipt (verifier/receipt.py) seals gates+harnesses+oracle+env with a content-SHA256 (optional HMAC).

4. Type & memory model (how the skeleton compiles cold)

struct-carry (verifier/struct_lift.py, wired in pipeline.py) lifts C state structs into Rust so the skeleton compiles before any body is filled. Resolves scalar typedefs (BYTE→u8), enum typedefs (jsmntype_t→i32), strips #ifdef in struct bodies, and raw-escapes keyword fields (type→r#type).
type_unifier (architect/type_unifier.py) auto-derives one coherent type model across fractured modules from the analysis (no hand-written registry — F.9).
normalizers (extractor/normalizer.py + auto_config lifts) canonicalize specs; solo._load_specs_and_arch re-applies them on every reload so a reloaded spec matches the in-memory one (P0.3).

5. Fill escalation ladder (`implementer/tdd_generator.py`, cheapest→dearest; `won_via` records which tier won)

cached (subject-anchored win cache <subject>/.alchemist/wins, P0.4) → deterministic template (init/reset init_templates.py; static-table no-op; free/destroy no-op) → single model fill → multi_sample best-of-N (multi_sample.py) → holistic whole-file fixer (holistic.py, self-terminates after 2 no-op patches, P0.5) → decomposition gcc-proven byte-exact split (structural_decomp.py, F.7). Reference transliteration via reference_probe.py.

6. Reliability & observability layer

refusal ledger (reporter/refusal_ledger.py) — the north-star metric: per-fn verified/refused + reason + won_via + telemetry (elapsed_s/llm_calls/output_tokens), plus wins_by_tier rollup. Written to <subject>/.alchemist/refusal_ledger.json.
deterministic replay — ALCHEMIST_DETERMINISTIC=1 forces temp 0 + single-sample everywhere (byte-identical output proven, P0.13).
benchmarks — bench/leaf/ (26 unseen leaf fns → scorecard, P0.11) and bench/lib/run_libbench.py (whole-lib batch → per-lib + overall refusal, P1.10). Nightly cron runs the real pipeline+model (P0.12).

7. How to trace any tracker item to its code

Every completed item's note carries (a) the component/shape it changed (names map to §1–6 above), (b) the commit SHA, and (c) the box-validation result where model-dependent. To go from an item to code: read the note → find the named module in the map above → git show <sha>. New capability items are almost always "a new shape" (§2, the 7 sites) or "a new gate/lever" (§3/§5).

Component → primary file quick map:

Concern	File(s)
Pipeline orchestration	`pipeline.py`, `cli.py`, `solo.py`, `lib_orchestrator.py`
Analyze	`analyzer/{parser,call_graph,module_detector,preprocessor}.py`
Extract / specs	`extractor/{spec_extractor,normalizer,function_classifier,schemas,fuzz_vectors}.py`
Architect / types	`architect/{crate_designer,trait_extractor,type_unifier,validator,schemas}.py`
Shapes & oracle config	`verifier/auto_config.py` (classify/fuzz/synthesize/build_diff_config)
Fill loop (the heart)	`implementer/tdd_generator.py`
Skeleton / tests	`implementer/{skeleton,test_generator,init_templates}.py`
Struct-carry	`verifier/struct_lift.py`
Gate emit	`verifier/{adapter_gen,proptest_gen,differential_tester,auto_ffi}.py`
Gates (stub/lint)	`implementer/{anti_stub,semantic_lints}.py`
Escalation tiers	`implementer/{multi_sample,holistic,structural_decomp,reference_probe}.py`
Report / receipts	`reporter/{refusal_ledger,metrics,perf}.py`, `verifier/receipt.py`
Benchmarks	`bench/leaf/`, `bench/lib/`

F · Foundations — already in the ground (DONE)

What exists and is verified today. The platform everything else stands on. Exit: a general, fail-closed, spec-first pipeline with real verified conversions behind it.

Foundations → code (each F item's primary location; see the Architecture §1 map for the full stage breakdown): F.1 pipeline.py + cli.py (stages) · F.2 verifier/auto_config.py + verifier/differential_tester.py (oracle) · F.3 zlib workspace under subjects/zlib*/ + verifier/zlib_config.py · F.4 subjects/sha256/ + standards/catalog.py (CAVP KATs) · F.5 libcrc subject workspace · F.6 implementer/scrubber.py + verifier/auto_ffi.py (static/inline strip + macro neutralize) · F.7 implementer/structural_decomp.py (wired in implementer/tdd_generator.py) · F.8 verifier/e2e_oracle.py (gated in pipeline.py verify) · F.9 architect/type_unifier.py · F.10 implementer/tdd_generator.py (cargo-fix pass, commit 36f1233) · F.11 verifier/auto_config.py + implementer/semantic_lints.py (the three false-refusal fixes) · F.12 Lua subjects under subjects/lua*/.

P0 · Reliability Floor (✅ COMPLETE — all 14 items + P0.8a)

Make single-function C→Rust on Gemma dependable. The wall we hit this week: correct code, sunk by mechanical trivia and false refusals. Exit (all met): tinychk reliably 4/4 ✅ · unseen leaf fns ≥90% verified (26-subject bench: 24/26 = 92.3%, cold-confirmed) ✅ · refusal ledger live (+ per-fn timing/cost + win-by-tier audit) ✅ · nightly cron runs the real pipeline+model ✅. Also delivered: deterministic-replay mode (byte-identical proven), subject-anchored win cache, spec-reload normalization, two new oracle shapes (iarray_reduce/cstr_scalar), cstr_out final-gate wiring.

P1 · Whole Small/Mid C Library — Push-Button (IN PROGRESS)

A never-seen C library → a verified Rust workspace, under 5% refusal, zero human touches. The first genuinely fundable claim. Exit (RE-REDEFINED 2026-07-14 — generality/convergence, not a lib count): ≥5 genuinely-unseen libraries converted FULLY hands-off, each ≥1000 LOC AND structurally hard (a parser/state-machine, or a pointer-linked + heap-allocation data structure — NOT a fat pile of independent leaf functions), each producing a byte-exact verified core + an honest, specific refusal tail (every refusal names what it couldn't prove and why), reproducible + signed-receipted — AND the crucial addition: new-human-fixes-per-library must trend to ~0 (the last 2 of the 5 need ≤1 touch each). Five libs banked via five rounds of hand-fixing proves we can hand-fix five libs; it does NOT prove the product. The convergence metric is the real exit — it is the difference between "we made 5 libraries work" and "the machine works on libraries." See the 2026-07-14 re-orientation banner above. The refusal rate is whatever it honestly is — the deliverable is a trustworthy verified core + a small hand-reviewable refused worklist, which is what c2rust (100% unsafe, unverified) cannot produce. Staged: prove the capability on jsmn (~340 LOC recursive parser — the unit test) first, then scale to the ≥1000-LOC libraries (the integration test). The old "5+ libs · refusal <5%" bar was met on 200-line primitives (the easy 80% of C) and is retired as insufficient for the fundable claim.

🎯 The real fundable claim (what P1 truly closes)

Point Alchemist at a real, messy, unseen C library, walk away, and every function comes back either byte-exact-verified against the original OR honestly, specifically refused with a reason — and the verified core is genuinely trustworthy because nothing shipped without the oracle agreeing. The verified-or-refused GUARANTEE is already always-on (fail-closed). What closes P1 is proving it, at useful COVERAGE, on ≥5 real ≥1000-LOC structurally-hard libraries.

The 3 keystones this requires (the capabilities the small-lib benchmark let us skip):

Whole-program type coherence — ✅ DONE (P1.18, 2026-07-13) — one canonical Rust type per C struct across ALL functions; carry EVERY referenced struct. jsmn exposed it: jsmn_parser came out as both ParserState and Parser, so a caller couldn't share the struct between init and parse. inject_state_shared_types now does a subject-wide canonicalization pass (pick one Rust name per C struct, rewrite every signature to it, emit one shared type per struct). Validated: jsmn's jsmn_parser collapses to a single ParserState across init+parse.

Parser-class oracle — ✅ DONE (P1.19, 2026-07-13) — differentially verify parse(input) → structured output: fuzz inputs (valid/malformed/truncated — real parsers must be safe on malformed), capture the C reference's token array AND signed return/error code, assert the Rust port matches byte-for-byte. New parse_seq shape in auto_config.py; validated model-free on real jsmn (captures {"a":1} → OBJECT/STRING/PRIMITIVE with exact spans, and {→PART / }→INVAL error returns). Unblocks jsmn / parson / http-parser.

Ownership at library scale — ✅ DONE (P1.20, 2026-07-13) — a pointer field to a carried struct is LIFTED to owned safe Rust (T* next → Option<Box<T>> for a single owned child; T* items + a length scalar → Vec<T> for a counted array/DOM) instead of being dropped, plus the transitive closure of reachable node types is emitted, so a linked-list / tree / DOM library gets a coherent compilable skeleton. Validated model-free (inject_state_shared_types on a real self-referential linked list → next: Option<Box<Node>>). Raw scalar/char buffer pointers still drop (rc4/allocators depend on it).

Real-library gate status: 0 / 5 done — but all 3 capability keystones now land, so the pipeline CAN handle the parser + heap-structure classes. jsmn (in-flight unit test) is UNBLOCKED (type-coherent + parser oracle); the model-fills-to-byte-exact end-to-end run is a box run (needs the local model). Candidates: parson (2760, JSON DOM), http-parser (~2500, state machine), a real hash table (pointer structure), heatshrink (stateful stream + ring buffer), tinycbor (codec). What remains is a run campaign, not R&D.

🏃 Run campaign log (started 2026-07-13, on the box + live Gemma)

Lib 1 — jsmn (parser unit test): ✅ VERIFIED 1/2 — the first real "verified core + honest refusal tail" on an unseen parser. jsmn_init verified byte-exact (parser-oracle init observer); jsmn_parse honestly refused (the model can't yet translate the ~200-line INLINED recursive parser — its static helpers are filtered out, so it can't decompose leaf-first). Lib 2 — parson (2760-LOC JSON DOM, opaque-typedef + tagged-union): 🔨 driven through EIGHT skeleton blockers, one run per fix. Started at "won't even compile"; each cold run peeled one general converter bug, all committed+synced: lifetimes → poison macros → file-I/O filter → typedef aliases → return-type/tag coherence → union-drop+alloc-Box → enum-type→i32 → scalar-typedef coherence (50bdfd6). Errors shrank from ~100 (every getter) to single specific type issues. Blocker #8 (JsonValueType ×3 E0425): parson declares enum json_value_type {..} and typedef int JSON_Value_Type; SEPARATELY (not typedef enum {..} T), so the enum-typedef scan missed the alias and the extractor's unresolved Rust type name JsonValueType broke the crate. Fix generalized inject_state_shared_types to resolve BOTH scalar typedefs (collect_scalar_typedefs→base Rust scalar) AND enum typedefs (→i32) via one signature-rewrite; real carried structs (JsonValue) untouched. Validated model-free on a parson typedef replica + 27-test keystone regression. parson9 → blocker #9 (bare Box/undefined-type): cleared the JsonValueType wall and reached implement, but parson-core failed compile with 6 errors: 4× bare Box in fn signatures + 2 extractor-invented undefined error types (SerializationError, ValidationError). Fixed general (bed5d97): no_std modules now use alloc::{boxed::Box,vec::Vec,string::String} so bare collection types resolve in signatures/fields/bodies; and the skeleton emits a pub struct <Name>; placeholder for ANY type a module signature references but never defines (broad scan when the crate has no deps; conservative error-position heuristic otherwise) → the crate always compiles. parson10 (cached specs, bed5d97): parson-core COMPILES ✅ (API ok) — but 0/99 verified, 99 honest refusals, all reason "no verifiable test vectors." parson's entire PUBLIC API is tagged-union DOM ops (json_object_set_string, json_array_append_boolean, json_value_get_type) over a linked JSON tree — none classify into an oracle shape, and its only leaf logic (hex/number/string helpers) is static (filtered). Honest outcome = compiles + 100% fail-closed refusal, zero false claims, but NO verified core → does not yet count toward the ≥5. To give parson a verified core needs a DOM tree-construction differential oracle + union→enum (a dedicated multi-part keystone), OR static-leaf exposure (#160). Decision (Jesse): BUILD parson's DOM oracle now (general to all tagged-union/DOM/AST libs). Part 1 DONE (7c40150) — union flattening: an inline C union field (JSON_Value_Value value;) is lifted to a FLATTENED safe sub-struct (one field per member) instead of dropped — chosen over a Rust enum so the access path v.value.number is identical to C (model writes plain field access, no match/discriminant), fully safe (no union/unsafe). collect_union_typedefs + emit_safe_struct(union_structs=) + PASS-3 closure now emit JsonValue{parent,type:i32,value:JsonValueValue} and JsonValueValue{number:f64,boolean:i32,null:i32,object/array:Option<Box<..>>} (string deferred to Tier-2). 50-test struct-lift/skeleton regression green; JSONValue→JsonValue casing now coheres. Next: Part 2 — the construct-observe oracle shape (pair scalar constructors T* init_X(scalar) with scalar getters scalar get_X(const T*); mint input→observed differential vectors) so null/boolean/number constructors+getters actually classify and verify → parson's first verified core. Then box-validate + bank as lib #2. Lib 3 — http-parser (3024-LOC goto state machine): ⏳ PRE-FLIGHTED + staged. Vendored + model-free-analyzed; 0 unions / 0 file-I/O (dodges parson's worst), 45 gotos, 2 opaque typedefs (covered). Diagnosis showed almost nothing classified → built the missing shape ahead of time.

Campaign has surfaced + fixed ~12 GENERAL converter capabilities (each committed+tested+synced), grouped:

Make any real C compile as a coherent Rust skeleton: compile-isolation (a06ff5c, the linchpin — a refused fn no longer sinks its verified siblings); lifetime elision (312d6d8); whole-program type coherence — opaque-typedef aliases keyed, return-only structs emitted, tag/alias unified, enum-type→i32 (faa1154, 31c772d); union-drop + alloc-qualified Box/Vec (1bd5455); no_std-safe rust_body (e7a9483); invalid-escape repair (38943c5); poison-macro/dangling-const filter (5ff2ac3); file-I/O filter (57e4935).

New oracle shapes (family-general): parser-class parse_seq + init observer (d1f3358, c2f9e1a); str_lookup — const char* f(enum)→string, a universal C idiom (629d968).

Runner autonomy: cache-prune so filter changes take effect without a manual wipe (a1508b6).

The compounding is real: http-parser (a different hard class) needed a shape parson didn't — but building str_lookup once covers http-parser's lookups and parson's _get_type accessors and every library's enum-name idiom. Fix an idiom, not a file. Remaining levers: C-union → Rust-enum keystone (upgrades parson from union-dropped-partial to fuller verification; general to all tagged-union libs); extract static helper fns for leaf-first parser decomposition (unblocks jsmn_parse + parser cores). Then bank the ≥5 real-library splits (parson, http-parser, a hash table, heatshrink/tinycbor).

📏 Distance to P1 complete (estimate, 2026-07-13)

Under the REDEFINED bar (2026-07-13): the infrastructure gates are met; the real-library gate is the whole remaining job.

P1 exit gate (redefined) Status

Signed receipts (tamper-evident) ✅ DONE — verify_receipt_integrity → True, → False after tamper (P1.14)

Reproducible (fresh-clone → same verified result) ✅ DONE — demonstrated on box (P1.14)

Verified-or-refused GUARANTEE (fail-closed) ✅ always-on — the architecture; every run

≥5 real ≥1000-LOC structurally-hard libs, hands-off, verified-core + honest refusals 🔴 0 / 5 — the real work. But ALL 3 capability keystones now land: #1 type coherence, #2 parser oracle, #3 ownership-at-scale. The easy-benchmark 4.8% and its 6 primitive passes are RETIRED as insufficient — they're the easy 80% of C.

Honest distance: the infra + guarantee are done, and all 3 hard capability builds now land (type coherence + parser oracle + ownership-at-scale) — the pipeline CAN now produce a coherent, compilable skeleton for the parser and heap-linked-structure classes, which is what blocked every real library. What remains for the fundable claim is the ≥5 real-library conversions — each a box run where the local model fills and the oracle verifies (or honestly refuses). This is a run campaign, not R&D: a multi-week compute campaign on the single box, staged jsmn → real libraries. Capability-complete (can the machine do it?) ≈ 95%; checkbox-complete = P1 11/20. We are NOT at "P1 done" (0/5 real libraries converted), and that's the correct, non-self-deceiving read — but the hard invention is behind us.

The expensive part — building the oracle SHAPES so the pipeline can handle each class of C library — is ~done (decoders, header-only, context-hashes, stateful sequences all landed this session). What remains is mostly a run campaign, not R&D:

~6 library conversions (P1.4–P1.9): "run the converter + triage the occasional new gap." ~0.5–1.5 sessions each ≈ ~6 focused sessions. Risk: a parser-class subject (http-parser) may hit the same type-coherence wall jsmn did (P2.2), +1–2 sessions.

Confirmation runs (P1.1 zlib, P1.2 libcrc, P1.3): already-conquered libs, fresh-clone re-prove ≈ ~1 session.

Reproducibility + receipts (P1.14): stranger-clone run + doc ≈ ~1 session.

jsmn canonical-naming (P2.2), if the parser class is wanted fully clean ≈ ~1–2 sessions.

Bottom line: ~8–10 focused, mostly-unattended run-and-triage sessions — a ~1–2 week compute campaign on the single box, no expected major capability walls (all 3 keystones now land). Capability-complete (can the machine do it?) ≈ 95%; checkbox-complete = P1 11/20. The load-bearing items — the 3 capability keystones — are all behind us; what's left is running the converter on real libraries.

📉 Refusal trajectory (cold 8-lib run_libbench.py)

Run Overall refusal Per-lib

Baseline (start of 2026-07-12) 23.5% 4/8 pass; sha256 & jsmn = 0/0 invisible failures

Post fix-waves 1-2 23.8% base64 0/0→2/2, heap 0/2→2/2; sha256/jsmn still dragged

After P1.15/16/17 + sha256 lint (fcda670) 9.5% base64 2/2, sha256 0/4→3/4, heap 2/2, murmur3 7/7, hashkit 3/3, siphash 1/1, rc4 1/2, jsmn 0/0

✅ After rc4 filter fix (fcda670) 4.8% — UNDER TARGET base64 2/2, sha256 3/4, siphash 1/1, murmur3 7/7, rc4 1/2→2/2, hashkit 3/3, heap 2/2, jsmn 0/0

🎯 4.8% HITS the P1.13 <5% refusal exit criterion (20 verified / 1 refused). The single remaining refusal is sha256_transform — the 64-round compression core, a model-capability frontier (NOT an oracle gap; the whole SHA-256 digest is proven byte-exact via P1.17). rc4 2/2 confirmed the stateful-sequence filter fix. jsmn advanced 0/0 → 0/2 (2026-07-13, commit d0f2d64): the header-only (P1.16) + non-first struct-carry (Token) fixes now make jsmn ingest AND its skeleton compile (struct-carry emits 3 structs; no more "cannot find type Token") — so its 2 functions are now visibly attempted rather than a silent 0/0. The remaining refusal is a distinct, larger gap: jsmn_parse (int f(Parser*, &str, &mut [Token]) -> count) has no oracle shape (parse-string-into-token-array) — the parser-class oracle, shared with P1.8 http-parser, a next capability. Plus the ParserState-vs-Parser inconsistent naming (P2.2 canonical-naming). jsmn is now a visible, precisely-diagnosed target. This session drove the whole-library refusal metric 23.5% → 4.8% purely by closing oracle-shape gaps and gate/accounting false-positives — the model was never the bottleneck. (Note: the P1 exit also needs 5+ libs converted hands-off with published receipts — P1.1–P1.9 — and reproducibility; 4.8% clears the refusal-rate bar.)

Baseline (2026-07-12, bench/lib/run_libbench.py, 8 unseen libs cold): 4/8 OVERALL PASS (siphash, murmur3, rc4, hashkit), overall function-level refusal 23.5%. Batch surfaced TWO problem classes: (a) shape-coverage refusals (base64_decode binary-out, rc4_keystream, heap alloc/free); (b) whole libraries producing 0/0 functions — the dangerous one, invisible to the refusal metric. Both 0/0 cases (sha256, jsmn) were STRUCT-CARRY failures now FIXED: scalar typedefs (BYTE/WORD → u8/u32; commit 9513ed6) + enum typedefs (jsmntype_t → i32) + #ifdef-in-struct-body + Rust-keyword field names (type→r#type; commit b0f0227). sha256's SHA256_CTX + jsmn's jsmntok_t/jsmn_parser now carry & compile cold (sha256 went total-failure → normal in-progress fill; the transform is just slow). Then closed a shape-coverage refusal: new buf_gen shape (<byteptr> f(<size> n, ...) -> Vec<u8>, commit a29c24a) — heap:make_buffer now verifies byte-exact on iter 1 (heap 0/2 → 1/2); generalizes to memset/pattern/PRNG fills. +8 regression tests.

Fix wave 2 (2026-07-12, commit 997e546, cold-VALIDATED on box): TWO whole-library unblocks landed + proven end-to-end. (1) free/destroy no-op template (free_noop_template, init_templates.py): a void free_X(ptr) whose C body is only deallocation calls is a no-op in safe Rust (owned Vec/Box drops) — accepted fail-closed (body-confirmed pure-free, else defer to model). heap:free_buffer now verifies → heap 1/2 → 2/2, OVERALL PASS, 0% refusal. (2) undefined-error placeholder (skeleton.py _lib_rs_for): the architect sometimes emits a trait method returning Result<_, SomeError> without defining SomeError, which broke the whole crate's compile → 0/0 functions filled. Skeleton now emits a minimal pub struct SomeError; + Display for any trait-referenced error type not defined/imported. base64 went 0/0 → 1/2: base64_encode verifies byte-exact; base64_decode still refuses (the binary-out decoder below). +7 regression tests, suite 777.

Fix wave 3 (2026-07-12, commits 07020fd→c8bff85, cold-VALIDATED): INVERSE-PAIR ROUNDTRIP ORACLE (P1.15) — base64 0/0 → 1/2 → 2/2 OVERALL PASS. base64_decode (char* f(char*) → Result<Vec<u8>,E>) refused with "no verifiable test vectors" (random fuzz strings aren't valid base64). Now the decoder class is unblocked: when a decoder is the inverse of an oracle-able encoder in the same subject, mint valid inputs by running the C ENCODER on random ASCII plaintext and require decode(encode(p)) == p. base64_decode is the first char* binary-out decoder the pipeline verifies byte-exact. Generalizes to inflate/decompress/deserialize. Details in P1.15 below.

Post-fix aggregate (2026-07-12, fresh cold 8-lib batch on all fixes, run_libbench.py): OVERALL REFUSAL 23.8% — ~flat vs the 23.5% baseline, but the flatness is misleading: the wins are real and confirmed at scale (base64 2/2 0% ✅, heap 2/2 0% ✅, murmur3 7/7, hashkit 3/3, siphash 1/1), while the aggregate is dominated by the two hardest libraries, which are DIFFERENT problems than the ones fixed: sha256 0/4 (the 64-round transform is genuinely hard/slow to verify cold — needs a decomposition or longer budget, not a coverage fix) and jsmn 0/0 (header-only + recursive parser — see below). The refusal % is a blunt whole-library aggregate; per-capability the frontier moved (decoder class + header-only libs are new).

sha256 0/4 root-caused + partly fixed (2026-07-12, commit 06166a7): the 0/4 was NOT a timeout — it was a two-stage blocker. (1) Semantic-lint false-positive [FIXED]: lint_sha256 (semantic_lints.py) required the H0[0] constant 0x6a09e667 in EVERY sha256-family function, but it lives only in sha256_init; sha256_transform/update/final were refused on every iteration ("semantic lint rejected iter 1–5"). Scoped the check to skip state-consuming helpers (transform/update/final/compress/block); still enforced on init + monolithic. +2 tests. (2) Remaining blocker [FIXED via P1.17 — DONE]: with the lint clear, all 4 fns hit "no test vectors" — sha256 is a stateful context-hash sequence (init(ctx)→update(ctx,data,len)→final(ctx,out_digest) over the multi-field SHA256_CTX). The existing hash_seq oracle only handled a SINGLE-SCALAR state with a SCALAR-returning final (FNV). Built the digest-sequence oracle (P1.17, commit add0847) — multi-field ctx + final(ctx, out_digest) — which took sha256 0/4 → 3/4 verified with the whole-sequence digest differential byte-exact GREEN. Lone holdout sha256_transform (64-round core) is a model-capability frontier, not an oracle gap. Unblocks the whole SHA/MD5/SHA-1/HMAC class. See P1.17 below.

jsmn diagnosis + two header-only fixes (2026-07-12, commits dd97d92, 32a3df9): jsmn showed the dangerous 0/0 "invisible failure." Root cause was NOT struct-carry — it was a .c-only assumption in TWO stages: (1) module_detector._group_by_file grouped only .c files into modules, so a header-only library (jsmn, stb-style — whole impl in the .h) produced 0 modules; (2) spec_extractor._extract_module read function bodies only from .c, so even once detected the functions weren't read ("No functions found"). Both fixed (the parser only records definitions, so a .h with a non-empty functions list is a source module; +6 tests). jsmn now passes analyze → extract → architect cleanly (6 fns detected, 2 algorithms after static-helper filtering, architecture validated 0 errors) — the invisible 0/0 dead-end is eliminated. Next jsmn blocker (root-caused, deferred — P2-class): the skeleton fails to compile with cannot find type Token. Precise cause: struct_lift.inject_state_shared_types only carries the params[0] STATE struct (jsmn_parser → ParserState, keyed on the spec's first-param lift, struct_lift.py:355). jsmntok_t appears as a secondary parameter — the token-array element type (tokens: &mut [Token]) — which struct-carry never emits, and the architect independently renamed it Token, so the reference dangles. The general fix is to carry EVERY struct type referenced in ANY function signature (not just params[0]) under the name the spec/architect uses — a real whole-program-type enhancement (P2). Only THEN does the recursive-descent parser itself have to verify (hardest, research). jsmn is now a visible, root-caused in-progress target, not a silent failure.

Remaining refusal worklist: rc4_keystream — verified via the cipher-sequence gate but the per-fn ledger marks it refused (accounting false-negative; needs sequence-member crediting).

P1 exit gate (redefined)	Status
Signed receipts (tamper-evident)	✅ DONE — `verify_receipt_integrity → True`, `→ False` after tamper (P1.14)
Reproducible (fresh-clone → same verified result)	✅ DONE — demonstrated on box (P1.14)
Verified-or-refused GUARANTEE (fail-closed)	✅ always-on — the architecture; every run
≥5 real ≥1000-LOC structurally-hard libs, hands-off, verified-core + honest refusals	🔴 0 / 5 — the real work. But ALL 3 capability keystones now land: #1 type coherence, #2 parser oracle, #3 ownership-at-scale. The easy-benchmark 4.8% and its 6 primitive passes are RETIRED as insufficient — they're the easy 80% of C.

Run	Overall refusal	Per-lib
Baseline (start of 2026-07-12)	23.5%	4/8 pass; sha256 & jsmn = 0/0 invisible failures
Post fix-waves 1-2	23.8%	base64 0/0→2/2, heap 0/2→2/2; sha256/jsmn still dragged
After P1.15/16/17 + sha256 lint (`fcda670`)	9.5%	base64 2/2, sha256 0/4→3/4, heap 2/2, murmur3 7/7, hashkit 3/3, siphash 1/1, rc4 1/2, jsmn 0/0
✅ After rc4 filter fix (`fcda670`)	4.8% — UNDER TARGET	base64 2/2, sha256 3/4, siphash 1/1, murmur3 7/7, rc4 1/2→2/2, hashkit 3/3, heap 2/2, jsmn 0/0

P2 · Scale — Large Single C Codebase (MID)

A 30k–100k-LOC C project (SQLite core, lwIP) → a verified Rust workspace over a long, resumable, unattended run. Exit: SQLite (or lwIP) core → verified workspace, honest refusals, resumable across days.

P3 · C++ Frontier (FAR)

Prove the C++ capability stack (built in SEM) on real targets. ArduPilot is majority C++; the pipeline is C-first today. Exit: a header-only C++ lib + a small C++ project (classes, templates, RAII) → verified idiomatic Rust.

P3.1 C++ tree-sitter analyzer + TU model eng
P3.2 C++ reference-oracle build + mangling-aware FFI eng
P3.3 Header-only C++ library milestone research
P3.4 A small class-based C++ project research
P3.5 A mid C++ library with templates + STL research
P3.6 Method-call differential harness eng
P3.7 C++ refusal taxonomy proven (multiple inheritance, heavy TMP flagged) eng
P3.8 C++ idiomaticity bar — traits/generics/ownership, not transliterated C++ research

P4 · Embedded & the Unsafe Boundary (FAR)

Where "perfect safe Rust" meets physics. Draw the unsafe boundary in exactly the right place and audit it. Exit: a real driver → safe algorithmic Rust + a thin, audited, clearly-marked unsafe HAL shim, verified at the boundary.

P4.1 no_std translation path eng
P4.2 Safe-vs-irreducibly-unsafe classifier unsafe
P4.3 A real embedded driver end-to-end (IMU/sensor) unsafe
P4.4 Boundary verification — safe-core differential + shim contract tests eng
P4.5 Unsafe-audit report — every block justified, minimized, reviewed unsafe
P4.6 RTOS abstraction shim milestone (ChibiOS/NuttX primitives → traits) unsafe
P4.7 Static-allocation / no-heap path proven eng
P4.8 Timing-preservation validation unsafe

P5 · ArduPilot (FRONTIER)

The dream target, in flyable slices. Algorithmic layers first (verified), then the boundary, with SITL as the behavioral oracle. Exit: AP_Math / filters / CRC verified byte-exact · a control subset behaviorally matched in SITL · a flyable-in-simulation Rust slice.

P6 · Autonomy — Point & Walk Away (CONTINUOUS)

alchemist translate <repo> runs unattended for hours→days and returns verified Rust + an honest refusal report. Exit: one command · unattended · resumable · verified workspace + a per-subsystem "% verified / % refused / why" report you can trust.

Track · SEM — C/C++ Semantics Coverage

Every C/C++ construct gets a sound, verified translation strategy — or an honest refusal. The correctness-completeness backbone. Exit: no construct silently mistranslated. Aliasing, unions, and UB respected, not ignored.

Memory & pointers

SEM.1 Pointer provenance & aliasing model — C's unrestricted aliasing → Rust's borrow model (the #1 hard problem) research
SEM.2 restrict/noalias exploitation → non-overlapping slice APIs research
SEM.3 Pointer arithmetic → slice/index or raw-ptr-in-unsafe with bounds proof research
SEM.4 Out-of-bounds-by-design (one-past-end, sentinels) → safe iterators/slices research
SEM.5 Multiple mutable aliases / shared mutable state → Cell/RefCell/split-borrow/indices research
SEM.6 container_of / offsetof / intrusive structures → safe ownership research
SEM.7 Tagged / low-bit-stashed pointers → safe encodings research
SEM.8 Null-pointer semantics → Option<&T>/Option eng
SEM.9 void* generic pointers → generics/enums/Box research

Memory model & UB

Control flow & functions

SEM.23 Computed goto / labels-as-values → state-machine lowering research
SEM.24 setjmp/longjmp → structured control flow / Result or refuse research
SEM.25 Variadic functions → refuse-or-shim unsafe
SEM.26 Function pointers & typedef'd signatures → fn ptr/dyn/enum research
SEM.27 Recursion & deep call graphs — stack-safety analysis eng
SEM.28 Comma operator / sequence points / eval order preserved eng

Preprocessor

SEM.29 Object-like & function-like macros → const/fn/inline, expansion-faithful research
SEM.30 Token pasting (##) & stringization (#) research
SEM.31 X-macros / macro-generated code → expand-then-translate research
SEM.32 Conditional compilation matrix (#if/#ifdef) research
SEM.33 Include-graph & translation-unit modeling eng

Qualifiers, atomics, concurrency, platform

C++

Track · VER — Verification & Formal Methods

From differential testing toward equivalence proof. Every function earns a sound gate — or an honest refusal. Exit: zero unverified emissions · each fn tagged with its proof method · cyclic cores verifiable · the oracle itself audited.

Track · MODEL — Model & Generation

Get the most from a local model — and close the self-improvement loop. The model isn't the bottleneck; the harness is. US-origin models only. Exit: high first-pass fill rate via better prompting, retrieval, repair, and a fine-tune on the tool's own verified conversions.

Track · IDIOM — Idiomaticity & Quality

The Rust must be genuinely good — idiomatic, clippy-clean, ergonomic — not a transliteration. Verified-preserving, always. Exit: output a Rust engineer would accept in review, correctness never traded for style.

Track · PERF — Performance Parity

The Rust must match or beat the C. A slower translation is a rejected translation. Exit: every conquered subject benchmarked; Rust ≥ C on time/size/allocation, with a regression gate.

PERF.1 Perf-parity gate threaded into the receipt (perf.py exists) wire
PERF.2 Benchmark suite per subject infra
PERF.3 Zero-cost-abstraction verification eng
PERF.4 Bounds-check elision where provably safe research
PERF.5 Binary-size parity eng
PERF.6 Allocation-behavior parity eng
PERF.7 SIMD / vectorization preservation research
PERF.8 Perf-regression gate across runs infra

Track · INFRA — Infrastructure, Eval & Product

The harness, the metrics, the trust story, and the path to funding. Exit: a public benchmark + leaderboard, reproducible signed receipts, one-command UX, a flagship dogfood demo, and a clear DARPA-TRACTOR/SBIR posture.

Critical path

F → P0 → P1 → P2 → P3 → P4 → P5 → P6, with tracks SEM · VER · MODEL · IDIOM · PERF · INFRA running alongside continuously. Vertical phases are integration checkpoints; tracks are the capabilities that feed them. The nearest fundable milestone is the P1 exit: an unseen real C library, converted hands-off, verified, under 5% refusal.

Caveats (honest)

Physics: "perfect safe Rust for all of ArduPilot" is unachievable as stated — register access, DMA, and ISRs are irreducibly unsafe. The real deliverable is verified safe Rust for the algorithmic layers + a thin, audited, clearly-marked unsafe hardware shim.
Research: research-tagged items are open problems, not schedule you can burn down on weekends. The whole ladder rests on the reliability floor (P0) holding.

Navigation Menu

Uh oh!

Alchemist — Master Tracker

Progress at a glance (as of 2026-07-12)

Where we sit in the field (researched, not guessed)

🧭 Re-orientation (2026-07-14): generality is the gate, not target size

Legend

Architecture — how the machine works, and where every item lives

0. The one idea

1. The 6-stage pipeline (`pipeline.py` orchestrates; `cli.py translate` is the entry point)

2. The shape system — the central abstraction (this is what most items touch)

3. The verification gate stack (stage 5; the fail-closed proof)

4. Type & memory model (how the skeleton compiles cold)

5. Fill escalation ladder (`implementer/tdd_generator.py`, cheapest→dearest; `won_via` records which tier won)

6. Reliability & observability layer

7. How to trace any tracker item to its code

F · Foundations — already in the ground (DONE)

P0 · Reliability Floor (✅ COMPLETE — all 14 items + P0.8a)

P1 · Whole Small/Mid C Library — Push-Button (IN PROGRESS)

🎯 The real fundable claim (what P1 truly closes)

🏃 Run campaign log (started 2026-07-13, on the box + live Gemma)

📏 Distance to P1 complete (estimate, 2026-07-13)

📉 Refusal trajectory (cold 8-lib `run_libbench.py`)

P2 · Scale — Large Single C Codebase (MID)

P3 · C++ Frontier (FAR)

P4 · Embedded & the Unsafe Boundary (FAR)

P5 · ArduPilot (FRONTIER)

P6 · Autonomy — Point & Walk Away (CONTINUOUS)

Track · SEM — C/C++ Semantics Coverage

Track · VER — Verification & Formal Methods

Track · MODEL — Model & Generation

Track · IDIOM — Idiomaticity & Quality

Track · PERF — Performance Parity

Track · INFRA — Infrastructure, Eval & Product

Critical path

Caveats (honest)

Uh oh!

FilesExpand file tree

MASTER_TRACKER.md

Latest commit

History

MASTER_TRACKER.md

File metadata and controls

Alchemist — Master Tracker

Progress at a glance (as of 2026-07-12)

Where we sit in the field (researched, not guessed)

🧭 Re-orientation (2026-07-14): generality is the gate, not target size

Legend

Architecture — how the machine works, and where every item lives

0. The one idea

1. The 6-stage pipeline (pipeline.py orchestrates; cli.py translate is the entry point)

2. The shape system — the central abstraction (this is what most items touch)

3. The verification gate stack (stage 5; the fail-closed proof)

4. Type & memory model (how the skeleton compiles cold)

5. Fill escalation ladder (implementer/tdd_generator.py, cheapest→dearest; won_via records which tier won)

6. Reliability & observability layer

7. How to trace any tracker item to its code

F · Foundations — already in the ground (DONE)

P0 · Reliability Floor (✅ COMPLETE — all 14 items + P0.8a)

P1 · Whole Small/Mid C Library — Push-Button (IN PROGRESS)

🎯 The real fundable claim (what P1 truly closes)

🏃 Run campaign log (started 2026-07-13, on the box + live Gemma)

📏 Distance to P1 complete (estimate, 2026-07-13)

📉 Refusal trajectory (cold 8-lib run_libbench.py)

P2 · Scale — Large Single C Codebase (MID)

P3 · C++ Frontier (FAR)

P4 · Embedded & the Unsafe Boundary (FAR)

P5 · ArduPilot (FRONTIER)

P6 · Autonomy — Point & Walk Away (CONTINUOUS)

Track · SEM — C/C++ Semantics Coverage

Track · VER — Verification & Formal Methods

Track · MODEL — Model & Generation

Track · IDIOM — Idiomaticity & Quality

Track · PERF — Performance Parity

Track · INFRA — Infrastructure, Eval & Product

Critical path

Caveats (honest)

1. The 6-stage pipeline (`pipeline.py` orchestrates; `cli.py translate` is the entry point)

5. Fill escalation ladder (`implementer/tdd_generator.py`, cheapest→dearest; `won_via` records which tier won)

📉 Refusal trajectory (cold 8-lib `run_libbench.py`)