hyperpolymath
diff --git a/‎.gitignore‎
Lines changed: 2 additions & 0 deletions b/‎.gitignore‎
Lines changed: 2 additions & 0 deletions
diff --git a/‎.machine_readable/6a2/META.a2ml‎
Lines changed: 193 additions & 0 deletions b/‎.machine_readable/6a2/META.a2ml‎
Lines changed: 193 additions & 0 deletions
diff --git a/‎.machine_readable/6a2/STATE.a2ml‎
Lines changed: 153 additions & 6 deletions b/‎.machine_readable/6a2/STATE.a2ml‎
Lines changed: 153 additions & 6 deletions
@@ -16,6 +16,8 @@ Thumbs.db
 /build/
 /dist/
 /out/
+# Idris2 build artifacts (nested, e.g. under formal-verification dirs)
+**/solo-core/build/
 
 # Dependencies
 /node_modules/
 
@@ -7,3 +7,196 @@ project = "affinescript"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "PMPL-1.0-or-later"
 standard = "RSR 2026"
+
+# ──────────────────────────────────────────────────────────────────────────────
+# Architecture Decision Records
+# ──────────────────────────────────────────────────────────────────────────────
+# ADRs are numbered sequentially and never renumbered. Superseded ADRs remain
+# in place with status = "superseded" and a pointer to the replacement.
+# Added 2026-04-10 during Track F1 (Idris2 Solo-core formalisation) — the
+# formal-verification track surfaced three decisions about the QTT type system
+# that were previously implicit.
+
+[[adr]]
+id = "ADR-001"
+status = "accepted"
+date = "2026-04-10"
+title = "Split-Γ is the canonical presentation of the QTT type system"
+context = """
+The Idris2 Solo-core formalisation (docs/academic/formal-verification/solo-core/)
+revealed that docs/spec.md §3.6 presents typing rules against a shared Γ
+(writing e.g. T-App with both premises typed under the same Γ), while
+lib/quantity.ml runs a post-hoc usage walk that accumulates per-variable
+usage summed across subterms. The literature-standard QTT presentation
+(Atkey 2018, Granule, Idris2 core) uses explicit context splitting
+  Γ = Γ₁ + q·Γ₂
+at every eliminator position.
+
+Both forms are extensionally equivalent for the Solo core (same programs
+accepted/rejected). The difference is purely presentational.
+"""
+decision = """
+Split-Γ is canonical. The spec, the formalisation, and all future
+documentation present typing rules in split-Γ form. The post-hoc usage walk
+in lib/quantity.ml is an equivalent implementation strategy, documented as
+such in a comment, not the definition of the type system.
+"""
+consequences = """
+- docs/spec.md §3.6 is rewritten to show explicit context splitting (~30-60 LOC).
+- lib/quantity.ml gets a header comment explaining that its flat walk is an
+  equivalent implementation of the split-Γ rules, with a pointer to this ADR.
+- The Idris2 formalisation's Typing.idr (which uses split-Γ) becomes the
+  mechanised witness of the spec — no translation layer required.
+- Progress + preservation proofs can proceed in textbook form.
+- Dependability gain: one source of truth. The spec-vs-impl gap (the failure
+  mode flagged in Track B's audit of TYPECHECKER-COMPLETION.md) cannot
+  structurally hide in this part of the system.
+- Interop gain: the spec becomes citable and legible to anyone with QTT
+  background (Atkey, Idris2, Granule, Quill readers).
+- Reader-tax cost: split-Γ notation is heavier than shared-Γ for newcomers.
+  Mitigated by surface-language tutorials keeping informal shared-Γ intuition
+  while the spec remains the formal reference.
+"""
+
+[[adr]]
+id = "ADR-002"
+status = "accepted"
+date = "2026-04-10"
+title = "Let rule scales value context by binder quantity (QTT-orthodox)"
+context = """
+During the Decision-2 audit of docs/spec.md T-Let against lib/typecheck.ml
+and lib/quantity.ml, the current implementation was found to handle Let
+unsoundly:
+
+- lib/typecheck.ml:631-665 (ExprLet) does zero quantity handling — pure
+  HM-style inference with let-generalisation, quantities entirely absent.
+- lib/quantity.ml:251-253 (ExprLet in infer_usage_expr) does a flat walk
+  that sums e1's and e2's usages without scaling e1 by the binder's quantity.
+
+This is equivalent to the rule
+  Γ₁ ⊢ e1 : A    (Γ₂, x:A) ⊢ e2 : B
+  ─────────────────────────────────
+            Γ₁ + Γ₂ ⊢ let x = e1 in e2 : B
+rather than the QTT-orthodox
+  Γ₁ ⊢ e1 : A    (Γ₂, x:^q A) ⊢ e2 : B
+  ─────────────────────────────────────
+         q·Γ₁ + Γ₂ ⊢ let x :^q = e1 in e2 : B
+
+Two concrete soundness bugs follow:
+
+BUG-001 (high severity — linear-value smuggling):
+  let x :ω = linear_resource() in use_x_once(x)
+  Current impl accepts; QTT-correct form rejects (e1's Γ must be scaled by
+  ω, so any Γ₁ containing a linear variable becomes ill-formed).
+
+BUG-002 (medium severity — erasure failure):
+  let x :0 = expensive_proof_term() in body_not_using_x
+  Current impl evaluates e1 and consumes its resources; QTT-correct form
+  scales e1's Γ by 0, producing the zero context, which means e1 can be
+  erased at runtime.
+
+BUG-001 is a soundness hole that defeats the point of affine types in any
+program where ω-binders and linear values coexist.
+"""
+decision = """
+The Let rule in both the spec and the implementation scales the value
+context by the binder's quantity. T-Let becomes:
+
+  Γ₁ ⊢ e1 : A    (Γ₂, x:^q A) ⊢ e2 : B
+  ─────────────────────────────────────
+         q·Γ₁ + Γ₂ ⊢ let x :^q = e1 in e2 : B
+
+Unannotated Let defaults to q = ω (matching current behaviour for all
+existing unannotated code — so the fix is non-breaking for the common case).
+"""
+consequences = """
+- lib/quantity.ml ExprLet case grows a scale-by-q step before summing
+  into the outer context (~10 LOC).
+- lib/typecheck.ml ExprLet case threads quantities (folded into Track A3
+  which is already rewriting quantity flow through typecheck.ml).
+- docs/spec.md T-Let rule is rewritten to show the scaling explicitly.
+- Two regression tests added as Track A2 fixtures covering BUG-001 and
+  BUG-002.
+- The Idris2 formalisation (Typing.idr THLet) already assumes the scaled
+  form — no rework there.
+- Users who had previously (accidentally) relied on the unsound behaviour
+  to duplicate linear values through ω-lets will now get a compile error.
+  Expected blast radius: near-zero because affine enforcement was never
+  wired in the first place (see ADR-001 rationale).
+"""
+
+[[adr]]
+id = "ADR-003"
+status = "accepted"
+date = "2026-04-10"
+title = "Evaluation order is strict CBV, left-to-right, for all n-ary forms"
+context = """
+During the Decision-3 audit of lib/interp.ml for the Track F1 Step relation,
+the evaluator was found to be internally inconsistent about evaluation order
+of n-ary expression forms.
+
+- ExprBinary (lib/interp.ml:135-138) is explicitly left-to-right:
+    let* left_val = eval env left in
+    let* right_val = eval env right in
+    eval_binop op left_val right_val
+- ExprApp args (:130), ExprTuple (:144), ExprArray (:148) all delegate to
+  eval_list, which is implemented with List.fold_right:
+    and eval_list env exprs =
+      List.fold_right (fun expr acc ->
+        let* vals = acc in
+        let* v = eval env expr in
+        Ok (v :: vals)
+      ) exprs (Ok [])
+  OCaml is strict, so in f (fold_right f [a;b;c] init) the innermost
+  application runs first — eval env c is forced before eval env b before
+  eval env a. Net result: right-to-left.
+
+This was almost certainly unintentional; nothing currently depends on the
+order because affine enforcement was never wired. However:
+
+- The WASM and Julia backends will naturally generate left-to-right code,
+  producing cross-backend semantic divergence for any program with effectful
+  or resource-consuming arguments.
+- The effect system (70% complete per STATE.a2ml) would observe handler
+  ordering tied to evaluation order, making this a latent soundness hazard.
+- A Track F1 Step relation defined in textbook CBV left-to-right form would
+  disagree with the interpreter, requiring a non-standard right-to-left
+  presentation or a proof of order-independence (which is false in general
+  for effectful languages).
+"""
+decision = """
+All n-ary expression forms evaluate their subterms strict left-to-right.
+This applies to: application arguments, tuples, arrays, record fields,
+function calls in all positions.
+
+lib/interp.ml eval_list is fixed to left-to-right:
+  and eval_list env exprs =
+    let rec loop acc = function
+      | [] -> Ok (List.rev acc)
+      | e :: rest ->
+        let* v = eval env e in
+        loop (v :: acc) rest
+    in
+    loop [] exprs
+
+Track F1's Step relation uses the standard CBV left-to-right presentation
+  e1 → e1'  ⟹  e1 e2 → e1' e2       (reduce function first)
+  e2 → e2'  ⟹  v1 e2 → v1 e2'       (then argument, only once function is a value)
+with the symmetric congruences for pairs, tuples, etc.
+"""
+consequences = """
+- lib/interp.ml eval_list is replaced (~6 LOC diff).
+- docs/spec.md gains (or receives an edit to) an explicit operational
+  semantics section stating strict CBV, left-to-right.
+- A regression test lands in Track A2 exercising a program whose output
+  depends on left-to-right evaluation (e.g. a tuple of two side-effecting
+  calls that mutate a shared counter).
+- WASM, Julia, and the effect system all become consistent with the
+  interpreter by default — no backend fix required.
+- Track F1 can proceed on its current footing to mechanise Step and the
+  progress/preservation proofs without author input.
+- Existing programs are unaffected unless they rely on observable right-
+  to-left evaluation of tuple/arg components. The interpreter is the only
+  place that did this, and nobody has filed a bug, so blast radius is
+  expected to be zero.
+"""
@@ -4,20 +4,22 @@
 [metadata]
 project = "affinescript"
 version = "0.1.0"
