Core implementation — current architecture

Summary: BANG has one graded-CBPV semantic core observed through several representations. The source oracle defines behavior; the calculated machine is the executable compiler specification; Wasm 3.0 is the target; each arrow carries its own proof or differential-test status.

Read this page to answer three questions:

1. Which representation or engine am I looking at?
2. What evidence connects it to the source meaning?
3. Which tier owns a change, and what may that tier import?

Architecture decisions remain authoritative: ADR-0016 fixes the two-hop shape, ADR-0059 revises the product target to Wasm 3.0, ADR-0110 preserves the abstract-model to concrete-emitter evidence boundary, and ADR-0035 separates source equivalence from compilation simulation.

1. One meaning, several representations

Reading the diagram: each edge label is the serialized evidence label followed by the serialized method; labels do not imply a stronger status.

The namespace Wasmfx survives in the formal Lean model for historical reasons. The model is a project-defined Wasm-oriented abstract machine: the checked compile_forward_sim theorem targets its Wasmfx.run, not the concrete WAT emitter or official Wasm semantics. Wasmfx.run returns Option Wasmfx.Val: only a singleton successful final value is some, and its neutral none does not classify fuel, stack-shape, handler-state, or unhandled-operation non-values using the source evaluator's Result. ADR-0059 separately makes stock Wasm 3.0 the product target through the concrete emitter, whose real-engine edge is differentially tested. A formal correspondence between those two target layers remains open; WasmFX is only a future fast path for the post-v1 general-resumption slot.

Architecture assertions

Generated from validated committed architecture and proof facts. The JSON is the consumer seam; source checks remain in the fact producers.

2. Proof arrows are different claims

Do not describe compiler correctness as “the Benton–Hur LR.” The LR and simulation are complementary, not interchangeable; ADR-0035 is the decision record.

Audited theorem census

Census: 33 enrolled theorems · 27 trusted · 6 flagged · 2 with no axioms.

Semantic inventory: 17 strong scoped claims · 3 structural · 2 bounded · 3 partial · 1 conjectural · 1 placeholder · 6 aliases. Alias and placeholder rows never increase the strong count.

Strong, precisely scoped claims: Bang.seq_unit, Bang.compile_forward_sim, Bang.compile_forward_sim_pure, Bang.source_eval_to_exec, Bang.Rung5ProofGrade.s5_exec_wexec_lockstep, Bang.subst_value, Bang.preservation, Bang.progress, Bang.type_safety, Bang.no_accidental_handling, Bang.no_accidental_handling_custom, Bang.closed_fully_handled_program_no_unclassified_stuck, Bang.CalcVM.compile_correct, Bang.CalcVM.evalD_agrees_source, Bang.CalcVM.sim, Bang.CalcVM.run_evalD, Bang.EnvMachine.evalE_agrees_evalD.

Live validator: python3 tools/docfacts_proof.py --live-check.

Axiom trust and semantic strength are independent axes. trusted means only that the kernel-reported axiom set is within the reviewed trusted set; it is not a generic product-level proven badge.

3. C4 component dependencies

The useful architecture zoom is the component level: repository tiers such as Frontend, Core, and Backend. Individual Lean modules are code-level detail—kept exact in the serialized fact, but intentionally omitted from the visual.

The dependency V still points inward at Core even though program data flows Frontend → Core → Backend. tools/import_facts.py is the single parser/classifier; tools/arch-check.py enforces the V. Unknown tiers and missing internal imports fail rather than silently falling into a default component.

BANG uses the C4 abstraction hierarchy to choose a useful zoom level for this page:

A C4 component is related functionality behind a defined interface and is not separately deployable. That matches these tiers better than C4's application/data-store container term.

Reading the diagram: arrows are dependencies between C4 components; edge labels aggregate the 69 code-level imports that cross a component boundary. Internal module-to-module imports are deliberately omitted from the visual.

The generated graph reports aggregate direct imports that cross component boundaries. It shows coupling pressure; it does not by itself prove semantic correctness or justify moving code.

4. Contributor routing

5. Current boundary versus horizon

• Current: v1 handlers are abortive or one-shot tail-resumptive; stock Wasm 3.0 exceptions, tail calls, GC values, and the tested concrete emitter are sufficient for the shipped path.
• Post-v1 horizon: general/multishot resumptions may use the GC-frame-chain slot, with WasmFX as a swappable fast path once standardized and deployed.
• Separate laboratory: Bang/Reify/ studies calculated handler machines; it is not another production execution path.
• Volatile project position: read repository-local CONTEXT.md in a checkout. This page intentionally contains no active-branch, checkpoint, or issue-status narrative.

6. Gates

python3 tools/import_facts.py --self-test
python3 tools/arch-check.py
python3 tools/gen-import-graph.py --check
python3 tools/check-architecture-assertions.py --check
just fitness

For theorem trust, run just axioms; for the full repository gate, run just verify from the Nix development shell.