Skip to content

HFIR parity: fix parse_json stack leak and map_get expression targets; HFIR in every verifier (#159, #155) - #160

Merged
howlcipher merged 1 commit into
mainfrom
fix-hfir-parity-159
Oct 12, 2026
Merged

howlcipher merged 1 commit into
mainfrom
fix-hfir-parity-159

Conversation

@howlcipher

Copy link
Copy Markdown
Owner

Fixes #159, Fixes #155

Experimental HFIR bytecode (-compile-hfir-bc) now agrees byte for byte (combined output, exit status, full sandbox file tree) with the interpreter (-run) and governed AST bytecode (build --profile governed + -run-bc) on every frozen HowlFrame benchmark solution.

Mismatch counts (HFIR vs interpreter/AST bytecode, same sandbox and grant)

Set Before After
heldout-v3 (baseline) 8/35 (x02, x03, x07, x08, x10, x11, x15, x27) 0/35
heldout-v3 postrec 8/35 (same IDs) 0/35
heldout-v2 1/37 (w22) 0/37
heldout-v2 postcf 1/37 (w22) 0/37
heldout-v1 5/34 (v17, v18, v19, v27, v29) 0/34
heldout-v0 0/30 0/30
v0 (token-efficiency) 0/60 0/60
Total 23/268 0/268

AST bytecode never diverged from the interpreter. The #155 shape ((print (encode_json (parse_json Any s)) (let (v (parse_json Any s)) …))) printed the raw s on base, and now prints the re-encoded JSON.

Root causes

  1. parse_json leaked its body onto the operand stack (x02, x03, x07, x08, x15, x27, w22, v17–v19, v27, v29, HFIR miscompile: encode_json(parse_json s) prints raw s when followed by a let argument #155). PARSE_JSON reads its body by variable name. The AST compiler emits only that instruction, but the HFIR lowerer also compiled the content edge (a LOAD_VAR of the same symbol). The stray raw string then got consumed by a later instruction:

    Fix: emit only PARSE_JSON, exactly as the AST compiler does. A content edge that is not the bound symbol now fails closed with a lowering diagnostic.

  2. map_get with an expression dict had no HFIR shape (x10, x11). (map_get (map_get t "meta") "tags") fell through to the generic node and failed with map_get requires a target name and key. Fix: lower it with target and key edges and emit the AST compiler's exact sequence, ending in MAP_GET with an empty variable operand.

Fail-closed: the capability fix widens nothing. The runtime check is untouched, and the program now hands WRITE_FILE the real path. TestHFIRParseJSONWriteFileStaysFailClosed checks all three paths: the write succeeds inside the write root, and is denied with no file written for a read-only grant or a different write root.

HFIR as a third path in CI

  • hfir_parity_cli_test.go / TestHFIRBenchmarkSolutionParity replays all 268 benchmark solutions on all 3 paths in fresh sandboxes. It runs in go test ./..., so any mismatch fails the build check.
  • experiments/internal/pathparity is shared by the heldout-v0/v1/v2/v3 verifiers (which also cover postcf/postrec through -howl-dir) and tokverify (v0). A HowlFrame task now passes only if the three paths agree. With the base binary the v3 verifier reports exactly Motoko's 8 failures; with this branch every verifier passes all tasks in all 4 languages.
  • tools/difftest: the CLI adds an HFIR leg. Only a lowering refusal of a construct on the locked promote-blocker fence (optimize_signature) skips the leg, so TestProdFlipCriteriaLock stays unchanged. A new TestHFIRRegressionParity uses the fixtures in tests/hfir_parity/.
  • Per-root-cause unit tests are in internal/hfir/issue159_test.go: no PARSE_JSON body leak (instruction stream equals the AST compiler's), non-symbol content fails closed, and the map_get expression target matches the AST compiler. All of them fail on base.

Constraints

  • No new opcode, capability or grant.
  • Production -compile-bc is untouched and there is no default flip. Write flagged http_server bytecode and stop #90 stays Partial, and TestProdFlipCriteriaLock is unchanged and passing.
  • All pinned results are byte-identical. I re-ran every verifier (heldout-v0/v1/v2/v3, postcf, postrec, v0) and git status shows no results/ change. Spec and results freeze tests pass.
  • gofmt -l . is empty, and go build ./..., go vet ./... and go test ./... pass. The Arity, Drift, Fuzz and Lock tests pass.

Not in scope / left open

  • The model adapter allow-list still lists only the key edge for map_get, so it stays narrower and rejects the new target shape (fail closed). That's for roadmap item 2.
  • tools/difftest's test_env.howl interpreter failure is environment-dependent and also fails on base.
  • The interpreter's runtime error text format differs from the VM's (for example list_len TYPE_ERROR). That's pre-existing, and no benchmark exercises it.

…s; add HFIR parity leg to verifiers and difftest (#159, #155)

@howlcipher howlcipher left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verdict: merge-ready (COMMENT). No blockers. Two nits below. Reviewed at 80da141 against base d7eb096, using one fresh clone plus a base worktree, built one after the other.

1. parse_json refusal

  • What's refused: the new diagnostic parse_json content must be a bound symbol fires only when the HFIR content edge is not a symbol whose value equals the node's operand. On the refusal path the lowerer returns a diagnostic and emits no instructions, so the compile fails cleanly (non-zero exit, no artifact). It can't produce wrong code, and it can't skip the governed scan or the capability checks, because nothing runs.
  • Legal shapes: I probed each one on all 3 paths and they all compile and match: nested in an expression, a read_text body, a (str s "") expression body, a defun argument, a return value, inside if, cond/else and for (both as the iterable and in the body), as the let value followed by a set rebind (assigned twice), and under chained map_get. A literal body is rejected by the checker on every path (bind it with let first), as before.
  • Newly refused programs: I compiled all 462 .howl files in the repo with -compile-hfir-bc on base and on head. Zero go from compiling to refused. Four go from refused to compiling: x10, x11, v29 and the new #159 fixture. In practice desugar always binds the body, so the new refusal is defensive and unreachable from source.

2. Stack-hygiene audit

I read every case in bytecode.go that ends in an opcode with a variable-name operand (let/set, map_get/list_get/map_delete/append, map_set, for, try, call, the stderr/convert/list_len/map_keys/env group). Each one compiles only the pushed edges the opcode pops; parse_json was the only one that also evaluated its by-name operand. read_json, rec/get/put and %/// desugar onto these, so they're covered too.

Differential fuzz: 600 generated programs, 535 of them with parse_json. Each mixes parse_json/read_json/read_text/rec/map_get chains/map_keys/%///, followed by WRITE_FILE, PRINT, MAP_GET-on-dict, let+write, for and if. I ran them under a read=in / write=out grant and compared output, exit code and the out/ tree (only the instruction index normalised). Head HFIR vs AST bytecode: 600/600 identical. The same corpus on base: 531/600 diverge, so the generator does hit the bug class.

Pre-existing, not HFIR: (print (encode_json (put d "c" 3))) prints null on -run but hits STACK_UNDERFLOW at ENCODE_JSON on both AST bytecode and HFIR. That happens on base too, so it's worth its own issue.

3. difftest HFIR skip

The predicate is strings.Contains(out7, "is not in the Phase-1 executable subset"). That's the generic default-case diagnostic (bytecode.go:726) for any unsupported node kind, not only optimize_signature. Among the tests/*.howl fixtures that reach testFixture, the only one that actually hits it is optimization_signature.howl. The others that would (store_open, spawn_agent, achieve, llm_generate, http/web_app, …) are already exempt in the manifest or are not a cli_app. So the effective scope is narrow and correct, but the predicate is broad.

Nit: a fenced fixture is counted as Passed with out8 = out1, with no SKIP line. Please match on node kind \"optimize_signature\" (or an explicit kind list) and print SKIP-HFIR <file>: <kind> so new fenced kinds can't hide silently.

The difftest run itself gives 17 passed, 31 skipped and 1 failed: test_env.howl hits a capability denial on the interpreter, and it fails the same way on the base binary.

4. Parity

  • Verifiers with the head binary: heldout-v0, v1, v2 (and postcf), v3 (and postrec) and tokverify all exit 0. With the base binary, v1 has 5 failures, v2 has 1 and v3 has 8, which matches the table; with postcf and postrec that's 23 in total.
  • CI test: TestHFIRBenchmarkSolutionParity -v reports 268 PASS subtests.
  • Mutation check: I temporarily restored base bytecode.go locally and the test failed (exit 1, 23 failing subtests plus the parent). Then I reverted it.
  • examples/*.howl (22 files): capability_lab, cli_hello, release_gate and native_math are identical on all 3 paths. poll_cli differs only because of its time_now/sleep race (the attempt count varies), which isn't deterministic. All the others are refused by HFIR on unsupported kinds (http_server/web_app/wasm_app/spawn_agent/read_line), or are use-modules that every path rejects. Those refusals are the same as on base.

5. Fail-closed writes

I ran a parse_json-then-write program on base and head, on AST bytecode and HFIR, under a read=in / write=out grant:

  • out/ok.txt is written in all 4 runs.
  • other/x.txt, out/../other/t.txt, out/link/s.txt (a symlink to outside) and an absolute /tmp/... path all give CAPABILITY_DENIED with no file written, in all 4 runs.

With the push gone, nothing stray can become a WRITE_FILE path. The diff touches no capability or grant code, and TestHFIRParseJSONWriteFileStaysFailClosed passes.

6–8. Pins, locks, CI and hard nos

  • Pins: after re-running every verifier on head, git status is clean, so the pins are byte-identical. No solution, spec or result file is in the diff, so I didn't need a tiktoken recount.
  • Freeze tests: all 8 pass, plus TestVerificationResultsCoverAndMatchSources.
  • Lock, arity, drift and fuzz: TestProdFlipCriteriaLock is unchanged and passes. The #142 arity, drift and fuzz tests pass (TestArityTableCoversRegistry, TestIssue141*, TestOpcodeCapabilityDrift, TestCoverageMatrixDrift, TestCompareToCanonicalDetectsDrift).
  • Local checks: gofmt -l . is empty, go vet ./... exits 0 and go test ./... exits 0. No apps/* flake showed up this run.
  • CI: the build check is green.
  • Hard nos: no -compile-bc or HFIR default flip (#90 stays Partial), no 4d74dbc tip-lock, and no live-LLM or H1 claim.

Nits

  1. Narrow the difftest fence predicate and log it as a skip, as described above.
  2. File the pre-existing put-as-expression interpreter-vs-VM divergence.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

HFIR disagrees with bytecode on 8 of 35 held-out v3 programs HFIR miscompile: encode_json(parse_json s) prints raw s when followed by a let argument

1 participant