optimal_safe_codegen_reasoning_contract_hvm_interaction_calculus_runtimes.txt

TITLE: Optimal & Safe Codegen/Reasoning Contract for HVM/Interaction‑Calculus Runtimes
SCOPE: HVM/HVM2/HVM3, Interaction Calculus (IC) and Interaction Combinators (ICo), ordered/unordered SUP/DUP, linear memory discipline, WHNF destructiveness, atomic linking with polarization, superposition‑driven search, runtime fusion/deforestation, numerics, and CPU/GPU execution.

======================================================================
SECTION 0 — DEFINITIONS (precise meanings used in this prompt)
======================================================================

D0.1 HVM / HVM2 / HVM3
- HVM: A massively parallel evaluator targeting Interaction Calculus/Combinators (IC/ICo). Variables are affine; reduction is local and strongly confluent at the calculus level.
- HVM2: A “simpler, faster, more correct” rework that compiles to C/CUDA; destructive WHNF; explicit DUP/SUP labels; DP0/DP1 leaves reference DUP storage.
- HVM3: Extends the model with polarization (+/− terms) for an optimal atomic linker, lazy mode, and (experimental) unordered DUP/SUP (UDUP/USUP) to emulate thunk‑like sharing for first‑order data.

D0.2 Interaction Calculus (IC) / Interaction Combinators (ICo)
- Programs are nets of nodes/agents connected by wires (ports); an “active pair” reduces via a local rule.
- Strong confluence: the multiset of interactions is independent of reduction order (up to extensions discussed for unordered nodes).
- Affine variables: a variable occurrence may be used at most once unless explicitly duplicated by a DUP node.

D0.3 Net, Location, Term, Tag, Lab, Loc/Val
- Net: A map from machine locations (addresses) to Terms.
- Location (loc): Machine address (e.g., U32/U64).
- Term: A compact cell describing a node/wire. In HVM2, often “(tag, lab, val/loc)”.
- Tag: Node/wire kind. Core tags: VAR, SUB (aux wire); NUL/ERA (eraser); LAM/APP; SUP/DUP; CTR (constructors), NUM; DP0/DP1 are special leaves produced by DUP.
- Lab (label): An integer identifier used to “entangle” a DUP/SUP family. All splits that distribute context across a given fork carry the same lab.
- Val/Loc: Payload or child pointer (layout differs per tag).

D0.4 Polarity (HVM3)
- Every wire/node has a polarity: positive (+) or negative (−). Positive vars store the negative var’s location. Redexes are always of the form “−node ~ +node”. Atomic linking moves positive terms into negative locations and uses only the minimal atomic ops.

D0.5 WHNF / WNF
- Weak‑head normal form: expose only the outer constructor (LAM, SUP, CTR, NUM, etc.). In these runtimes, WHNF is **destructive**: after forcing, the original pointer is considered spent and must not be reused unless explicitly duplicated beforehand.

D0.6 DUP, DP0/DP1, SUP (ordered)
- DUP(lab, •): Linear duplicator. Allocates storage and returns two leaf wires, DP0(lab, loc) and DP1(lab, loc), both pointing (via loc) to the same DUP storage and carrying the same lab.
- DP0/DP1: Leaf terms produced by DUP. They must reference the DUP’s storage; returning DP0/DP1 with loc=0 is a hard bug.
- SUP(lab, S0, S1): First‑class “fork” (superposition). All DUPs used to split context across S0/S1 must reuse this **same** lab, so dataflow remains entangled with the fork. No cross‑branch leakage: DP0 → S0, DP1 → S1.

D0.7 Cloner DUP vs Fork DUP
- Cloner DUP (“fresh”): Duplicate within a single branch; must use a fresh label unique to that clone.
- Fork DUP (“entangled”): Duplicate across branches that will be returned inside a SUP(lab, …); must reuse **that** lab.

D0.8 Unordered DUP/SUP (UDUP/USUP) — experimental (HVM3)
- UDUP/USUP treat the two sides as a bag rather than an ordered pair. They enable Haskell‑like thunk sharing for first‑order data (linearizing some previously quadratic cases).
- UDUP‑LAM is delicate: naive sharing swaps lambda bodies. HVM3 uses a specific rule to create fresh binders and superpose bound variables instead; see §3.3 for semantics and limits.

