Machine / backend role lab

This role lab is generated from the shared four-stage contract. Page identity, route, prerequisites, first-edit seams, and gates are manifest-owned; prose, checks, the fixture, and additional seams are content-owned.

Prerequisites

1. Retrieve and predict

Start from the existing Comp.binop constructor and its source meaning. Locate the constructor in Bang/Core/IR.lean, then the closed-integer reduction in Bang/Core/Semantics/Eval.lean. Predict the disposable program's observable value before running any engine. The task is to follow an existing calculation, not to propose an instruction or optimize it.

Retrieve:

Locate Comp.binop and BinOp.add in Bang/Core/IR.lean.
Locate the closed-integer Comp.binop arm in Bang/Core/Semantics/Eval.lean.
Locate evalD, compile, exec, and Agree in Bang/Backend/AbstractMachine.lean.

Predict before running:

Predict the value of 19 + 23 before running env, oracle, or compiled.
Predict whether compile/exec keeps an arithmetic instruction or collapses the closed operation to a return.
Predict whether the Wasm emitter supports integer addition or must refuse it loudly.

2. Trace the seam

Trace one constructor through linked owners. The kernel step defines source meaning; evalD is the state-explicit denotation from which compile and exec are calculated; Agree ties exec ∘ compile and Source.eval to one observable value. The Wasm emitter is a separate tested path from the same Comp: its emitComp arm emits supported arithmetic and its differential harness compares Wasmtime with the kernel oracle. The calculated machine remains an output of the calculation; this lab adds no instruction or semantic rule.

Checks:

Name the source step, evalD arm, compile arm, exec return behavior, and Agree observation without copying their bodies.
Explain why compile/exec constant-folding and direct Wasm arithmetic emission may differ internally while sharing the source result.
Explain how an explicit emitter refusal differs from an agreement failure or a silent skip.

Tracked seams:

3. Practise in isolation

Create the fixture below only in the disposable exact-HEAD clone. Materialize its expected output beside it, then run the same source through env, oracle, and compiled; each engine must match that one expected file. Run the existing Agree battery and, because integer addition is supported, the existing rung-1 emitter differential. Do not edit a production Lean file or add a new machine case. A refusal from a supported addition or any skipped engine is a failure.

Start from the clean, ready checkout used for the common journey. The project helper creates an independent full clone at its exact commit; all writes and gates below happen there.

set -euo pipefail
root="$(git rev-parse --show-toplevel)"
test -z "$(git -C "$root" status --porcelain)"
base="$(git -C "$root" rev-parse HEAD)"
parent="$(mktemp -d)"
lane="$parent/repo"
branch="practice/machine-backend-$(date +%s)-$$"
"$root/tools/new-worktree.sh" "$lane" "$branch" "$base"
cd "$lane"
practice="$lane/main.bang"
bundle="$parent/evidence"
mkdir "$bundle"
cat > "$practice" <<'BANG'
let main = 19 + 23
BANG

Run every step in order:

nix develop --command lake build bang
expected="$lane/expected.txt"
printf '42\n' > "$expected"
./.lake/build/bin/bang run --engine=env "$practice" > "$bundle/env.txt" && diff -u "$expected" "$bundle/env.txt"
./.lake/build/bin/bang run --engine=oracle "$practice" > "$bundle/oracle.txt" && diff -u "$expected" "$bundle/oracle.txt"
./.lake/build/bin/bang run --engine=compiled "$practice" > "$bundle/compiled.txt" && diff -u "$expected" "$bundle/compiled.txt"
nix develop --command just check Bang/Backend/AbstractMachine.lean > "$bundle/agree.txt" 2>&1
nix develop --command bash tools/emit-rung1-diff.sh > "$bundle/emitter.txt" 2>&1
nix develop --command just test-role-lab-machine-backend > "$bundle/harness.txt" 2>&1
cp "$practice" "$expected" "$bundle"
rm "$practice" "$expected"
test -z "$(git status --porcelain)"

Bounded outcome: The disposable source yields 42 under env, oracle, and compiled; the Agree battery elaborates; the supported addition sample emits and agrees with Wasmtime; cleanup leaves the exact-HEAD lane unchanged.

4. Inspect evidence and select live work

Keep the three engine outputs, Agree check, emitter report, source, and expected file as one evidence bundle outside the disposable clone. Agreement means all observations equal the committed expected value. Unsupported means the emitter returns and reports an explicit refusal; it never means a missing result or an unrun command. Select live backend work read-only only after naming the owning module and the smallest gate that can falsify a change on this seam.

Evidence checks:

Require env, oracle, and compiled to run exactly once and match the same expected file.
Confirm a deliberately wrong expected value would reject every captured engine output.
Require the AbstractMachine check to exercise the existing Agree battery.
Require the emitter report to include the supported integer-add sample, no refusal, and a Wasmtime/oracle agreement verdict.
Confirm no production Lean source changed and cleanup returned the exact-HEAD lane to a clean state.
Record the real narrow and full gate exit statuses; a skipped gate is not a pass.

Narrow gate:

nix develop --command just check Bang/Backend/AbstractMachine.lean

Full gate:

nix develop --command just verify

Read-only issue selection:

Run gh issue list --repo phibkro/bang --state open --search "backend OR CalcVM OR Wasm OR emitter"; set issue=<candidate-number> and inspect it with gh issue view "$issue" --repo phibkro/bang. Recommend one only after naming its owning module, semantic oracle, and smallest falsifying gate; do not claim, comment on, or mutate it.