C5: execution receipt v0 (--receipt)

[howlcipher]

Summary

Implements review candidate C5: execution receipt v0 on top of C4b (#112 / 9360cbf0).

• New --receipt <path> on legacy -run-bc and howlframe run (bytecode/bc target, both .hfbc artifacts and in-process .howl compilation). --target interpreter / -run with --receipt is rejected.
• The Go runner writes the receipt (0600, temp file + rename) after execution and before os.Exit, on normal exit, CAPABILITY_DENIED, LIMIT_EXCEEDED, and other runtime failures. Program output is unchanged, and no opcode can reach the recorder, so print cannot forge a receipt.
• Without --receipt, behavior is unchanged (RunBytecodeWithPolicy path untouched; recorder is nil / no-op).

Schema howlframe.receipt/v0 (deterministic struct order, 2-space indent)

schema, artifact_sha256, compiler_version, grant[] (sorted), limits{max_instructions, max_call_depth, max_memory_bytes, max_fetch_body_bytes, max_exec_output_bytes, deadline_ms}, instructions_used, effects[{op, capability, target_summary, decision}], effects_truncated, exit{status, code, error|null}

• effects and grant are always [], never null. Effects are capped at 10000 entries (effects_truncated).
• artifact_sha256 is the sha256 of the artifact bytes that ran. For .howl it is the sha256 of the canonical serialized artifact.
• compiler_version is the runner's Version.
• Exit error messages keep the runner text only for LIMIT_EXCEEDED/CAPABILITY_DENIED. For other failure codes the message is generic, because host errors can contain URLs or SQL.

Redaction (target_summary, ≤256 bytes)

fetch → scheme://host[:port] (no userinfo/path/query/fragment) · env → variable name · read/write_file, mkdir → path · exec → argv0 basename · db_connect → driver (no DSN) · sql/store ops → handle/store name · http server → addr/route · model/LLM ops, res bodies → "".

Effects are recorded at each capability decision (allowed/denied), and SPAWN, HTTP-route, and SPAWN_AGENT children share the same recorder. Ambient ops (print, stderr, sleep, time_now, read_line, exit) are not recorded in v0.

Hard nos intact

No prod -compile-bc/HFIR flip; #90 stays Partial. No HFBC/opcode change and no change to the ExecutionEvidence sealing format. No DOM, no harness. C4a/C4b flags and behavior unchanged.

Deferrals

No signing or attestation of receipts. Not bound into sealed ExecutionEvidence. No AST interpreter receipt. Detached SPAWN goroutine effects that land after finalization are dropped.

Test plan

• gofmt -l . clean
• go vet ./...
• go test ./... -count=1 green (outside sandbox)
• internal/vm receipt tests (redaction, env/exec, denied, limit, empty/deterministic, spawn_agent, HTTP child, store, cap/finalization, concurrent recorder) with -race
• CLI TestReceiptCLI (forge/deny/limit across -run-bc and run, .hfbc and .howl, hash check, interpreter rejection, no file without flag) and TestReceiptWriteFailureCLI
• C4a/C4b CLI regressions (TestRunBytecodeMaxCallDepthFlag, TestRunBytecodeMaxInstructionsFlag, limits/deadline/memory tests)

[howlcipher]

Dev-lead COMMENT (Motoko) — head 97b8957c

Merge-ready for undraft + squash-merge (CI build green on Go 1.21).

Diff matches scope

• --receipt on -run-bc and run bytecode/bc (incl. in-process .howl); interpreter / -run reject nonempty receipt.
• Runner-written howlframe.receipt/v0: schema, artifact_sha256, compiler_version (runner Version), sorted grant, C4 limits + deadline_ms, instructions_used, redacted effects (cap 10k + truncated), exit.
• Writes on success and deny/limit/runtime failures via temp+rename 0600 before exit; nil recorder / empty path leaves RunBytecodeWithPolicy untouched.
• Unforgeable by program (print forge CLI regression); ambient print/sleep/etc omitted and documented.
• SPAWN / HTTP-route / SPAWN_AGENT share recorder; late post-finalize SPAWN effects dropped.

Hard nos intact

No prod HFIR/-compile-bc flip; #90 stays Partial; no HFBC/opcode change; no harness/DOM; C4a/C4b flags and enforce path preserved.

Deferrals acknowledged

No signing/attestation; no sealed ExecutionEvidence binding; no interpreter receipts; detached late SPAWN effects dropped — as scoped.

Doc skim (Codex status lines)

C5 status updates are honest (PARTIAL / v0 bytecode / signing open) in 00/02/06/07/08/11/FINAL_REPORT. Non-blocking: 05 termination cell and FINAL_REPORT P1 C4 row still read pre-C4b (“instruction count only” / “Planned (C4)”) — pre-existing vs #112, not a C5 overclaim.

Non-blockers

• Journal notes sandbox full-suite gaps (listener/EPERM); CI build green is the gate.
• Paths/env names/store URIs remain resource-level (documented, not PII wipe).

Left draft. Undraft + squash-merge when you are ready.