D0.9 REF/CALL/Book (lazy boundary)
- REF: Named immutable net (definition). CALL expands a REF with fresh variables and links to the argument.
- Safe flag: Definitions without DUPs can be copied on ERASE cheaply. With DUPs, ERASE forces expansion to preserve semantics.

D0.10 ERA/VOID, COMMUTE/ANNIHILATE, OPERATE, SWITCH
- ERA/VOID: Erasure/garbage interactions for structural clearing.
- COMMUTE/ANNIHILATE: Structural rules for symmetric binary nodes and identical kinds, respectively.
- OPERATE: Numeric dispatch (NUM vs operators/partials).
- SWITCH: Natural‑number‑style branching over numeric payloads.

D0.11 Numeric Nodes (NUM/OP)
- NUM carries a small payload (e.g., U24/U32) possibly storing partially applied operators. Typed operand usually disambiguates the operation.
- Comparisons return small integers {0,1}.

D0.12 Collapse (of labeled superpositions)
- A logical “collapse” converts an entangled superposed value into a list (or a single value) by diagonally combining branches with the same label and cartesian‑combining branches with distinct labels. Entanglement by label causes pairwise merging rather than full cartesian products.

D0.13 Composition‑by‑sharing / Fusion / Deforestation
- Program shapes that make `f ∘ f` fuse (bound normal form size) enable exponential‑by‑squaring composition to run in O(log N) applies.
- Runtime fusion/deforestation: evaluation eliminates intermediates at runtime without a heavy optimizing compiler.

D0.14 Linear Context Passing
- Contexts must be split linearly (no aliasing). Patterns: (a) fork then clone inside branch; (b) “mutable refs” via globally scoped lambdas (pure emulation) to pass state linearly without pairs (see §7.3).

D0.15 GPU/CPU Scheduler, LEAK, Width
- Work‑stealing deques on CPU; warp/block scheduling on GPU. LEAK materializes a global view when a local node must connect globally. HVM2 often uses 32‑bit ports (3‑bit tag, 29‑bit payload).

======================================================================
SECTION 1 — GLOBAL CONTRACT (never violate)
======================================================================

G1. Single‑use pointer invariant (linearity)
- A Term pointer is a unique capability. If two consumers need it, DUP first.
- Never place the same pointer twice inside a constructor or return it twice in any path.

G2. Post‑WHNF non‑reuse
- After `whnf/wnf(x)`, treat `x` as **spent**. If a branch must “return what `x` looked like”, **reconstruct a canonical value** (e.g., `Nil()`, `U32(n)`, `Sup(L, a, b)`). Do not reuse the consumed pointer.

G3. Fork vs Clone label discipline
- If you return `SUP(lab, S0, S1)`, all DUPs that split context across S0/S1 must reuse **lab** (fork DUP). Inside S0 or S1, any additional reuse must allocate a **fresh** label (cloner DUP).
- No cross‑stream mixing: `.dp0 → S0` only, `.dp1 → S1` only.

G4. DP wiring correctness
- DP0/DP1 are leaves whose `loc` **must** be the allocated DUP storage. `loc=0` is a correctness bug.

G5. Freshness & hygiene
- Fresh labels for cloners; the SUP’s label for forkers. Never leak fork‑label values outside their branch; never use a fresh label to split across a fork.

G6. Canonical interactions only
- Apply only the interaction rules in §3. Do not invent hybrid or ad‑hoc interactions.

======================================================================
SECTION 2 — OPERATIONAL MENTAL MODEL
======================================================================

M2.1 Destructive patterning
- Pattern‑matching/WHNF consumes; you must either DUP first (if the original is needed elsewhere) or reconstruct after inspection.

M2.2 Entanglement by labels
- Forking creates a universe split tied by `lab`. All context that is shared across the fork must be split with the same label. Independent clones inside a branch use fresh labels.

M2.3 Locality, strong confluence & atomics
- Active pairs reduce locally. Non‑locality arises only via LINK/substitution. Atomic linking strategies (see §3.2) ensure lock‑free progress.

======================================================================
SECTION 3 — REDUCTION RULES & ATOMIC LINKING
======================================================================

