ReScript→AffineScript migration: toolchain + Types.affine (module 1 of 17)

PROOF-NEEDS.md

@@ -4,11 +4,91 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # PROOF-NEEDS.md
 
-## Template ABI Cleanup (2026-03-29)
+> Engineering ledger for the error-lang **formal core**. This is the honest
+> substrate beneath the language's deliberately tongue-in-cheek "100%
+> production-ready, formally verified" self-presentation: it records what is
+> *actually* machine-checked, what is not, and how to reproduce the checks.
+> The language may dissemble about itself on purpose — this file does not.
 
-Template ABI removed -- was creating false impression of formal verification.
-The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
-scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
+## Formal core (`src/abi/`)
 
-When this project needs formal ABI verification, create domain-specific Idris2 proofs
-following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.
+Three properties of the computational-haptics engine are proved in Idris2 and
+**machine-checked under Idris 2, version 0.8.0**, with **no escape hatches**
+(no `believe_me`, `assert_total`, `cast`-coerced equality, or `postulate`):
+
+| Property | Module | Status |
+|---|---|---|
+| Stability score ∈ [0, 100] | `src/abi/Stability.idr` | ✅ proved (`stabilityUpperBound`, `stabilityLowerBound`) |
+| Positional-operator determinism | `src/abi/Positional.idr` | ✅ proved (`positionalDeterministic`) + sanity evaluations |
+| Paradox-factor monotonicity | `src/abi/Paradox.idr` | ⚠️ partial — two factors proved, blanket claim retracted (below) |
+
+`src/abi/Foreign.idr` is an honest, self-contained ABI **binding-declaration**
+layer (it asserts no theorems). All four modules are listed in
+`src/abi/error-lang-abi.ipkg`.
+
+### Reproduce
+
+```sh
+# idris2 is not in apt here, and the ziglang/deno mirrors are blocked by the
+# environment network policy, so build the proof checker from source via Chez:
+sudo apt-get install -y chezscheme libgmp-dev make gcc
+git clone https://github.com/idris-lang/Idris2 && cd Idris2
+make bootstrap SCHEME=chezscheme && make install
+export PATH="$HOME/.idris2/bin:$PATH"
+
+# then, from the error-lang repo root:
+./verification/check-proofs.sh
+# or:  cd src/abi && idris2 --typecheck error-lang-abi.ipkg
+```
+
+### The monotonicity retraction (an honest finding)
+
+The previously-advertised property *"paradox detection is monotonic with
+complexity"* is **false of the implementation** — and attempting to prove it
+honestly is what surfaced that. `error_lang_detect_paradoxes`
+(`ffi/zig/src/main.zig`) gates `scope_leakage` on `isPrime(line_count)`, which
+is not monotone: line **7** is prime → active, line **8** is composite →
+inactive, even though 8 > 7.
+
+`src/abi/Paradox.idr` therefore proves the part that *is* true — the two
+threshold-gated factors are monotone in their driving metric
+(`superpositionMonotone` for `var_count > 10`; `temporalMonotone` for
+`depth > 5`) — and retracts the blanket claim, recording the scope-leakage
+obstruction explicitly. Non-monotone scope leakage is intentional; it is the
+pedagogical point of the paradox. The difference now is that the proof says so
+out loud, instead of hiding it behind `cast Refl`.
+
+## What was removed (2026-06-23)
+
+`src/abi/Foreign.idr` previously carried three "Safety Proofs" —
+`stabilityBounded`, `positionalDeterministic`, `paradoxMonotonic` — that were
+**not proofs**. Each manufactured its evidence with `cast ()` / `cast Refl`
+over an `IO` action (e.g. calling an FFI function twice and coercing
+`Refl : x = x` onto the two distinct results, with a comment that it "should
+hold in practice"). An earlier note in this file claimed these files had been
+removed; in fact `Foreign.idr` was still present and still exported the fakes.
+
+They are now deleted and replaced by the genuine, machine-checked modules above.
+
+## Open obligations
+
+1. **CI gate.** Add an Idris2 `--typecheck error-lang-abi.ipkg` job so the core
+   is checked on every push. (The dev image has no idris2 by default; it was
+   built from source for this change.)
+2. **Implementation conformance.** The proofs are stated over abstract models
+   that mirror `ffi/zig/src/main.zig` and `compiler/src/Types.res`. Two of those
+   implementations **disagree**: positional behaviour is `column % 2` (two-way)
+   in the Zig FFI but `(line*31 + column) mod 4` (four-way) in `Stability.res`.
+   Reconcile them, then bind the proofs to the chosen implementation by
+   extraction or conformance tests rather than parallel models.
+3. **Zig weighted-average path.** `error_lang_calculate_stability` is a convex
+   combination (weights sum to 1) of per-factor scores in [0,100]; its [0,100]
+   bound holds for a *different* reason than the `Stability.res` clamp proved
+   here. Prove that path too.
+4. **Programs not executed in this environment.** Under the current network
+   policy the Deno runtime's JSR std deps (`jsr.io`) and Zig 0.13.0
+   (`ziglang.org`) are unreachable, and the ReScript compiler does not currently
+   build (`return` is not valid ReScript — `VM.res:407`; `dict<string, int>`
+   applies the one-argument `dict` constructor to two arguments —
+   `Types.res:233`). These were **not** run or fixed as part of this change and
+   are tracked as separate work — they are not claimed to pass.

compiler/src/Types.affine

@@ -0,0 +1,241 @@
+// SPDX-License-Identifier: MPL-2.0
+// Types.affine — core type definitions for Error-Lang
+// Ported from compiler/src/Types.res. Port conventions:
+//   * ReScript inline-record variants -> positional constructor args.
+//   * array<T> -> [T]; option<T> -> Option<T>; dict<k,v> -> Dict<k,v>; tuples kept.
+//   * Token variants `Float`/`String` renamed `FloatTok`/`StringTok`
+//     (`Float`/`String` are reserved type keywords in AffineScript).
+//
+// This is the `Types` module; sibling compiler modules `use Types::{...}`.
+// Cross-module struct field access requires the affinescript module-resolver
+// fix in patches/affinescript-module-struct-fields.patch.
+
+module Types;
+
+use prelude::*;
+
+pub struct Position {
+  line: Int,
+  column: Int,
+  offset: Int
+}
+
+pub struct Location {
+  start: Position,
+  end_: Position,
+  file: String
+}
+
+pub enum TokenType {
+  // Keywords
+  Main, End, Let, Mutable, Function, Struct, If, Elseif, Else, While, For, In,
+  Break, Continue, Return, And, Or, Not, True, False, Nil, Gutter, Fn,
+  // Types
+  TInt, TFloat, TString, TBool, TArray, TEcho, TEchoR,
+  // Literals
+  Integer(Int),
+  FloatTok(Float),     // ReScript Float(float)
+  StringTok(String),   // ReScript String(string)
+  Identifier(String),
+  // Operators
+  Plus, Minus, Star, Slash, Percent, EqualEqual, BangEqual, Less, Greater,
+  LessEqual, GreaterEqual, Ampersand, Pipe, Caret, Tilde, LessLess, GreaterGreater,
+  Equal, Arrow, Question, Colon,
+  // Delimiters
+  LParen, RParen, LBracket, RBracket, LBrace, RBrace, Comma, Dot,
+  // Special
+  Newline, EOF, Error(String)
+}
+
+pub struct Token {
+  type_: TokenType,
+  lexeme: String,
+  loc: Location
+}
+
+// ============================================
+// AST
+// ============================================
+
+pub enum Expr {
+  IntLit(Int, Location),
+  FloatLit(Float, Location),
+  StringLit(String, Location),
+  BoolLit(Bool, Location),
+  NilLit(Location),
+  Ident(String, Location),
+  Array([Expr], Location),
+  Binary(Expr, BinaryOp, Expr, Location),
+  Unary(UnaryOp, Expr, Location),
+  Call(Expr, [Expr], Location),
+  Index(Expr, Expr, Location),
+  Member(Expr, String, Location),
+  Ternary(Expr, Expr, Expr, Location),
+  Lambda([Param], Option<TypeExpr>, LambdaBody, Location)
+}
+
+pub enum BinaryOp {
+  Add, Sub, Mul, Div, Mod,
+  Eq, Neq, Lt, Gt, Lte, Gte,
+  BAnd, BOr, BXor, Shl, Shr,
+  LAnd, LOr
+}
+
+pub enum UnaryOp { Neg, LNot, BNot }
+
+pub struct Param {
+  name: String,
+  type_: Option<TypeExpr>,
+  loc: Location
+}
+
+pub enum TypeExpr {
+  TyInt,
+  TyFloat,
+  TyString,
+  TyBool,
+  TyArray(TypeExpr),
+  // Echo types (Trope-IR-ready, see docs/Trope-Particularity-Integration.adoc):
+  //   TyEcho        ~ Trope[Phi]        (retained witness)
+  //   TyEchoResidue ~ FloatingQuality   (witness severed)
+  TyEcho(Option<TypeExpr>, Option<TypeExpr>),
+  TyEchoResidue(Option<TypeExpr>, Option<TypeExpr>),
+  TyIdent(String)
+}
+
+pub enum LambdaBody {
+  LambdaExpr(Expr),
+  LambdaBlock([Stmt])
+}
+
+pub enum Stmt {
+  // inline records -> positional: (mutable_, name, type_, value, loc)
+  LetStmt(Bool, String, Option<TypeExpr>, Expr, Location),
+  // (target, value, loc)
+  AssignStmt(Expr, Expr, Location),
+  // (cond, then_, elseifs, else_, loc)
+  IfStmt(Expr, [Stmt], [(Expr, [Stmt])], Option<[Stmt]>, Location),
+  // (cond, body, loc)
+  WhileStmt(Expr, [Stmt], Location),
+  // (var, iter, body, loc)
+  ForStmt(String, Expr, [Stmt], Location),
+  // (value, loc)
+  ReturnStmt(Option<Expr>, Location),
+  BreakStmt(Location),
+  ContinueStmt(Location),
+  // (println, args, loc)
+  PrintStmt(Bool, [Expr], Location),
+  // (tokens, recovered, loc)
+  GutterBlock([Token], Bool, Location),
+  ExprStmt(Expr)
+}
+
+pub enum Decl {
+  // (name, params, returnType, body, loc)
+  FunctionDecl(String, [Param], Option<TypeExpr>, [Stmt], Location),
+  // (name, fields, loc)
+  StructDecl(String, [(String, TypeExpr)], Location),
+  // (body, loc)
+  MainBlock([Stmt], Location),
+  StmtDecl(Stmt)
+}
+
+pub struct Program {
+  declarations: [Decl],
+  loc: Location
+}
+
+// ============================================
+// Errors
+// ============================================
+
+pub enum ErrorCode {
+  E0001, E0002, E0003, E0004, E0005, E0006, E0007, E0008, E0009, E0010
+}
+
+pub struct Diagnostic {
+  code: ErrorCode,
+  message: String,
+  loc: Location,
+  runNumber: Int,
+  hint: Option<String>
+}
+
+// ============================================
+// Runtime state & stability
+// ============================================
+
+pub enum StabilityFactor {
+  MutableState(Int, Int),       // mutations, readers
+  TypeInstability(Int),         // reassignments
+  NullPropagation(Int),         // depth
+  GlobalState(Int, Int),        // mutations, dependencies
+  UnhandledError(Int),          // paths
+  AlgorithmComplexity(Float),   // time_ms
+  MemoryLeak(Int),              // bytes
+  RaceCondition(Int)            // conflicts
+}
+
+pub struct StabilityReport {
+  score: Int,
+  factors: [StabilityFactor],
+  breakdown: Dict<String, Int>,
+  recommendations: [String]
+}
+
+pub struct RuntimeState {
+  runCounter: Int,
+  stabilityScore: Int,
+  lastError: Option<ErrorCode>,
+  seed: Int,
+  stabilityFactors: [StabilityFactor],
+  discoveredRules: [String],
+  historicalRuns: [Int]
+}
+
+pub fn make_default_state() -> RuntimeState {
+  #{
+    runCounter: 0,
+    stabilityScore: 100,
+    lastError: None,
+    seed: 0,
+    stabilityFactors: [],
+    discoveredRules: [],
+    historicalRuns: []
+  }
+}
+
+// Stability impact (non-positive), mirrors Types.res `stabilityImpact`.
+pub fn stability_impact(factor: StabilityFactor) -> Int {
+  match factor {
+    MutableState(mutations, readers) => -(10 * mutations + 5 * readers),
+    TypeInstability(reassignments) => -(15 * reassignments),
+    NullPropagation(depth) => -(20 * depth),
+    GlobalState(mutations, dependencies) => -(30 * mutations + 5 * dependencies),
+    UnhandledError(paths) => -(25 * paths),
+    AlgorithmComplexity(time_ms) => -trunc(time_ms / 10.0),
+    MemoryLeak(bytes) => -(10 * (bytes / 1024)),
+    RaceCondition(conflicts) => -(40 * conflicts)
+  }
+}
+
+// mirrors Types.res `calculateStability`: max(0, 100 + sum(impacts))
+pub fn calculate_stability(factors: [StabilityFactor]) -> Int {
+  let penalties = fold(factors, 0, |acc, x| acc + stability_impact(x));
+  max(0, 100 + penalties)
+}
+
+pub fn error_code_to_string(code: ErrorCode) -> String {
+  match code {
+    E0001 => "E0001",
+    E0002 => "E0002",
+    E0003 => "E0003",
+    E0004 => "E0004",
+    E0005 => "E0005",
+    E0006 => "E0006",
+    E0007 => "E0007",
+    E0008 => "E0008",
+    E0009 => "E0009",
+    E0010 => "E0010"
+  }
+}