Define lowered-HFIR ABI v1 and core conformance suite (#90 phase 1)

change_log.md

@@ -7,6 +7,7 @@
 * Locked the pure-versus-store capability split in docs and tests. `map_keys` grants nothing and runs under an empty grant. `store_keys` stays `database`. A `file://` store additionally requires `filesystem`. No opcode grant changed. Journal: `docs/journals/2026-09-30_capability_surface_honesty.md`.
 
 ### Added
+* Lowered-HFIR ABI v1 (`docs/reference/lowered_hfir_abi_v1.md`) and a conformance suite (`tests/conformance/lowered_hfir_abi_v1.json`) run by `tools/difftest` across the interpreter, the bytecode VM, Go, and JavaScript. The production compiler is still the AST bytecode path. Journal: `docs/journals/2026-09-30_lowered_hfir_abi_phase1.md`.
 * `html_escape` and `attr_escape`, with `HTML_ESCAPE` and `ATTR_ESCAPE`. Both
   encode `&`, `<`, `>`, `"`, and `'` the same way (`&amp;`, `&lt;`, `&gt;`,
   `&#34;`, `&#39;`) and grant no capability. `attr_escape` is the attribute-context

docs/hfir_execution_status.md

@@ -77,6 +77,12 @@ The existing HowlBoard backend compatibility suite passes against the baseline H
 
 Improvement #88 has a real but deliberately bounded execution destination: model-authored graphs that meet the Phase-1 schema can be verified and lowered directly to a deterministic artifact, while unsupported nodes fail closed. Before a broad adapter can replace `.howl`, HFIR still needs explicit semantic forms for functions, structured error recovery, iteration, opaque effect operations, and stronger graph/control-flow verification. Work on #88 is meaningful as constrained Phase-1 adapter design, but not as a claim that arbitrary model-authored HFIR can execute today.
 
+## Lowered ABI v1 (improvement #90, phase 1)
+
+`docs/reference/lowered_hfir_abi_v1.md` versions the contract the hosts must share (`lowered-hfir-abi/v1`). The conformance suite compares the interpreter, the bytecode VM, Go, and JavaScript on a pure core and on `env` denial. That comparison runs the production AST paths through `tools/difftest`. It does not switch `-compile-bc` over to `LowerToBytecode`.
+
+Wasm feasibility in this revision is the closed set `exec`, `spawn_agent`, and `http_server_start` (`HFIR_TARGET_INFEASIBLE`). Control edges are still unpopulated. Calls are still not executable HFIR. Phase 2 is the execution-path move. Journal: `docs/journals/2026-09-30_lowered_hfir_abi_phase1.md`.
+
 ## Provenance limitation
 
 HFIR-to-bytecode compile diagnostics retain the source filename, line, and column available on their semantic node. Existing runtime `VMError` values identify function, instruction offset, and opcode only; bytecode instructions do not yet carry HFIR provenance. This Phase 1 does not redesign the artifact source-map format.

docs/journals/2026-09-30_lowered_hfir_abi_phase1.md

@@ -0,0 +1,33 @@
+# Lowered HFIR ABI, phase 1
+
+## Why this slice
+
+Improvement #90 asks for one lowered contract so the interpreter, the bytecode VM, Go, JavaScript, and eventually Wasm mean the same thing. The production compiler does not consume HFIR. `runHFIRGate` verifies a graph, then `-compile-bc` calls `bytecode.CompileToBytecode` on the AST. `-compile-hfir-bc` is still the experimental lowerer. `LowerAST` still leaves `ControlEdges` empty.
+
+Shipping "HFIR owns execution" in this change would be a false Done. Phase 1 publishes the contract and proves the hosts that already run the core agree on it.
+
+## What landed
+
+`docs/reference/lowered_hfir_abi_v1.md` is version `lowered-hfir-abi/v1` (`hfir.LoweredABIV1`). It states typed values, the call shape the hosts already share, the absence of a linear-memory import, error classes, pure effects versus `env`, and the Wasm feasibility set.
+
+The Wasm set is exactly `exec`, `spawn_agent`, and `http_server_start`, rejected with `HFIR_TARGET_INFEASIBLE`. `isFeasible` reads `hfir.WasmInfeasibleKinds`. Other targets stay permissive. No Wasm opcode was added.
+
+`tests/conformance/lowered_hfir_abi_v1.json` is the suite. `tools/difftest` already compared bytecode, the interpreter, and Go, and it already knew how to run JavaScript for a `web_app`. The suite extends that harness. A `cli_app` body is rewritten to `web_app` only for the JavaScript host. Empty grants are explicit. Passing cases match normalized stdout. Rejections match one error class, exit nonzero, and print nothing.
+
+The core cases are exact integer arithmetic and `if`, `map_keys` including the #109 UTF-8 byte-order fixtures, `map_get` absence (#103), a dynamic `map_keys` `TYPE_ERROR` (#108), and `env` denial plus `env` granted. `map_keys` and `map_get` run with an empty grant (#107). A seeded property check generates eight arithmetic expressions and requires the same integer on every host. `defun`, `call`, and `while` stay in the existing `tests/parity` corpus for the AST hosts; `LowerToBytecode` still rejects them with `HFIR_BYTECODE_UNSUPPORTED`.
+
+## Phase 2
+
+One lowered graph is the source for every host.
+
+* `-compile-bc` still compiles the AST.
+* Calls and `while` are not executable HFIR.
+* Control edges are still empty, so the graph is not SSA.
+* Generated Go reads `env` with `os.Getenv` and does not deny a missing grant. JavaScript does not mediate `env`. The denial case therefore lists only the interpreter and the bytecode VM.
+* Feasibility is still a Wasm-only set of three host effects.
+* Non-exact `/` is not one rule.
+* #73 and #84 stay behind this ABI. This slice does not grow them.
+
+## What this does not do
+
+No new opcode. No language surface. No module linker, HFIR module graph, or VM module opcode. No Factory or supervisor work. #102–#109 are not reopened. Wasm SSA collections are not started.

docs/reference/lowered_hfir_abi_v1.md

@@ -0,0 +1,138 @@
+# Lowered HFIR backend ABI v1
+
+Version: `lowered-hfir-abi/v1`
+
+This is the contract a backend must meet for the deterministic core, and the shape a later lowering has to grow into. It is not a claim that HFIR owns execution. Production compilation is still the checked AST: `runHFIRGate`, then `bytecode.CompileToBytecode` (`-compile-bc`). `-compile-hfir-bc` remains the experimental research lowerer. Go, JavaScript, and the interpreter still consume the AST.
+
+The executable suite is `tests/conformance/lowered_hfir_abi_v1.json`, run by `tools/difftest`. The constant `hfir.LoweredABIV1` must match the manifest's `abi` field.
+
+## In scope for v1
+
+The suite runs one fixture on every applicable host and requires the same observable outcome.
+
+| Outcome | What must match |
+| --- | --- |
+| Pass | Normalized stdout, stderr, and process exit code |
+| Rejection | One error class, a nonzero exit, and empty stdout |
+
+Rejection exit codes do not have to be the same number. The bytecode VM exits 1. A generated Go panic exits 2. The class is the contract.
+
+Hosts for a `cli_app` body:
+
+| Host | How the suite reaches it |
+| --- | --- |
+| Bytecode VM | `-compile-bc` then `-run-bc`. Canonical result. |
+| Interpreter | `-run` |
+| Go | Default `cli_app` backend, then `go build` |
+| JavaScript | The same body with the root rewritten to `web_app`, then `node`, when `node` is on `PATH` |
+
+A missing `node` is `BACKEND_UNSUPPORTED` for that host only. A present `node` that disagrees is a failure.
+
+Wasm is not an execution host in v1. Its feasibility rule is the rejection set below. This revision does not add Wasm opcodes, collections, or host imports.
+
+### Values
+
+| Value | v1 rule |
+| --- | --- |
+| int | Signed integer. Printed with no decimal point when the value is a small exact integer. |
+| float | IEEE-754 binary64. The v1 suite does not use inexact floats. |
+| string | Unicode text compared and printed as UTF-8. |
+| bool | `true` or `false`. |
+| list | Ordered. An empty list is empty, not nil. |
+| dict | String keys. Values stay as stored. |
+| nil | The store-miss sentinel. Distinct from `""`. |
+
+### Pure operations
+
+These grant nothing. The suite runs them with an empty capability grant.
+
+* Arithmetic `+`, `-`, `*` on integers, and `/` only when the quotient is an exact integer (`(/ 20 4)` is `5`).
+* Comparisons and `if`.
+* `let` and `print`. `print` writes one line. Several arguments are separated by a single space.
+* `dict`, `map_get`, `map_keys`, `list`, `list_len`, `str_join`, `is_nil`.
+
+`(map_get dict key)` on a missing key is `""`. `is_nil` of that result is false. A present value is returned as stored. This is the #103 absence rule. `map_get` grants nothing.
+
+`(map_keys dict)` returns a list of strings in UTF-8 byte order (Go `sort.Strings`, Go string `<`). An empty dict is an empty list, so its length is `0`. A value that is not a dict fails at runtime with `TYPE_ERROR` and the text `map_keys expected dict`. `map_keys` grants nothing. The order, including keys outside the Basic Multilingual Plane, is the #109 rule. The suite replays `tests/fixtures/map_keys_sort_bmp.howl` and `tests/fixtures/map_keys_sort_nonbmp.howl`. Wasm does not emit `map_keys`; #73 must use this byte order if it ever does.
+
+Integer `/` is not one rule yet. The interpreter truncates `int64`. The bytecode VM divides `float64`. JavaScript divides IEEE numbers. Go uses the operand types it emitted. Exact quotients agree. Non-exact quotients are outside v1. Division by zero is already in `tests/parity/12_error_div_zero.howl` and normalizes to `DIVISION_BY_ZERO`.
+
+### Calls
+
+A `defun` has a name, a parameter list, optional `type_hints`, and a body. `return` leaves the function. `(call name arg ...)` passes arguments by position. The existing harness already compares that shape on the interpreter, the bytecode VM, and Go: `tests/parity/06_control_flow.howl` (`TestParityCorpus`).
+
+The experimental lowerer does not emit `defun`, `call`, or `while`. `LowerToBytecode` fails those graphs with `HFIR_BYTECODE_UNSUPPORTED` and no `BCProgram`. v1 does not move call execution onto HFIR.
+
+### Memory and runtime imports
+
+v1 defines no linear memory and no Wasm import table.
+
+Observability imports `print`, `stderr`, and `exit` grant nothing.
+
+Host effects are named by `capability.ForConstruct`. The v1 suite uses one of them: `(env "KEY")` requires `environment`. An empty grant denies it before the variable is read. The grant `environment` returns the value. File, network, process, and database imports stay on that same table and are not given new opcodes here.
+
+### Errors
+
+Backends may use different JSON. The suite compares the class from `tools/difftest.NormalizeError`.
+
+| Class | When |
+| --- | --- |
+| `TYPE_ERROR` | A pure operation rejects a wrong receiver, including `map_keys` on a non-dict. |
+| `CAPABILITY_DENIED` | A host effect runs without its grant. |
+| `DIVISION_BY_ZERO` | Division by zero. |
+| `HFIR_TARGET_INFEASIBLE` | A target cannot execute a construct. Diagnostic contract `v1`. |
+| `HFIR_BYTECODE_UNSUPPORTED` | The experimental lowerer is given a node outside its executable subset. No partial program. |
+
+`map_keys` of a list literal is a checker diagnostic (`map_keys target must be dict, got list`) and never reaches the runtime. The runtime class is locked with a dynamically typed receiver, the same shape as `internal/vm/collection_type_test.go`.
+
+### Effects and capability boundaries
+
+Pure operations declare no capability. `map_keys` and `map_get` stay pure (#107). `store_keys` stays `database`, and a `file://` store also requires `filesystem`. v1 does not change that split.
+
+`env` is the negative capability case. The suite binds it with `let` and prints the binding. With no grant, the interpreter and the bytecode VM both reject with `CAPABILITY_DENIED`, exit nonzero, write no stdout, and do not include the secret value. With the `environment` grant, those two hosts and the Go backend print the value. The Go backend emits `os.Getenv` for that `let` binding.
+
+Generated Go does not consult the capability grant. Generated JavaScript has no `env` form. Those hosts are not conformance targets for the denial case. Putting them on that case is allowed only once they reject with `CAPABILITY_DENIED` and do not reveal the value.
+
+### Feasibility
+
+`isFeasible` rejects a closed set for target `wasm`, and only that target:
+
+* `exec`
+* `spawn_agent`
+* `http_server_start`
+
+The diagnostic is `HFIR_TARGET_INFEASIBLE`. The same kinds are not rejected for `bytecode`, `interpreter`, `go`, `javascript`, or the empty `-validate` target. `hfir.WasmInfeasibleKinds` is that set. Adding a kind, or rejecting a v1 pure kind such as `map_keys` or `print`, changes this contract.
+
+Bytecode construct support stays on `hfir.VerifyConstructs` over the AST (`internal/construct`), which also emits `HFIR_TARGET_INFEASIBLE`. That scan is unchanged.
+
+Other targets do not yet share one feasibility table. A passing verifier result for `go` or `javascript` does not mean the effect is implemented there.
+
+### CFG and SSA
+
+A later lowering that owns meaning has to be a typed CFG in SSA:
+
+* Blocks end in a jump, a conditional branch, or a return.
+* Each value is assigned once.
+* Data edges name operand roles (`key`, `value`, `body`, and so on).
+* Control edges connect blocks.
+* Node kinds are constructs, not user binding names.
+
+`hfir.LowerAST` is not that form. It fills data edges for the semantic subset and leaves `ControlEdges` empty on every node, including the v1 arithmetic fixture. Kinds outside `lowerSemanticList` still come from the list head, so a user name can appear as a kind. v1 records that fact. It does not pretend the graph is SSA.
+
+## Deferred (Phase 2)
+
+Phase 2 is one lowered graph consumed by every host, with identical outcomes or the same feasibility rejection.
+
+* Production `-compile-bc` still compiles the AST. Flipping that path is Phase 2.
+* `defun`, `call`, and `while` become executable HFIR, or every host rejects them with one code. Today the hosts run them and the experimental lowerer rejects them.
+* `ControlEdges` are populated and the graph is SSA.
+* Go and JavaScript mediate capabilities the way the interpreter and the bytecode VM do.
+* One feasibility table covers every target, not only the three Wasm host effects.
+* Non-exact integer division picks one rule.
+* Wasm collections (#73) and `for` / `match` / `try_let` / `spawn` SSA lowering (#84) target this ABI. They are not part of v1, and this revision does not grow them.
+* No bytecode module linker, no HFIR module graph, no VM module opcode (#106).
+* No new Frame opcode and no new capability.
+
+## What the suite does not prove
+
+Agreement among the AST backends is not proof that HFIR is the source of that agreement. `internal/vm/hfir_equivalence_test.go` is separate evidence that the experimental lowerer matches the bytecode VM on the subset it already emits, including `map_keys` and a granted `env`. That test is not the production compiler.