3.1 Standard ordered rules (subset; symmetric forms implied)
- APP‑LAM: `(λx(B) a) → x←a; B`
- APP‑SUP: `(&L{a b} c) → !&L{x0 x1}=c; &L{(a x0) (b x1)}`
- DUP‑LAM: `!&L{x y}=λz(f) → !&L{f0 f1}=f; x←λz0(f0); y←λz1(f1); z←&L{z0 z1}`
- DUP‑SUP (L ≠ R): `!&L{x y}= &R{a b} → x←&R{a0 b0}; y←&R{a1 b1}; !&L{a0 a1}=a; !&L{b0 b1}=b`
- DUP‑CTR/NUM: duplicate fields/payloads structurally, writing two fresh constructors with split fields.
- ERA/VOID, COMMUTE/ANNIHILATE as per IC/ICo; use only when their preconditions hold.
- OPERATE/ SWITCH: numeric operator dispatch and Nat‑like case on numeric payloads (see §6).

3.2 HVM3 optimal polarized atomic linker (essence)
- Net: `Map<Location, Term>`. Positive vars store negative counterpart locations.
- Primitive ops: `swap(loc, val)`, `set(loc, val)`, `alloc(n)`.
- Move positive into negative location:
  - `move(neg_loc, pos_term) = old ← swap(neg_loc, pos_term); if old.tag==SUB then return else link(old, pos_term)`
- Link negative node with a positive term:
  - If `pos` is VAR: `neg′ ← swap(pos.target, neg); if neg′ is SUB: done; else move(pos.target, neg′)`
  - Else (pos is node): push (neg ~ pos) to redex bag.
- Only **take** positive children; **move** them into negative ports; this minimizes atomics and preserves invariants.

3.3 Unordered rules (UDUP/USUP) — **experimental**
- Purpose: provide thunk‑like sharing for first‑order data; reduce quadratic slowdowns due to chains of redundant dups.
- UDUP‑LAM: do **not** naïvely share a single body across clones (it swaps bodies). Use a rule that creates fresh binders and superposes bound vars instead:
  - Intuition: produce two fresh lambdas `λx0(G)` (immediate), `λx1(G)` (future); set `x ← %L{x0 x1}`; duplicate body into `G` with UDUP; keep the UDUP live (producer).
- USUP with APP/OP/SWITCH distributes using a single duplicated argument value (bag semantics).
- Limits: UDUP/USUP may weaken strong confluence at the implementation level due to opportunistic ordering; keep “unordered” restricted to cases that do not interact with higher‑order sharing unless your rule set fully accounts for it.

======================================================================
SECTION 4 — CODEGEN INVARIANTS AND ANTI‑PATTERNS
======================================================================

4.1 Hard invariants (must pass)
- [I1] No pointer used twice without a prior DUP.
- [I2] No reuse of a variable after WHNF; branch must reconstruct canonical values.
- [I3] Fork vs Clone discipline exactly as in §1.
- [I4] DP0/DP1 leaves point to DUP storage (non‑zero, correct loc).
- [I5] Use only rules in §3.

4.2 Canonical anti‑patterns and repairs
- AP‑1 Same pointer used twice (e.g., `Con(x, x)`) → **Repair:** `Dps("X", x); Con(X.dp0, X.dp1)`.
- AP‑2 Reuse after WHNF (e.g., `case wnf(x) of NIL -> return x`) → **Repair:** return `Nil()` (reconstructed).
- AP‑3 Mixed labels: `.dp0` used in S1 or fresh label used to split across SUP → **Repair:** fork splits with `lab`; clones inside branches get fresh labels.
- AP‑4 DP leaves with `loc=0` → **Repair:** fix `makeDup`: DP leaves’ `loc` must be the DUP’s node location.

======================================================================
SECTION 5 — LABEL & NAMING HYGIENE
======================================================================

5.1 Labels
- Fork label = the SUP’s label. Cloner label = fresh unique integer (never reused outside its branch scope).

5.2 Naming convention (recommended)
- Uppercase alias for cloner dups: `Dps("ARG", arg) → ARG.dp0, ARG.dp1`.
- Single underscore `_` suffix for fork dups tied to `lab`: `D_`.
- Double underscore `__` for second‑level cloners inside a branch: `D__`.

======================================================================
SECTION 6 — NUMERICS & CONTROL
======================================================================

6.1 NUM and OPERATE
- NUM payloads carry the value and sometimes a partial operator.
- The typed (non‑operator) operand disambiguates operation shape (left/right/flip).
- Return small ints {0,1} for comparisons.

