pre-release-2 audit — spec vs code consistency

scope: nox/specs/**.md compared against rs/reduce.rs, rs/patterns/.rs, rs/noun/.rs, rs/trace.rs, rs/call.rs

blockers

specs/patterns/15-hash.md:9 — hash cost stated f - 200 but reduce.rs defines COST_HASH = 300. fix: change spec to 300 or align code to 200 (cross-referenced everywhere; trace.md uses 300, others use 200 — see hash-cost group below).

specs/patterns/README.md:76 — cost table row "15 hash 200" contradicts COST_HASH=300 in reduce.rs:22. fix: change "200" → "300" (or align code).

specs/reduction.md:176 — example reduce(o, [15 a], f) = let (v, f1) = reduce(o, a, f-200) contradicts COST_HASH=300. fix: change "f-200" → "f-300".

specs/reduction.md:312 — "hash: 300" in this line is the only spec location that matches code; the surrounding hash references in the same file (lines 176, 153 column) say 200. fix: pick one number and propagate.

specs/jets/hash.md:17 — jet table "hash | ... | exec cost 200" contradicts COST_HASH=300. fix: align to 300 (or revise code).

specs/encoding.md:324 — formula encoding [17 a] (single-arg look) contradicts both rs/patterns/look.rs (calls cell_pair, expects two children ns/key) and specs/patterns/17-look.md:10 which uses [17 [ns_f key_f]]. fix: change to [17 [n k]].

specs/noun/README.md:44 — formula skeleton cell(17, key) (single-arg) contradicts the two-arg form in specs/patterns/17-look.md and rs/patterns/look.rs. fix: change to cell(17, cell(ns, key)).

specs/reduction.md:156 — dispatch table claims look has 1 sub-expression (17 look 1) but the implementation evaluates two sub-formulas (ns and key) and specs/patterns/17-look.md confirms two. fix: change subs column from 1 to 2 and note both eager.

specs/reduction.md:177 — example reduce(o, [17 k], f) = ... bbg.read(v) uses single-arg form; same bug as encoding.md:324. fix: rewrite as two-arg [17 [ns k]].

specs/trace.md:215-262 — pattern 8 inv multi-row layout claims 64 rows where row 0 is an init row and rows 1-62 are transitions; rs/patterns/inv.rs emits exactly 64 rows total but writes row 0 with r10=v, r11=1, r12=0 (init), then steps 1..=63 (63 step rows). spec says "row 0: r10=1 (accumulator initialized to 1)" — code initializes acc=v not 1. fix: either change spec to "row 0 acc=v (corresponds to MSB=1 of p-2)" or change code to start from acc=1 and process 64 bits.

specs/trace.md:262 — inv budget rule r8 = r9 = 0 on rows 1-63 is contradicted by rs/patterns/inv.rs:67-69 which copies step_row.r[8] = row.r[8] (budget_in) onto every step row, and only the final row sets r[9] = budget. fix: align spec ("r8 carries budget_in across all rows; r9 only set on final row") or change code.

specs/trace.md:370-420 — pattern 15 hash multi-row layout specifies "~300 consecutive rows" and step-by-step Poseidon2 progression; rs/patterns/hash.rs emits exactly 1 summary row (test hash_emits_one_row asserts count==1, code comments mark this as TODO). fix: add explicit "current implementation: single summary row; multi-row trace deferred to step-level hemera API" note in spec, OR mark trace.md hash layout as "target" with status flag.

specs/trace.md:84-93 — axis register layout specifies r4 = noun polynomial commitment, r5 = axis index, r6 = evaluation point, r7 = result value, with a Lens-opening constraint. rs/patterns/axis.rs:19-56 actually writes r4 = addr, r5 = addr (again, only for addr>=2), r6 = levels traversed, r7 = result NounId. there is no Lens commitment column and no evaluation-point encoding. fix: rewrite axis row layout to match implementation (or flag spec as "Lens-opening axis is target; current impl traverses cells").

specs/trace.md:438 — pattern 17 look register layout specifies r5 = BBG_root, r6 = value, r7/r10/r11 = Brakedown opening proof elements, plus Lens.verify constraint. rs/patterns/look.rs:27-31 writes r4 = ns, r5 = key, r6 = value only; no BBG_root, no proof elements, no commitment binding. fix: align spec to match minimal LookProvider implementation, or mark current code as stub.

specs/trace.md:530-538 — error-kind table says r10 = error kind and lists kinds 0..5 including 5 = call rejected. rs/reduce.rs:39-46 ErrorKind matches (TypeError=0, AxisError=1, InvZero=2, Unavailable=3, Malformed=4, CallRejected=5), and reduce.rs:117 writes row.r[10] = *k as u64. spec lists 3 = unavailable — resource exhausted (order full, provider returned nothing) — the "provider returned nothing" wording overlaps with Halt semantics in look.rs:34 (returns Error(Unavailable)) but call.rs:32 returns Halt(budget) for the same condition. fix: clarify which provider-None paths are Halt vs Error(Unavailable) and align look.rs to match call.rs convention (likely Halt).

major

specs/noun/tag.md:6-13 — value tower table lists three type tags (Field 0x00, Word 0x01, Hash 0x02 with 4 elements). rs/noun/tag.rs defines only two variants (Field, Word). Hash atoms are constructed as cell-of-cells in code (rs/noun/order.rs:79-87 hash_noun). Spec's "Hash type = single atom of 4 elements" model is not what code does. fix: revise tag.md to say "field and word are atom tags; hash is a structural cell of four field atoms".

specs/encoding.md:20-69 — atom tag 0x02 (hash atom, 33-byte encoding) is specified as a wire format type; no equivalent variant exists in Noun enum or Tag enum in code. fix: either implement the Hash atom variant or remove 0x02 from encoding spec and route 4-element hashes through the cell encoding.

specs/encoding.md:88-94 — encoding summary lists four sizes 9/9/33/65; with no Hash atom in code, the 33-byte path is dead spec. fix: drop 0x02 row or implement atom-hash variant.

specs/patterns/00-axis.md:6-12 — spec says axis(s, eval(a)) and "evaluated axis index must be a field-type or word-type atom"; rs/patterns/axis.rs takes the address atom directly from the formula body without an internal reduce() call (passes addr_ref straight to atom_value). fix: clarify that the address in [0 a] is a literal atom in the formula (not evaluated), or update code to reduce(a) first.

specs/noun/README.md:54-62 — axis table says axis(s, 0) = H(s) (hash introspection) and axis on an atom (except 0 and 1) produces ⊥_error; rs/patterns/axis.rs:21-37 implements addr==0 → H(s) and addr==1 → s, matching spec. patterns/00-axis.md:10 says "if eval(a) produces a cell or hash-type atom → ⊥_error" — this is more restrictive than implementation (which doesn't check tag on the address atom). fix: align 00-axis.md to README behavior.

specs/patterns/09-eq.md:8-9 — abstract semantics eq(a, b) → 0 if a = b in F (field equality only). rs/patterns/eq.rs:34 compares full noun digests (works on cells and hash nouns too). fix: spec to say "structural noun-identity equality across atoms, cells, hash nouns" — the code is stronger than spec claims.

specs/patterns/10-lt.md:8-9 — abstract semantics lt(a, b) → 0 if a < b under F's canonical ordering; rs/patterns/lt.rs:19-22 calls evaluate_field which type-errors on Word atoms. spec doesn't restrict types, code does. fix: state in 10-lt.md that operands must be Field type (TypeError on Word/cells).

specs/patterns/16-call.md:5-13 — semantics says "result = reduce([witness o], check_f); return result"; rs/patterns/call.rs:43-49 actually returns witness (not check_result) when check_result == 0. fix: change spec to "if check_result == 0 then return witness, else return CallRejected".

specs/patterns/16-call.md:30-40 — tag conventions table 0x00..0x04; this is an open convention but code/test in rs/patterns/call.rs use raw tag value with no enforcement. fine — only fix is to make spec explicitly say tags are application-level. fix: add "tags are not validated by the VM; any field value is accepted".

specs/patterns/17-look.md:9-20 — spec evaluates C_t = axis(o, BBG_ROOT_AXIS) to extract commitment root from object, plus error cases ⊥_namespace, ⊥_range, ⊥_commitment_root_missing; rs/patterns/look.rs ignores C_t entirely, calls hints.look(ns, key), returns only Unavailable on None. fix: either revise spec to current trait shape, or mark spec section as the target implementation with a "current implementation: stub via LookProvider" note.

specs/patterns/17-look.md:107-110 — cost table: "dispatch 1 + cost(ns_f) + cost(key_f) + 1 Brakedown opening"; reduce.rs uses cost=1 only for dispatch; no extra "+1" for opening. fix: drop the final "+1" or count it under jet costs.

specs/reduction.md:262 — error kinds list 0..4 missing 5 = call rejected. trace.md:530-538 lists kind 5. fix: add CallRejected to reduction.md error list.

specs/reduction.md:296-299 — instance includes (object_id, formula_id, result_id, status); trace.md:40-47 matches but reduction.md:299 says "r15 (status) and r12 (error kind)" while trace.md:530 says error kind is r10. fix: align reduction.md status/error register names to r10/r15→? actually code uses r10 for error kind; r15 is unused. fix reduction.md:299.

specs/trace.md:14-31 — register comment says r10-r15: reserved (zero-filled unless otherwise specified); per-pattern map uses r10 for inv/hash accumulator, r10-r12 for hash output, r10 for error kind. spec is internally consistent but the header summary table at line 28 hides this. fix: change r10 description in the header to "error kind / pattern-specific" and r11-r12 to "multi-row state / pattern-specific".

specs/trace.md:108 — pattern 1 quote constraint r7 = r4 (degree 1). rs/patterns/quote.rs:8-10 sets both r4 and r7 = body. consistent. fine. flagging that this is the only constraint with r4 == r7 redundancy.

specs/trace.md:148-165 — pattern 4 branch row layout uses r10 = selector; reduce.rs:117 also writes r10 = error_kind. on a non-error branch row r10 carries selector (0/1). these uses do not collide in practice but the spec needs to note "r10 is selector on branch success rows, error kind on error rows". fix: add an explicit per-pattern note. also rs/patterns/branch.rs:29-31 does NOT set r10 — code is missing the selector population. fix code or relax spec.

specs/trace.md:430-438 — pattern 16 call row: r5 = witness value (non-deterministic); rs/patterns/call.rs:46 writes r5 = witness as u64 (NounId, not value). consistent in role; spec wording "witness value" is misleading because it's a NounId reference. fix: change "witness value" → "witness NounId".

specs/trace.md:84-93 — pattern 0 axis spec says r5 = axis index, r6 = evaluation point; code writes r5=addr only when addr >= 2 and r6=levels traversed. r5/r6 redundancy and "evaluation point" naming are misleading. fix: align register names to actual usage (r5 = addr, r6 = depth navigated).

specs/trace.md:267-302 — pattern 9 eq r6 = 0 if equal, else 1 and r7 = (r4 - r5)^-1; rs/patterns/eq.rs:35-37 writes r4=ra NounId, r5=rb NounId, r6=0/1, but never writes r7 (no inverse hint). fix: either remove the r7 hint requirement (single-row constraint without hint) or have eq compute and emit the hint.

specs/trace.md:285-302 — pattern 10 lt spec includes r7 = range decomposition limb 0, r10 = limb 1, r11 = borrow/sign bit, and "~64 constraints"; rs/patterns/lt.rs:25-28 writes only r4=va, r5=vb, r6=0/1. no decomposition. fix: align spec to current stub or implement decomposition.

specs/trace.md:312-336 — patterns 11/12/13 xor/and/not specify r7 = bit decomposition witness 0, r10 = witness 1; rs/patterns/xor.rs (via word_binary_op in reduce.rs:197-223) and not.rs only write r4/r5/r6. no decomposition. fix: same as lt — align spec or implement.

specs/trace.md:358-368 — pattern 14 shl r7 = bit decomposition witness; rs/patterns/shl.rs:24-26 writes r4=va, r5=vn, r6=result only. no witness. fix: align.

specs/trace.md:498-505 — row-linking constraints describe r1/r2/r3 wiring across consecutive rows; reduce.rs pre-fills r1/r2 per call but does not enforce or model row-to-row wiring (single tracer.record per call, no continuity checks). fine for an interpreter, but spec language "r1_{t+1} = r1_t" reads as a constraint that no code enforces. fix: clarify this is a verifier-side constraint expected to hold over the emitted sequence, not enforced at trace-emit time.

specs/reduction.md:179 — abstract rule reduce(o, [8 a], f) = ... f-1 shows inv cost as 1; the abstract dispatch should use the per-pattern cost (64 for inv per reduction.md:311). fix: change to f - 64.

specs/README.md:14 — claim "jets.md | Layer 3: genesis jet registry"; nox crate exposes no jet module (rs/lib.rs lists noun/reduce/call/patterns/trace only). jets are spec-only / planned. fix: add a status note in jets.md and README that jet implementation is deferred.

specs/vm.md:8 — "five jets" wording is loose; jets.md lists 30+ jets across groups. fix: align vm.md to "30+ jets" or rewrite as "five jet groups".

specs/vm.md:30-41 — execution regimes table refers to repos nebu, kuro, jali, trop, genies; only nebu and hemera exist as path dependencies in the actual project (per CLAUDE.md table). fix: mark non-existent regime crates as "planned" or remove the table from the canonical spec.

specs/vm.md:36-37 — regimes kuro/jali/trop/genies referenced as wikilinks kuro etc.; companion repos do not exist in the cyberia-to workspace. fix: same as above — mark as planned.

specs/vm.md:213 — Hemera s-box "(partial rounds): x^{-1} (field inversion, 0^{-1} = 0)" — confirmed by hemera spec. consistent.

specs/vm.md:232-238 — domain separation tags list COMMITMENT/NULLIFIER/MERKLE/OWNER with byte sequences; no nox code path injects these. fix: mark as "protocol-level convention; not used by reduction patterns".

specs/encoding.md:301-325 — formula encoding table includes [16 [t c]] and [17 a]; the call form [16 [t c]] matches reduction.md and patterns/16-call.md, but [17 a] contradicts the two-arg look (see blocker above).

rs/noun/hash.rs:19 — hash_atom puts the tag byte INSIDE the absorbed data (data[8] = tag as u8) AND passes tag as the hemera tree domain parameter; specs/noun/hash.md:13-19 says tag goes only in capacity[14] not in input bytes. fix: align hash.rs to put tag only in capacity, or update the spec to document the dual encoding.

minor

specs/README.md:12 — "patterns/ | all 18 patterns: structural (0-4), field (5-10), bitwise (11-14), hash (15), call (16), look (17)" misses that there are 16 compute + call + look (this matches code), fine. minor: README counts 18 patterns but lists 7 groups; redundant phrasing.

specs/patterns/README.md:8 — "16 compute + call + look = 18 patterns"; consistent.

specs/reduction.md:30-46 — reduction signature documents Result = (Noun, Budget') | Halt | ⊥_error | ⊥_unavailable; code has Outcome::{Ok, Halt, Error} where Unavailable is an ErrorKind (not a separate variant). spec acknowledges this collapse at line 296 but the signature still implies four variants. fix: clarify "Unavailable is an error_kind, not a fourth variant".

specs/reduction.md:128-129 — "the partitioning scheme is not yet specified ... this is an open specification gap." — explicitly TBD, marked as such, no fix needed.

specs/reduction.md:240-249 — memoization scope description; consistent with code (no memo implementation in rs/, so spec describes future behavior). add "memoization layer not yet implemented in rs/" note.

specs/trace.md:418-420 — explicit TODO note: "current implementation emits a single summary row; full round-progression trace is deferred." — well-flagged; not a finding.

specs/trace.md:485 — header says "single-row (cost 1): 0-7, 9-14, 16, 17"; consistent with code multi-row check tag == TAG_INV || tag == TAG_HASH.

specs/jets.md:71 — table row "state | F_p | 6 (1 exact + 5 templates)" — spec-only; no code impact.

specs/jets/*.md — entire jets/ subdirectory describes planned jets with no rust-side counterpart. fix: add a top-level status flag to jets.md ("Layer 3 jets: specification-only, implementation deferred post-genesis").

specs/vm.md:251-256 — three-layer description: "Layer 3: 30+ jets across 5 algebras"; no jet code exists. covered above.

specs/encoding.md:226-262 — wire format / message types; no nox code touches wire encoding (this is downstream BBG/network concern). fix: mark as "consumer responsibility".

specs/noun/order.md:28 — "max count: 2^24 (16M nouns)"; rs/noun/order.rs uses a const generic N: usize without enforced upper bound (assert is_power_of_two only). fix: mark 2^24 as recommended default, not enforced.

specs/noun/order.md:29 — "max atom size: 4 field elements (32 bytes) ... hash type = 4 × F_p"; code has no 4-element atom (Hash atoms are cells). consistent with earlier finding on tag.md.

specs/CLAUDE.md (not under specs/) references "SuperSpartan + WHIR" while specs/vm.md:279 says "SuperSpartan + Brakedown"; zheng/specs/expander-pcs.md confirms Brakedown is the primary PCS. CLAUDE.md is out of audit scope; flagging that the cross-repo reference inside specs/ is correct.

specs/patterns/15-hash.md:14 — "hash CAN be expressed as pure Layer 1 patterns (~1000 field ops...)"; matches jets/hash.md:17 "pure cost: ~1,000". consistent.

specs/patterns/16-call.md:57 — "call dispatch: 1. tag evaluation: cost of tag_f. check evaluation: cost of check_f. total: 1 + cost(tag_f) + cost(check_f)" — consistent with reduce.rs (call cost=1 dispatch, sub-calls recurse).

specs/jets/hash.md:17 — "exec cost 200" — see hash-cost group above.

specs/encoding.md:32-43 — field atom encoding fully specified; no rust encoder/decoder exists in the crate. consumer responsibility; flagged.