-last-updated = "2026-04-04"
+last-updated = "2026-04-10"
 status = "active"
 
 [project-context]
 name = "affinescript"
-completion-percentage = 92
-phase = "lsp-phase-b"
+completion-percentage = 78
+phase = "manhattan-track-a"
 tagline = "Rust-inspired language with affine types, dependent types, row polymorphism, and extensible effects"
+note = "Track A (Manhattan plan) in progress — affine enforcement landing T+7d. Headline features partially declared-but-unwired; see [features] for honest status."
 
 [components]
-lexer = "complete"
+lexer = "complete-minus-affine-tokens (ZERO/ONE tokens for quantity literals NOT emitted; blocks QTT surface syntax)"
 parser = "complete (1245 conflicts; block_terminator rule added for self-delimiting exprs)"
-type-checker = "99% (Never/bottom type handling fixed; block divergence propagation added)"
-borrow-checker = "95%"
+type-checker-rules = "99% (bidirectional inference, Never/bottom, block divergence, variant/constructor/record-spread/mutable bindings all implemented in lib/typecheck.ml)"
+type-checker-enforcement-wiring = "0% (type checker not invoked from bin/main.ml on the check/compile/eval CLI paths; rules exist but do not gate user programs)"
+borrow-checker = "phase-3-in-progress (lib/borrow.ml carries [IMPL-DEP: Phase 3] markers; not yet authoritative)"
 interpreter = "95%"
 wasm-codegen = "92% (real-world game compiles: airborne-submarine-squadron/src/main.affine → 8KB WASM)"
 wasm-gc-codegen = "70% (WasmGC proposal target: struct.new/struct.get/array.new_fixed/array.get; --wasm-gc CLI flag)"