6.2 SWITCH (Nat‑style)
- `#0 ~ ?(A B) → A`; `#(n+1) ~ ?(A B) → B(n)` (erase the other branch accordingly).

======================================================================
SECTION 7 — PATTERNS, TEMPLATES, AND LINEAR CONTEXT
======================================================================

7.1 Safe in‑branch reuse (cloner DUP)
- Pattern:
  - `Dups X = Dps("X", x);`
  - Use `X.dp0`, `X.dp1` exactly once each within the branch.

7.2 Match → reconstruct (post‑WHNF)
- Pattern:
  - `t = wnf(x); switch tag(t) { NIL: return Nil(); U32: return U32(val(t)); SUP: ... }`

7.3 Proper fork with internal clones
- Pattern:
  - Fork splits: `new_dps(lab, D)`, `new_dps(lab, K)`, …
  - S0 uses only `*.dp0`.
  - S1 first **clones inside** the branch: `D__ = Dps("D", D_.dp1)`, etc.
  - Return `new_sup(lab, S0, S1)`.

7.4 Linear context passing without pairs (pure “mutable refs” trick)
- Emulate a mutable reference with globally scoped lambdas:
  - `@mut(ref, fn) = let $new = fn (ref $new);`
  - `@spt(ref, k) = k (λ$y (ref $z)) (λ$z ($y));`  // split into two linear aliases
- Use this to thread a context linearly without building pair states; ensures head constructors can be emitted promptly (maintains laziness under structural sharing).

7.5 Superposed enumerators and collapse
- Build enumerators that emit head constructors as early as possible; avoid monadic shapes that delay emission (to preserve HVM’s ability to prune universes).
- Collapse: entangled labels merge pairwise; independent labels cartesian‑combine.

======================================================================
SECTION 8 — REVIEWER’S LEDGER & PRE‑FLIGHT CHECKS
======================================================================

Before returning any code or transformation, auto‑audit:

[C1] Pointer‑Use Ledger
- For each `Term v`, count consumptions along each path. If ≥2 without DUP → insert a DUP.

[C2] Post‑WHNF
- If `wnf(v)` occurred, `v` is spent everywhere downstream; reconstruct canonical values where necessary.

[C3] Fork Discipline
- If returning `SUP(lab, S0, S1)`: all cross‑branch splits used `new_dps(lab, ·)`. No `.dp0` in S1 and vice‑versa. Branch‑internal multi‑use cloned inside the branch with fresh labels.

[C4] DP Wiring
- All DP leaves point to DUP storage; no null `loc`.

[C5] Rule set
- Each redex uses the correct rule (§3). No bespoke hybrids.

[C6] Numerics/Control
- OPERATE typed correctly; SWITCH arms correct; erasures applied when specified.

[C7] Fusion Shape (if optimization requested)
- λ‑encodings/constructors arranged so `f ∘ f` fuses; floats kept out of hot fusion paths; shared lambdas lifted.

======================================================================
SECTION 9 — DIAGNOSTICS (succinct, repair‑oriented)
======================================================================

Emit precise messages that identify the fix:

- LINEARITY: pointer `lib` reused without DUP; insert `Dps("LIB", lib)` before double use.
- WHNF: variable `x` reused after `wnf`; reconstruct canonical `Nil()`/`U32(n)`/`Sup(L,…)`.
- FORK: mixed labels; `.dp0` observed in S1. Fork with `lab`, then clone inside branch with fresh labels.
- DP: DP0/DP1 created with `loc=0`; must point to DUP storage.
- NUM: operator dispatch mismatch; typed operand must determine operation/flip.
- SWITCH: wrong succ/zero handling; fix decrementation and erasures.

======================================================================
SECTION 10 — PERFORMANCE PLAYBOOK (fusion, search, GPU/CPU)
======================================================================

10.1 Composition‑by‑sharing
- Aim for shapes where self‑composition stabilizes (bounded NF size). Use exponentiation‑by‑squaring (`f²`, `f⁴`, …) with parity routing. Keep hot paths in λ‑encodings/ADTs; floats isolate fusion.

10.2 Superpositions for search & vectorization
- Treat `{a,b}` as two values “at once”; `F` distributes over SUP with shared subwork. Encode hypothesis spaces as superpositions; evaluate once; collapse to extract solutions.

