Repository navigation
HFIR parity: fix parse_json stack leak and map_get expression targets; HFIR in every verifier (#159, #155) - #160
Conversation
howlcipher
left a comment
There was a problem hiding this comment.
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 symbolfires only when the HFIR content edge is not asymbolwhose 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_textbody, a(str s "")expression body, a defun argument, a return value, insideif,cond/elseandfor(both as the iterable and in the body), as theletvalue followed by asetrebind (assigned twice), and under chainedmap_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
.howlfiles in the repo with-compile-hfir-bcon 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 -vreports 268 PASS subtests. - Mutation check: I temporarily restored base
bytecode.golocally 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/sleeprace (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 areuse-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.txtis 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 giveCAPABILITY_DENIEDwith 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 statusis 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:
TestProdFlipCriteriaLockis 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 andgo test ./...exits 0. No apps/* flake showed up this run. - CI: the
buildcheck is green. - Hard nos: no
-compile-bcor HFIR default flip (#90 stays Partial), no 4d74dbc tip-lock, and no live-LLM or H1 claim.
Nits
- Narrow the difftest fence predicate and log it as a skip, as described above.
- File the pre-existing
put-as-expression interpreter-vs-VM divergence.
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)
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 rawson base, and now prints the re-encoded JSON.Root causes
parse_jsonleaked 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_JSONreads its body by variable name. The AST compiler emits only that instruction, but the HFIR lowerer also compiled the content edge (aLOAD_VARof the same symbol). The stray raw string then got consumed by a later instruction:WRITE_FILEpopped it as the path. That's the falseCAPABILITY_DENIEDinside the grant: the write was checked against a JSON string, notout/....MAP_GETpopped it as the key (TYPE_ERROR map_get expected dict, got string).PRINTpopped it (HFIR miscompile: encode_json(parse_json s) prints raw s when followed by a let argument #155).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.map_getwith an expression dict had no HFIR shape (x10, x11).(map_get (map_get t "meta") "tags")fell through to the generic node and failed withmap_get requires a target name and key. Fix: lower it withtargetandkeyedges and emit the AST compiler's exact sequence, ending inMAP_GETwith an empty variable operand.Fail-closed: the capability fix widens nothing. The runtime check is untouched, and the program now hands
WRITE_FILEthe real path.TestHFIRParseJSONWriteFileStaysFailClosedchecks 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/TestHFIRBenchmarkSolutionParityreplays all 268 benchmark solutions on all 3 paths in fresh sandboxes. It runs ingo test ./..., so any mismatch fails thebuildcheck.experiments/internal/pathparityis shared by the heldout-v0/v1/v2/v3 verifiers (which also cover postcf/postrec through-howl-dir) andtokverify(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, soTestProdFlipCriteriaLockstays unchanged. A newTestHFIRRegressionParityuses the fixtures intests/hfir_parity/.internal/hfir/issue159_test.go: noPARSE_JSONbody leak (instruction stream equals the AST compiler's), non-symbol content fails closed, and themap_getexpression target matches the AST compiler. All of them fail on base.Constraints
-compile-bcis untouched and there is no default flip. Write flagged http_server bytecode and stop #90 stays Partial, andTestProdFlipCriteriaLockis unchanged and passing.git statusshows noresults/change. Spec and results freeze tests pass.gofmt -l .is empty, andgo build ./...,go vet ./...andgo test ./...pass. The Arity, Drift, Fuzz and Lock tests pass.Not in scope / left open
keyedge formap_get, so it stays narrower and rejects the newtargetshape (fail closed). That's for roadmap item 2.tools/difftest'stest_env.howlinterpreter failure is environment-dependent and also fails on base.list_lenTYPE_ERROR). That's pre-existing, and no benchmark exercises it.