@@ -33,3 +35,148 @@ compiler-loc = 12424
 compiler-modules = 38
 lsp-files = 5
 test-files = 54
+
+[features]
+# Honest status of the headline language features advertised in README.adoc.
+# "declared-but-unwired" = surface syntax and/or internal module exists, but
+# the feature is not enforced on user programs through the CLI pipeline.
+affine-types = "declared-but-unwired (quantity semiring exists in lib/quantity.ml but is never called from bin/main.ml; lexer does not emit ZERO/ONE tokens; enforcement landing via Track A Manhattan plan, ETA T+7d)"
+linear-arrows = "parse-only (-[q]-> syntax accepted by parser; quantity annotation not propagated into enforcement)"
+borrow-checker = "phase-3-in-progress (see lib/borrow.ml [IMPL-DEP: Phase 3])"
+row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
+effects = "declarations-only (effect types parsed and tracked; handler semantics not yet in interpreter or backends)"
+dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"
+traits = "70% (registry and lookup work; generic trait resolution needs unification integration)"
+
+[track-a-manhattan]
+owner = "primary"
+scope = "wire the quantity checker into CLI check/compile/eval paths; emit ZERO/ONE tokens from lexer; close the declared-but-unwired gap on affine types"
+spine-files = ["lib/lexer.ml", "lib/parser.mly", "lib/token.ml", "lib/typecheck.ml", "lib/quantity.ml", "bin/main.ml", "lib/interp.ml"]
+eta = "T+7d from 2026-04-10"
+
+[[open-bug]]
+id = "BUG-001"
+severity = "high"
+category = "soundness"
+title = "ω-let smuggles linear values"
+discovered = "2026-04-10"
+description = """
+let x :ω = linear_resource() in use_x_once(x) is currently accepted.
+QTT-correct form rejects — see ADR-002. The current implementation does not
+scale the Let value context by the binder quantity, so a linear value captured
+in e1 can be bound at ω and duplicated in e2.
+"""
+evidence = "lib/quantity.ml:251-253 (flat walk, no scaling); lib/typecheck.ml:631-665 (zero quantity handling)"
+fix-plan = "Track A3 — fold Let scaling into the quantity-wiring work. See ADR-002."
+regression-test = "Track A2 — add fixture examples/bug_001_omega_let_smuggles_linear.affine (must be rejected)."
+
+[[open-bug]]
+id = "BUG-002"
+severity = "medium"
+category = "semantics"
+title = ":0 lets do not erase their RHS"
+discovered = "2026-04-10"
+description = """
+let x :0 = expensive_proof_term() in body_not_using_x currently evaluates
+expensive_proof_term() and consumes its resources. QTT-correct form scales
+e1's context by 0, producing the zero context, which means e1 can be erased
+at runtime. Not a soundness hole but defeats the erasure story.
+"""
+evidence = "lib/quantity.ml:251-253; lib/interp.ml ExprLet always evaluates the RHS"
+fix-plan = "Track A3 semantics fix lands with BUG-001. Interpreter may additionally skip eval of :0-bound RHS (opt-in, deferrable)."
+regression-test = "Track A2 — add fixture examples/bug_002_zero_let_erasure.affine (non-terminating RHS bound at :0 must terminate)."
+
+[[open-bug]]
+id = "BUG-003"
+severity = "medium"
+category = "semantics"
+title = "eval_list evaluates right-to-left via List.fold_right"
+discovered = "2026-04-10"
+description = """
+lib/interp.ml:348 eval_list uses List.fold_right with monadic bind, which
+in strict OCaml evaluates arguments right-to-left. ExprBinary at :135-138 is
+left-to-right. This creates internal evaluator inconsistency and future
+backend/interpreter divergence once effects or affine enforcement land.
+See ADR-003.
+"""
+evidence = "lib/interp.ml:348-353 (fold_right); lib/interp.ml:135-138 (L-to-R binop by contrast)"
+fix-plan = "Track A3 — fix eval_list to strict L-to-R (~6 LOC). See ADR-003."
+regression-test = "Track A2 — add fixture examples/bug_003_eval_order.affine with observable L-to-R ordering via a shared counter."
+
+[[open-bug]]
+id = "BUG-004"
+severity = "medium"
+category = "soundness"
+title = "Lambda-body usage not tracked against outer captures"
+discovered = "2026-04-10"
+description = """
+lib/quantity.ml:245-249 explicitly documents that lambda-bound params are
+not tracked and that 'the lambda body may still reference outer tracked
+variables' — but the current code does not charge usage against those
+captures. A lambda capturing a linear variable can be called multiple times,
+duplicating the captured resource.
+"""
+evidence = "lib/quantity.ml:245-249 (comment admits the gap)"
+fix-plan = "Track D (borrow checker Phase 3) — lambda capture analysis is part of the borrow/ownership story. Not A3 scope."
+regression-test = "Track D fixture — deferred until borrow checker lands."
+
+[[open-bug]]
+id = "BUG-005"
+severity = "medium"
+category = "codegen"
+title = "WasmGC backend silently drops unknown function calls"
+discovered = "2026-04-10"
+description = """
+lib/codegen_gc.ml ExprApp handling silently emits 'drop all args + push null'
+when the callee is not in the func_indices table, and does the same for
+indirect calls. This is placeholder behaviour that produces wrong code rather
+than failing loudly. Any program that reaches codegen with an unresolved
+function call will compile to nonsense at runtime.
+"""
+evidence = "lib/codegen_gc.ml gen_gc_expr ExprApp case (the 38-line block added as part of the in-progress WasmGC work)"
+fix-plan = "Replace silent drops with explicit CodegenError. Direct-call path (via func_indices) and int/float builtin coercions stay — they're correct. Only the fallback arms need to fail loudly."
+regression-test = "Add a fixture that intentionally references an unknown function name and expects a loud compile error."
+
+# ─── Deferred upgrade: bring .machine_readable/ to current standards ──────────
+# AffineScript predates most of the current hyperpolymath .machine_readable/
+# suite. The 6a2 core is present; the surrounding machinery is not. This is
+# logged as deferred work, separate from the Manhattan recovery, to avoid
+# scope creep into that plan.
+
+[deferred-upgrade]
+session = "separate, not Phase 0"
+estimated-effort = "1-2 focused hours"
+
+present:
+# What AffineScript already has
+present = [
+  ".machine_readable/6a2/AGENTIC.a2ml",
+  ".machine_readable/6a2/ECOSYSTEM.a2ml",
+  ".machine_readable/6a2/META.a2ml",
+  ".machine_readable/6a2/NEUROSYM.a2ml",
+  ".machine_readable/6a2/PLAYBOOK.a2ml",
+  ".machine_readable/6a2/STATE.a2ml",
+  ".machine_readable/anchors/ANCHOR.a2ml",  # added 2026-04-10 as first anchor
+  "contractiles/ (root-level, old location) — dust, k9, lust, must, trust"
+]
+
+missing = [
+  ".machine_readable/CLADE.a2ml",
+  ".machine_readable/contractiles/ (should migrate from root contractiles/)",
+  ".machine_readable/contractiles/adjust/",
+  ".machine_readable/contractiles/intend/",
+  ".machine_readable/agent_instructions/",
+  ".machine_readable/integrations/",
+  ".machine_readable/ADJUST.contractile (top-level instance)",
+  ".machine_readable/INTENT.contractile (top-level instance)",
+  ".machine_readable/MUST.contractile (top-level instance)",
+  ".machine_readable/TRUST.contractile (top-level instance)"
+]
+
+notes = """
+Root-level contractiles/ directory has 5 of 7 current types. The canonical
+pattern is .machine_readable/contractiles/ with all 7 types. Migration is
+deferred to a separate session because it requires reading each contractile
+definition from the standards repo and deciding which apply to AffineScript
+specifically. Do not conflate with Manhattan Phase 0.
+"""