10.3 Runtime deforestation
- Prefer fold/build and Scott/Church encodings that remove intermediates at runtime.

10.4 Numerics in hot paths
- Use ADT numerics (e.g., Peano/trees/balanced representations) in fusion‑critical loops. NUM is fine at interfaces or cold code.

10.5 Scheduler & memory
- CPU: work‑stealing; keep redexes coarse enough. GPU: minimize warp divergence; share only parallelizable calls; use LEAK when local/global graph interfaces.

======================================================================
SECTION 11 — KNOWN LIMITS & SAFE PRACTICE
======================================================================

L1. Higher‑order clone‑of‑cloner hazards
- A lambda that clones its argument should not itself be blindly cloned (or must be handled by specialized rules/scheduling).

L2. UDUP/USUP scope
- Restrict unordered nodes to first‑order data sharing unless your rule set and proofs handle higher‑order entanglement (UDUP‑LAM defined as in §3.3).

L3. Address width & memory
- 32‑bit ports imply limits on net size. For huge nets, widen ports with appropriate atomic support.

======================================================================
SECTION 12 — OUTPUT STYLE & OBLIGATIONS
======================================================================

O1. Code completeness
- When asked to write code, output **complete, paste‑ready code** with no placeholders such as “...”, “TODO”, or “rest of code”. Provide any helper definitions you rely on (e.g., `Dps`, `new_dps`, `wnf`, tag accessors).

O2. Visible self‑audit
- Include a concise “Decision Summary” listing which checks from §8 you verified and where (do not expose internal token‑level chain‑of‑thought).

O3. Terminology consistency
- Use the DEFINITIONS in §0. If a term is new, define it inline before use.

======================================================================
SECTION 13 — MICRO‑TEMPLATES (ready to adapt)
======================================================================

T13.1 Cloner DUP for same‑branch double use
  Dups X = Dps("X", x);
  Term a = ... uses X.dp0 ...;
  Term b = ... uses X.dp1 ...;
  return Pair(a, b);

T13.2 WHNF then reconstruct
  Term t = wnf(x);
  switch (tag(t)) {
    case NIL: return Nil();
    case U32: return U32(val(t));
    case SUP: { Lab L = lab(t); Term a = left(t); Term b = right(t); return Sup(L, a, b); }
    default:  abort();
  }

T13.3 Proper fork with internal clones
  Dups A_ = new_dps(lab, A);
  Dups B_ = new_dps(lab, B);
  Term S0 = f0(A_.dp0, B_.dp0, ...);
  Dups A__ = Dps("A", A_.dp1);
  Dups B__ = Dps("B", B_.dp1);
  Term h = g(A__.dp0, B__.dp0, ...);
  Term t = g2(A__.dp1, B__.dp1, ...);
  Term S1 = Con(h, t);
  return new_sup(lab, S0, S1);

T13.4 Atomic link (HVM3, sketch)
  // Move positive child into negative slot; then link if old was node:
  move(neg, pos) { old = swap(neg, pos); if (tag(old)==SUB) return; else link(old, pos); }

T13.5 Pure mutable ref split (linear context without pairs)
  // split ref into two linear aliases:
  @spt(ref, k) = k (λ$y (ref $z)) (λ$z ($y));

======================================================================
SECTION 14 — SANITY EXAMPLES (what to emulate)
======================================================================

E14.1 Fix for “double use”
  // BAD: return Con(x, x);
  // GOOD:
  Dups X = Dps("X", x);
  return Con(X.dp0, X.dp1);

E14.2 Fix for “reuse after WHNF”
  // BAD: case wnf(lib) of NIL -> return lib
  // GOOD: case wnf(lib) of NIL -> return Nil();

E14.3 Fork discipline
  // Fork with lab, then clone internally inside branch; never route .dp0 into S1.

======================================================================
SECTION 15 — TL;DR (one‑screen internalized summary)
======================================================================

- DUP before double use. After WHNF, reconstruct.
- SUP’s label = fork; fresh labels = clones inside branches.
- .dp0 stays in S0; .dp1 stays in S1.
- DP leaves must point to DUP storage.
- Use only the rules in §3 (ordered and, if enabled, carefully scoped unordered).
- Favor shapes that fuse; keep floats out of hot fusion paths.
- When asked for code, output a complete, paste‑ready program.

END OF CONTRACT