diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 566ed20..f8b5a30 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -4,11 +4,91 @@ Copyright (c) Jonathan D.A. Jewell --> # 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` + 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. diff --git a/compiler/src/Lexer.affine b/compiler/src/Lexer.affine new file mode 100644 index 0000000..78f3ea1 --- /dev/null +++ b/compiler/src/Lexer.affine @@ -0,0 +1,363 @@ +// SPDX-License-Identifier: MPL-2.0 +// Lexer.affine — tokenizer for Error-Lang (ported from compiler/src/Lexer.res). +// +// AffineScript has no mutable struct fields or record-spread, so the imperative +// ReScript lexer is rendered functionally: state-mutating helpers take a +// LexerState and return a new one (full-record reconstruction); the scanners and +// driver loop a `let mut` local. Single chars are Char (char_at / char_to_int); +// the escape buffer is built with single-char substrings. +// +// Known parity gaps vs Lexer.res (decimal/core path is faithful; these are +// tracked for a follow-up parity pass): +// - hex (0x) / binary (0b) integer prefixes +// - triple-quoted strings and the \0 null escape +// - smart-quote (U+201C / U+201D) detection (diagnostic E0007) + +module Lexer; + +use prelude::*; +use string::{char_at, length, substring, is_digit, is_alpha, is_alphanumeric}; +use Types::*; + +pub struct LexerState { + source: String, + file: String, + pos: Int, + line: Int, + column: Int, + tokens: [Token], + diagnostics: [Diagnostic], + runNumber: Int +} + +pub fn make(source: String, file: String, run_number: Int) -> LexerState { + #{ source: source, file: file, pos: 0, line: 1, column: 1, + tokens: [], diagnostics: [], runNumber: run_number } +} + +// ---- peeking (read copyable fields only; never consume the state) ---- + +fn peek_at(source: String, pos: Int, offset: Int) -> Option { + char_at(source, pos + offset) +} + +// code point of the char at pos+offset, or -1 at end of input +fn code_at(source: String, pos: Int, offset: Int) -> Int { + match char_at(source, pos + offset) { + Some(c) => char_to_int(c), + None => -1 + } +} + +fn mk_pos(line: Int, column: Int, offset: Int) -> Position { + #{ line: line, column: column, offset: offset } +} + +fn is_hex_digit(c: Char) -> Bool { + let k = char_to_int(c); + (k >= 48 && k <= 57) || (k >= 97 && k <= 102) || (k >= 65 && k <= 70) +} + +// ---- keyword table (ReScript Dict -> match on string equality) ---- + +fn keyword_lookup(w: String) -> Option { + if w == "main" { Some(Main) } + else if w == "end" { Some(End) } + else if w == "let" { Some(Let) } + else if w == "mutable" { Some(Mutable) } + else if w == "function" { Some(Function) } + else if w == "struct" { Some(Struct) } + else if w == "if" { Some(If) } + else if w == "elseif" { Some(Elseif) } + else if w == "else" { Some(Else) } + else if w == "while" { Some(While) } + else if w == "for" { Some(For) } + else if w == "in" { Some(In) } + else if w == "break" { Some(Break) } + else if w == "continue" { Some(Continue) } + else if w == "return" { Some(Return) } + else if w == "and" { Some(And) } + else if w == "or" { Some(Or) } + else if w == "not" { Some(Not) } + else if w == "true" { Some(True) } + else if w == "false" { Some(False) } + else if w == "nil" { Some(Nil) } + else if w == "gutter" { Some(Gutter) } + else if w == "fn" { Some(Fn) } + else if w == "Int" { Some(TInt) } + else if w == "Float" { Some(TFloat) } + else if w == "String" { Some(TString) } + else if w == "Bool" { Some(TBool) } + else if w == "Array" { Some(TArray) } + else if w == "Echo" { Some(TEcho) } + else if w == "EchoR" { Some(TEchoR) } + else if w == "print" { Some(Identifier("print")) } + else if w == "println" { Some(Identifier("println")) } + else { None } +} + +// ---- state transitions (consume + rebuild) ---- + +fn advance(s: LexerState) -> LexerState { + let is_nl = code_at(s.source, s.pos, 0) == 10; + let new_line = if is_nl { s.line + 1 } else { s.line }; + let new_col = if is_nl { 1 } else { s.column + 1 }; + #{ source: s.source, file: s.file, pos: s.pos + 1, + line: new_line, column: new_col, + tokens: s.tokens, diagnostics: s.diagnostics, runNumber: s.runNumber } +} + +fn add_token(s: LexerState, type_: TokenType, lexeme: String, loc: Location) -> LexerState { + let tok = #{ type_: type_, lexeme: lexeme, loc: loc }; + #{ source: s.source, file: s.file, pos: s.pos, line: s.line, column: s.column, + tokens: s.tokens ++ [tok], diagnostics: s.diagnostics, runNumber: s.runNumber } +} + +fn add_diagnostic(s: LexerState, code: ErrorCode, message: String, loc: Location) -> LexerState { + let diag = #{ code: code, message: message, loc: loc, + runNumber: s.runNumber, hint: None }; + #{ source: s.source, file: s.file, pos: s.pos, line: s.line, column: s.column, + tokens: s.tokens, diagnostics: s.diagnostics ++ [diag], runNumber: s.runNumber } +} + +// Advance once, emitting a token whose location spans the single consumed char. +fn single_tok(s: LexerState, t: TokenType, lex: String) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, t, lex, loc) +} + +// ---- scanners ---- + +fn scan_comment(s: LexerState) -> LexerState { + let mut st = s; + while (code_at(st.source, st.pos, 0) != 10) && (st.pos < length(st.source)) { + st = advance(st); + } + st +} + +fn scan_identifier(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let start_pos = s.pos; + let mut st = s; + while (match char_at(st.source, st.pos) { Some(c) => is_alphanumeric(c), None => false }) { + st = advance(st); + } + let lexeme = substring(st.source, start_pos, st.pos); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let type_ = match keyword_lookup(lexeme) { + Some(kw) => kw, + None => Identifier(lexeme) + }; + add_token(st, type_, lexeme, loc) +} + +fn scan_number(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let start_pos = s.pos; + let mut st = s; + + // integer part + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + + // optional fractional part: '.' followed by a digit + let mut is_float = false; + if (code_at(st.source, st.pos, 0) == 46) && (match char_at(st.source, st.pos + 1) { Some(c) => is_digit(c), None => false }) { + is_float = true; + st = advance(st); // '.' + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + } + + // optional exponent + let ec = code_at(st.source, st.pos, 0); + if ec == 101 || ec == 69 { // e / E + is_float = true; + st = advance(st); + let sgn = code_at(st.source, st.pos, 0); + if sgn == 43 || sgn == 45 { st = advance(st); } // + / - + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + } + + let lexeme = substring(st.source, start_pos, st.pos); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + if is_float { + match parse_float(lexeme) { + Some(f) => add_token(st, FloatTok(f), lexeme, loc), + None => add_token(st, Error("Invalid float"), lexeme, loc) + } + } else { + match parse_int(lexeme) { + Some(n) => add_token(st, Integer(n), lexeme, loc), + None => add_token(st, Error("Invalid integer"), lexeme, loc) + } + } +} + +// String literal (single-quote-aware double-quoted; escapes; no triple-quote — +// simplified from the .res triple-quote handling, noted for the parity pass). +fn scan_string(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let mut st = advance(s); // opening quote + let mut buf = ""; + let mut done = false; + let mut result = st; + + while !done { + let c = code_at(st.source, st.pos, 0); + if c == -1 { + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let st2 = add_diagnostic(st, E0002, "Unterminated string literal", loc); + result = add_token(st2, Error("Unterminated string"), buf, loc); + done = true; + } else if c == 34 { // closing " + st = advance(st); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let quoted = "\"" ++ buf ++ "\""; + result = add_token(st, StringTok(buf), quoted, loc); + done = true; + } else if c == 92 { // backslash escape + st = advance(st); + let e = code_at(st.source, st.pos, 0); + if e == 110 { buf = buf ++ "\n"; st = advance(st); } + else if e == 114 { buf = buf ++ "\r"; st = advance(st); } + else if e == 116 { buf = buf ++ "\t"; st = advance(st); } + else if e == 92 { buf = buf ++ "\\"; st = advance(st); } + else if e == 34 { buf = buf ++ "\""; st = advance(st); } + else if e == -1 { done = true; result = st; } + else { + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + st = add_diagnostic(st, E0003, "Invalid escape sequence", loc); + st = advance(st); + } + } else if c == 10 { // newline in string + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let st2 = add_diagnostic(st, E0002, "Unterminated string literal (newline in string)", loc); + result = add_token(st2, Error("Unterminated string"), buf, loc); + done = true; + } else { + buf = buf ++ substring(st.source, st.pos, st.pos + 1); + st = advance(st); + } + } + result +} + +// ---- main dispatch + driver ---- + +fn step(s: LexerState) -> LexerState { + let c = code_at(s.source, s.pos, 0); + if c == 32 || c == 9 || c == 13 { + advance(s) + } else if c == 10 { // newline token + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, Newline, "\\n", loc) + } else if c == 35 { // # + scan_comment(s) + } else if c == 43 { single_tok(s, Plus, "+") } + else if c == 45 { // - or -> + if code_at(s.source, s.pos, 1) == 62 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, Arrow, "->", loc) + } else { single_tok(s, Minus, "-") } + } + else if c == 42 { single_tok(s, Star, "*") } + else if c == 47 { single_tok(s, Slash, "/") } + else if c == 37 { single_tok(s, Percent, "%") } + else if c == 61 { // = or == + if code_at(s.source, s.pos, 1) == 61 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, EqualEqual, "==", loc) + } else { single_tok(s, Equal, "=") } + } + else if c == 33 { // ! -> != or error + if code_at(s.source, s.pos, 1) == 61 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, BangEqual, "!=", loc) + } else { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_diagnostic(s2, E0001, "Unexpected character '!'", loc) + } + } + else if c == 60 { // < <= << + let n = code_at(s.source, s.pos, 1); + if n == 61 { two_char(s, LessEqual, "<=") } + else if n == 60 { two_char(s, LessLess, "<<") } + else { single_tok(s, Less, "<") } + } + else if c == 62 { // > >= >> + let n = code_at(s.source, s.pos, 1); + if n == 61 { two_char(s, GreaterEqual, ">=") } + else if n == 62 { two_char(s, GreaterGreater, ">>") } + else { single_tok(s, Greater, ">") } + } + else if c == 38 { single_tok(s, Ampersand, "&") } + else if c == 124 { single_tok(s, Pipe, "|") } + else if c == 94 { single_tok(s, Caret, "^") } + else if c == 126 { single_tok(s, Tilde, "~") } + else if c == 63 { single_tok(s, Question, "?") } + else if c == 58 { single_tok(s, Colon, ":") } + else if c == 40 { single_tok(s, LParen, "(") } + else if c == 41 { single_tok(s, RParen, ")") } + else if c == 91 { single_tok(s, LBracket, "[") } + else if c == 93 { single_tok(s, RBracket, "]") } + else if c == 123 { single_tok(s, LBrace, "{") } + else if c == 125 { single_tok(s, RBrace, "}") } + else if c == 44 { single_tok(s, Comma, ",") } + else if c == 46 { single_tok(s, Dot, ".") } + else if c == 34 { scan_string(s) } // " + else { + match char_at(s.source, s.pos) { + Some(ch) => + if is_digit(ch) { scan_number(s) } + else if is_alpha(ch) { scan_identifier(s) } + else { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + let lex = substring(s2.source, start.offset, s2.pos); + add_token(add_diagnostic(s2, E0004, "Illegal character", loc), Error("Illegal"), lex, loc) + }, + None => s + } + } +} + +fn two_char(s: LexerState, t: TokenType, lex: String) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, t, lex, loc) +} + +pub fn tokenize(s0: LexerState) -> LexerState { + let mut s = s0; + while s.pos < length(s.source) { + s = step(s); + } + let eof = mk_pos(s.line, s.column, s.pos); + let loc = #{ start: eof, end_: mk_pos(s.line, s.column, s.pos), file: s.file }; + add_token(s, EOF, "", loc) +} + +pub fn lex(source: String, file: String, run_number: Int) -> ([Token], [Diagnostic]) { + let s = tokenize(make(source, file, run_number)); + (s.tokens, s.diagnostics) +} diff --git a/compiler/src/Types.affine b/compiler/src/Types.affine new file mode 100644 index 0000000..75f41c2 --- /dev/null +++ b/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]; option -> Option; dict -> Dict; 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, 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, + 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, Option), + TyEchoResidue(Option, Option), + TyIdent(String) +} + +pub enum LambdaBody { + LambdaExpr(Expr), + LambdaBlock([Stmt]) +} + +pub enum Stmt { + // inline records -> positional: (mutable_, name, type_, value, loc) + LetStmt(Bool, String, Option, 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, 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, [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 +} + +// ============================================ +// 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, + recommendations: [String] +} + +pub struct RuntimeState { + runCounter: Int, + stabilityScore: Int, + lastError: Option, + 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" + } +} diff --git a/docs/Trope-Particularity-Integration.adoc b/docs/Trope-Particularity-Integration.adoc new file mode 100644 index 0000000..ea4ad12 --- /dev/null +++ b/docs/Trope-Particularity-Integration.adoc @@ -0,0 +1,246 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Trope-Particularity Integration: Error-Lang as a Trope IR Front End +:toc: +:sectnums: +:source-highlighter: rouge + +[abstract] +This is a *design* (not yet implemented). It proposes that Error-Lang become a +second *front end* to the portable trope-checker +(https://github.com/hyperpolymath/trope-checker[`hyperpolymath/trope-checker`]), +lowering its Echo operations and its stability factors to the language-neutral +*Trope IR* (v0.1, `prevent` profile) and consuming the checker's verified verdict +and witness. It defines the object/effect/grade correspondence, the verdict +mapping, the architecture (reference, never vendor), and — most importantly — the +per-front-end *lowering-correctness obligations* the trope-checker does **not** +discharge for us. + +Both systems already sit on the same substrate: the +https://github.com/hyperpolymath/echo-types[echo-types] graded-loss line, cited +verbatim by `docs/Echo-Decomposition.adoc` and by the trope calculus +(`trope-checker/spec/calculus.adoc`, "Provenance of the ideas"). This document +makes that shared lineage *operational*. + +== Motivation: a stability score is a scalar; loss is not + +Error-Lang grades instability with `calculateStability` (`compiler/src/Types.res` +lines 270–274): + +[source] +---- +calculateStability(factors) = max(0, 100 + Σ stabilityImpact(factor)) +---- + +Every `stabilityFactor` is mapped to a single negative integer and the integers +are summed. That is a *scalar collapse* of structured loss. The trope-particularity +calculus exists to reject exactly this move — its load-bearing thesis +(`calculus.adoc` §3) is: + +[quote] +A grade is *not a scalar*: two operations can lose the same _amount_ yet differ +in _kind_ and in _honesty_. + +So the calculus's three-coordinate grade is a principled *upgrade* of Error-Lang's +stability model. It lets us keep _which_ particularity degraded, whether the loss +is _recoverable_, and whether it is _honest_ — and it yields a use-relative +*verdict* with a *witness edge* ("the operation to repair") in place of an opaque +`0–100` number. For a language whose entire identity is the *visible decomposition* +of structure (`Echo-Decomposition.adoc`, "Decomposition must be visible"), this is +a capability upgrade, not ornament. + +Two further alignments make the fit unusually tight: + +* **The Echo operations already _are_ trope effects.** `echo`, `echo_to_residue`, + `echo_input`, `echo_output` implement witness-retention and irreversible erasure + — which the calculus names `preserve`, `detach`, and field `project` (§5). +* **The verification toolchains already overlap.** The trope-checker's core is an + Agda reference plus an Idris2 implementation (the `trope-checker` repo's Idris2 core, `Main.idr`); + Error-Lang already carries an Idris2 proof of the *scalar* bound + (`src/abi/Stability.idr`). The integration generalises that proof's target from + a clamped integer to a checked grade. + +== The correspondence + +=== Objects: Echo ↔ trope, EchoR ↔ FloatingQuality + +A trope is a property-instance over the field set +`Φ = {quality, bearer, context, record}` (`calculus.adoc` §2). Error-Lang's +`Echo` — a retained witness `x : A` with the visible output `y : B` it +reached — populates Φ as: + +[cols="1,2,3",options="header"] +|=== +| Φ field | Echo content | Justification + +| `bearer` | the witness `x : A` | the *particular* entity the result is a result _of_ +| `quality` | the reached output `y : B` (and `f x ≡ y`) | the situated property borne by `x` +| `context` | the function `f` / evaluation site | what individuates this fibre element +| `record` | the runtime pairing `VEcho{input,output}` | honest provenance of how `y` arose +|=== + +[cols="1,2",options="header"] +|=== +| Echo form | Trope IR node + +| `Echo` | `type: "Trope"`, `present: ["quality","bearer","context","record"]` +| `EchoR` | `type: "FloatingQuality"`, `present: ["quality"]` (no `bearer` — the severance is structurally visible) +|=== + +The type change `Echo → EchoR` is exactly the type change `Trope → FloatingQuality`, +and the reason `echo_input` is *illegal on a residue* (`Echo-Decomposition.adoc` +Plane 3) is, in IR terms, that a `FloatingQuality` node has *no bearer field to +project*. The same fact, two vocabularies. + +=== Echo operations → writable effects + +[cols="2,2,3",options="header"] +|=== +| Echo op | Effect | Grade (per `calculus.adoc` §5) + +| `echo(x,y)` | `preserve` | `ε` — all fields `Present`, `bond=Intact`, `merge=Single` +| `echo_output(e)` | `project[quality]` | drop `bearer,context,record`; quality survives; `bond=Withheld` +| `echo_input(e)` | `project[bearer]` | legal only while `bearer ∈ S`; *undefined on `FloatingQuality`* +| `echo_to_residue(e)`| `detach` | `sever`: `fate(quality)=Present`, others `Dropped`, `bond=Severed`, `merge=Single` +|=== + +The `[Stab-Erase]` rule (`spec/type-system.md` §7) debits stability *exactly once*, +on `echo_to_residue`, and never on projection. That is precisely the calculus's +accounting: `detach` carries the `Severed` (irrecoverable) loss; `project` carries +only a recoverable `Withheld`. The educational invariant "`echo_to_residue` must +**not** become a silent cast" is the calculus's refusal of untagged/deceptive +collapse. + +.Worked Trope IR — `echo_to_residue` as a `detach` (illustrative, schema-shaped) +[source,json] +---- +{ + "version": "0.1", "profile": "prevent", + "nodes": [ + { "id": "e", "type": "Trope", "present": ["quality","bearer","context","record"] }, + { "id": "res", "type": "FloatingQuality", "present": ["quality"] } + ], + "edges": [ + { "id": "erase", "effect": "detach", "inputs": ["e"], "output": "res", + "grade": { + "fate": { "quality": {"k":"Present"}, "bearer": {"k":"Dropped"}, + "context": {"k":"Dropped"}, "record": {"k":"Dropped"} }, + "bond": { "k": "Severed" }, "merge": { "k": "Single" } }, + "note": "echo_to_residue: witness erased, output reachable" } + ], + "use_model": { "output": "res", "floor": { "bond": { "k": "Withheld" } } } +} +---- + +Here the floor demands `bond ⊒ Withheld` (the use needs a _recoverable_ bearer); +since `detach` delivered `Severed`, the verdict is `p-insufficient`, witness = +`erase`. A use that only reads `echo_output` would declare a quality-only floor and +pass. The score becomes a *reason*. + +=== stabilityFactor → grade + +Each `stabilityFactor` becomes a grade, with its `stabilityImpact` magnitude +feeding the fidelity element `δ`. Crucially, the two *silent* instabilities land +on the deceptive `Conflated` bottom — an untagged merge of particulars — which, +under the `prevent` profile, is a *lowering fault* the validator rejects by name. +Error-Lang's worst bugs are the calculus's moral-core violation. + +[cols="2,3,2",options="header"] +|=== +| Factor | Grade (faithful lowering) | Honesty + +| `TypeInstability{reassignments}` | `fate(quality)=Attenuated(15·r)` | faithful +| `NullPropagation{depth}` | `fate(quality)=Attenuated(20·d)`, `Dropped` at the leaf | faithful +| `UnhandledError{paths}` | `fate=Dropped` on the unguarded error fields | faithful (visible gap) +| `AlgorithmComplexity{time_ms}` | `fate=Attenuated(δ)`, `δ=⊤` when unbounded (matches `fix`→`⊤`, §7) | faithful +| `MutableState{mutations,readers}` | `fate(quality)=Attenuated(10·m+5·r)`; `Fused(τ=write-site)` if writes blend | faithful if tracked +| `MemoryLeak{bytes}` | `detach`: `bond=Severed` (owner unreachable, irrecoverable) | faithful +| `GlobalState{mutations,deps}` | `Fused(τ=global@site)` if threaded; **`Conflated` (fault)** if silent | *deceptive when silent* +| `RaceCondition{conflicts}` | `Fused(τ=lock)` if serialised; **`Conflated` (fault)** if unsynchronised | *deceptive when silent* +|=== + +=== Verdict and witness + +[cols="1,2",options="header"] +|=== +| Error-Lang today | Trope-checker + +| `score = max(0,100+Σ)` | `p-sufficient ⟺ floor(U) ⊑ acc(output)` +| (no locus) | `p-insufficient` + *witness edge* = first edge whose accumulated grade drops below the floor +| `breakdown : dict` | per-coordinate retention at each node +| `recommendStabilization(factor)` | human advice *attached to the witnessed edge* (now principled, not heuristic) +| `Stability.idr`: `score ∈ [0,100]` | grade soundness (`calculus.adoc` §8): declared grade never over-claims retention +|=== + +The witness is, by the calculus's own statement (§6.2), "the trope-particularity +analogue of the invariant-path argmin" — the same argmin shape `Stability.idr` +already reasons about. The verdict thus _subsumes_ the current score: the score is +recoverable as a projection, but the verdict additionally names the edge to repair. + +== Architecture: reference, never vendor + +[cols="1,3",options="header"] +|=== +| Concern | Decision + +| Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary"). +| Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`. +| New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics. +| Precedent | The same trust-tagged "fold external prover output back into our report" pattern the panic-attack repo uses in its `aggregate/` module. +| Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer. +|=== + +== O2 — lowering-correctness obligations (ours to discharge) + +The trope-checker proves the *composition* of grades is sound. It explicitly does +**not** prove that an Error-Lang construct lowered to effect `X` _is_ an `X` +(`calculus.adoc` §8, firewall 2; §10-O2). Those are our proof obligations: + +[cols="1,4",options="header"] +|=== +| ID | Obligation + +| *L-Echo* | `OpEchoToResidue` (`VM.res`) semantically _is_ `detach`: the witness becomes unreachable ⇒ `bond=Severed`; output reachability survives ⇒ `fate(quality)=Present`. **Open decision:** is residue's quality `Present`, or `Attenuated(δ)` (only "reachability", not full `y`)? This must be fixed before Phase 1 freezes the lowering. +| *L-Grade* | Each `stabilityFactor`'s grade is a *faithful over-approximation* of the real loss (grade-soundness direction: never claim more retention than occurs). The current `stabilityImpact` magnitudes are heuristic; for soundness `δ` must be a conservative loss bound. +| *L-Silent* | The `Conflated` lowering of `GlobalState`/`RaceCondition` is correct only when the merge is genuinely untagged. If a provenance tag is recoverable, we MUST emit `Fused(τ)` instead; emitting `Conflated` for a tractable merge is a false positive. +| *L-Floor* | The `use_model` floor Error-Lang emits faithfully encodes the program's declared stability requirement (per-function loss signatures, §7 "Declared signatures at the boundaries"). +|=== + +These mirror, in Error-Lang's setting, the open obligations the calculus states for +itself (O1–O4) — and they are checkable with the *same* Idris2 discipline already +used in `src/abi/`. + +== Phasing + +[cols="1,3",options="header"] +|=== +| Phase | Work + +| *0 (now)* | Shape the AffineScript Echo types (during the ReScript→AffineScript port) so `Echo`/`EchoR`/`echo_to_residue` lower cleanly to `Trope`/`FloatingQuality`/`detach`. This document + cross-references. *No new runtime coupling.* +| *1* | Implement the `trope` lowering backend for the Echo operations only (the tightest correspondence). Emit schema-valid IR; conformance-test against `trope-checker/tests/conformance/fixtures/`. +| *2* | Lower `stabilityFactor` → grade and emit a `use_model`; surface the verdict + witness as diagnostics alongside (then in place of) the scalar score. +| *3* | Discharge L-Echo / L-Grade / L-Silent / L-Floor as Idris2/Agda proofs; CI-gate the lowering. +|=== + +== Open questions + +* *Profile.* Adopt `prevent` (silent merges rejected at validation — strongest, and + on-message for "decomposition must be visible") or `detect` (representable, caught + at the verdict)? This design assumes `prevent`. +* *Residue fidelity* (L-Echo): `Present` vs `Attenuated(δ)` for `echo_to_residue`. +* *Floor authorship.* Where do use-models come from — a whole-program default, or + per-function loss-signature annotations the learner writes? +* *Coverage* (calculus O1): are all eight `stabilityFactor`s expressible with the + six writable effects? The table above is a well-chosen mapping, not yet a theorem. + +== See also + +* `docs/Echo-Decomposition.adoc` — the three decomposition planes this builds on. +* `docs/Design-Philosophy.adoc` — consequence amplification and the stability score. +* `spec/type-system.md` §7 — typing rules and the `[Stab-Erase]` stability debit. +* `src/abi/Stability.idr` — the existing Idris2 bound proof (verdict-soundness anchor). +* External (referenced, not vendored): + https://github.com/hyperpolymath/trope-checker[trope-checker] (`spec/calculus.adoc`, + `spec/trope-ir.adoc`, `schemas/trope-ir.schema.json`), + https://github.com/hyperpolymath/trope-particularity-workbench[trope-particularity-workbench] + (the nine effects), https://github.com/hyperpolymath/echo-types[echo-types] (shared substrate). diff --git a/patches/README.adoc b/patches/README.adoc new file mode 100644 index 0000000..f5711c1 --- /dev/null +++ b/patches/README.adoc @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += AffineScript toolchain patches +:toc: + +Patches applied to a fresh `hyperpolymath/affinescript` checkout by +`scripts/install-affinescript-toolchain.sh` before building the compiler, to +support the ReScript -> AffineScript migration. Each is a stop-gap pending +upstream; drop it from the install script once upstreamed. + +== affinescript-module-struct-fields.patch + +*Problem.* AffineScript's module resolver exported imported *enum* constructors +but dropped imported *struct/alias* type definitions: `lib/resolve.ml` registered +`TyEnum` variant constructors for imported modules but had a bare +`| TyAlias _ | TyStruct _ | TyExtern -> ()`. Field access on an imported struct +therefore failed with `Field 'x' not found in type T` — the named type stayed an +opaque `TCon` and never expanded to its `TRecord`. + +This blocked a per-module `.res -> .affine` port: the shared AST in +`compiler/src/Types.affine` (`Location`, `Token`, `Position`, ...) is +field-accessed by every other compiler module. + +*Fix.* Thread imported modules' `type_env` (struct/alias/enum type definitions) +and `constructor_env` into the importing module's type-check context, mirroring +the existing `name_types` (scheme) threading that already made enums cross: + +* `lib/typecheck.ml` — `check_program` gains `?import_type_env` / + `?import_constructor_env`, seeding `ctx.type_env` / `ctx.constructor_env`. +* `lib/resolve.ml` — a new `import_type_defs` copies a resolved module's + `type_env` / `constructor_env` into the destination context, called from all + three import forms (`use M;`, `use M::{...}`, `use M::*`); the imported-module + check site passes the new params. +* `bin/main.ml` — the `check` / `compile` / `eval` entry points pass the threaded + `type_env` / `constructor_env` to `check_program`. + +*Verification.* A module importing a struct and accessing its (nested) fields, +constructing it, and matching on an imported enum field now type-checks; existing +stdlib cross-module imports (`http_fetch`, `option`, `io`) still pass. + +*Upstream.* This belongs in `hyperpolymath/affinescript` — it fixes any multi-file +AffineScript program, not only error-lang. It could not be pushed from the +migration session (affinescript was outside the session's repo scope); upstream +when convenient, then delete this patch and its hook in the install script. diff --git a/patches/affinescript-module-struct-fields.patch b/patches/affinescript-module-struct-fields.patch new file mode 100644 index 0000000..54aae35 --- /dev/null +++ b/patches/affinescript-module-struct-fields.patch @@ -0,0 +1,142 @@ +diff --git a/bin/main.ml b/bin/main.ml +index 8230ab2..b772a3c 100644 +--- a/bin/main.ml ++++ b/bin/main.ml +@@ -195,6 +195,8 @@ let check_file face json path = + resolve_refs := List.rev resolve_ctx.references; + (match Affinescript.Typecheck.check_program + ~import_types:type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + add (Affinescript.Json_output.of_type_error e) +@@ -242,6 +244,8 @@ let check_file face json path = + | Ok (resolve_ctx, type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + Format.eprintf "@[%s@]@." +@@ -505,6 +509,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc + | Ok (resolve_ctx, import_type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:import_type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + add (Affinescript.Json_output.of_type_error e) +@@ -732,6 +738,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc + | Ok (resolve_ctx, import_type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:import_type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + Format.eprintf "@[%s@]@." +diff --git a/lib/resolve.ml b/lib/resolve.ml +index 65a6b48..65a9206 100644 +--- a/lib/resolve.ml ++++ b/lib/resolve.ml +@@ -654,6 +654,20 @@ let import_specific_items + Error (UndefinedVariable item.ii_name, item.ii_name.span) + ) (Ok ()) items + ++(** Thread imported struct/alias/enum type definitions and value constructors ++ from a resolved source module into the destination type-check context, so ++ that field access on an imported struct resolves (companion to the scheme ++ imports above — a struct needs its TRecord definition, not just a ++ name_types scheme). *) ++let import_type_defs ++ (dest : Typecheck.context) (source : Typecheck.context) : unit = ++ Hashtbl.iter (fun name ty -> ++ Hashtbl.replace dest.Typecheck.type_env name ty ++ ) source.Typecheck.type_env; ++ Hashtbl.iter (fun name ty -> ++ Hashtbl.replace dest.Typecheck.constructor_env name ty ++ ) source.Typecheck.constructor_env ++ + (** Resolve imports in a program using module loader *) + let rec resolve_and_typecheck_module + (loader : Module_loader.t) +@@ -698,7 +712,10 @@ let rec resolve_and_typecheck_module + imported modules must check the same way top-level programs do.) *) + match + Typecheck.check_program +- ~import_types:type_ctx.Typecheck.name_types symbols prog ++ ~import_types:type_ctx.Typecheck.name_types ++ ~import_type_env:type_ctx.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Typecheck.constructor_env ++ symbols prog + with + | Ok final_ctx -> Ok (symbols, final_ctx) + | Error type_err -> +@@ -729,6 +746,7 @@ and resolve_imports_with_loader + mod_type_ctx.Typecheck.var_types + mod_type_ctx.Typecheck.name_types + alias_str; ++ import_type_defs type_ctx mod_type_ctx; + Ok () + | Error e -> Error e + end +@@ -747,13 +765,15 @@ and resolve_imports_with_loader + (* Resolve and type-check the module *) + begin match resolve_and_typecheck_module loader loaded_mod with + | Ok (mod_symbols, mod_type_ctx) -> +- import_specific_items ctx.symbols ++ let* () = import_specific_items ctx.symbols + type_ctx.Typecheck.var_types + type_ctx.Typecheck.name_types + mod_symbols + mod_type_ctx.Typecheck.var_types + mod_type_ctx.Typecheck.name_types +- items ++ items in ++ import_type_defs type_ctx mod_type_ctx; ++ Ok () + | Error e -> Error e + end + | Error (Module_loader.ModuleNotFound _) -> +@@ -785,6 +805,7 @@ and resolve_imports_with_loader + sym) + | _ -> () + ) mod_symbols.all_symbols; ++ import_type_defs type_ctx mod_type_ctx; + Ok () + | Error e -> Error e + end +diff --git a/lib/typecheck.ml b/lib/typecheck.ml +index e38e302..4390c71 100644 +--- a/lib/typecheck.ml ++++ b/lib/typecheck.ml +@@ -2401,6 +2401,8 @@ let populate_call_effects (ctx : context) (prog : Ast.program) : unit = + Effect_sites.set_async_by_ord async_tbl + + let check_program ?(import_types : (string, scheme) Hashtbl.t option) ++ ?(import_type_env : (string, ty) Hashtbl.t option) ++ ?(import_constructor_env : (string, ty) Hashtbl.t option) + (symbols : Symbol.t) (prog : Ast.program) + : (context, type_error) Result.t = + try +@@ -2423,6 +2425,17 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option) + Option.iter (fun tbl -> + Hashtbl.iter (fun name sc -> Hashtbl.replace ctx.name_types name sc) tbl + ) import_types; ++ (* Thread imported struct/alias/enum type definitions (type_env) and value ++ constructors (constructor_env) so field access on an imported struct ++ resolves: enums already cross via name_types schemes, but a struct's ++ TRecord definition must be present for a named param type to expand to ++ its fields (otherwise it stays an opaque TCon -> FieldNotFound). *) ++ Option.iter (fun tbl -> ++ Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.type_env name ty) tbl ++ ) import_type_env; ++ Option.iter (fun tbl -> ++ Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.constructor_env name ty) tbl ++ ) import_constructor_env; + (* Forward pass: register all types, effects, traits, impls, and + function signatures so that mutually recursive declarations resolve. *) + let* () = List.fold_left (fun acc decl -> diff --git a/scripts/install-affinescript-toolchain.sh b/scripts/install-affinescript-toolchain.sh new file mode 100755 index 0000000..3b4e694 --- /dev/null +++ b/scripts/install-affinescript-toolchain.sh @@ -0,0 +1,57 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# install-affinescript-toolchain.sh — build & install the AffineScript compiler +# (hyperpolymath/affinescript, the OCaml/dune compiler) so error-lang's `.affine` +# sources — which replace the legacy ReScript per the Hyperpolymath language +# policy — can be typechecked and compiled. +# +# Why build from distro OCaml packages instead of opam: some CI/network policies +# block opam.ocaml.org. Every dependency below is available from the Debian/Ubuntu +# archive at a version satisfying affinescript's dune-project constraints +# (notably ocaml-dune 3.14 == `(lang dune 3.14)`). +# +# Network note: this clones github.com/hyperpolymath/affinescript directly; run it +# where GitHub is reachable (a normal CI runner or dev box). +set -euo pipefail + +AFFINE_REPO="${AFFINE_REPO:-https://github.com/hyperpolymath/affinescript}" +AFFINE_SRC="${AFFINE_SRC:-${TMPDIR:-/tmp}/affinescript}" +PREFIX="${PREFIX:-/usr/local}" +SUDO="$(command -v sudo || true)" + +# 1. OCaml toolchain + AffineScript build dependencies. +$SUDO apt-get update +$SUDO apt-get install -y \ + ocaml-dune menhir libmenhir-ocaml-dev libsedlex-ocaml-dev \ + libppx-deriving-ocaml-dev libppx-sexp-conv-ocaml-dev libsexplib0-ocaml-dev \ + libfmt-ocaml-dev libcmdliner-ocaml-dev libyojson-ocaml-dev \ + libppxlib-ocaml-dev libjs-of-ocaml-dev + +# 2. Fetch the compiler. +[ -d "$AFFINE_SRC/.git" ] || git clone --depth 1 "$AFFINE_REPO" "$AFFINE_SRC" + +# 2a. Apply the module-resolver fix (export imported struct field definitions so +# cross-module struct field access type-checks) until it is upstreamed to +# affinescript. See patches/README.adoc. Idempotent: skipped if already applied. +PATCH="$(cd "$(dirname "$0")/.." && pwd)/patches/affinescript-module-struct-fields.patch" +if [ -f "$PATCH" ] && git -C "$AFFINE_SRC" apply --check "$PATCH" 2>/dev/null; then + git -C "$AFFINE_SRC" apply "$PATCH" && echo "applied $PATCH" +else + echo "module-struct-fields patch: already applied or not applicable — continuing" +fi + +# 3. Build the compiler binary. +( cd "$AFFINE_SRC" && dune build bin/main.exe ) + +# 3. Install the binary + stdlib. The module loader discovers the stdlib at +# /../share/affinescript/stdlib, so this needs no env var. +$SUDO install -m755 "$AFFINE_SRC/_build/default/bin/main.exe" "$PREFIX/bin/affinescript" +$SUDO mkdir -p "$PREFIX/share/affinescript" +$SUDO rm -rf "$PREFIX/share/affinescript/stdlib" +$SUDO cp -r "$AFFINE_SRC/stdlib" "$PREFIX/share/affinescript/stdlib" + +echo "Installed: $(command -v affinescript)" +affinescript check "$AFFINE_SRC/examples/hello.affine" || true +echo "AffineScript toolchain installed under $PREFIX." diff --git a/src/abi/Foreign.idr b/src/abi/Foreign.idr index f3158df..1bfa14a 100644 --- a/src/abi/Foreign.idr +++ b/src/abi/Foreign.idr @@ -9,13 +9,39 @@ ||| All functions have type signatures and safety guarantees proven at ||| compile-time through dependent types. -module ErrorLang.ABI.Foreign - -import ErrorLang.ABI.Types -import ErrorLang.ABI.Layout +module Foreign %default total +-------------------------------------------------------------------------------- +-- Minimal ABI value types (inlined so this binding module is self-contained +-- and independently checkable: `idris2 --check Foreign.idr` from src/abi). +-- The previous external `ErrorLang.ABI.Types` / `ErrorLang.ABI.Layout` modules +-- were removed. The fabricated "Safety Proofs" that lived here -- which used +-- `cast ()` / `cast Refl` over IO actions to manufacture evidence -- have been +-- replaced by genuine, machine-checked proofs in the sibling modules +-- Stability.idr, Positional.idr and Paradox.idr. +-- +-- This file is a BINDING-DECLARATION layer only: it declares the C ABI of the +-- Zig haptics library (ffi/zig). It asserts no theorems. +-------------------------------------------------------------------------------- + +||| Result codes (must match the Zig `Result` enum in ffi/zig/src/main.zig). +public export +data Result = Ok | Error | InvalidParam | OutOfMemory | NullPointer + +||| Opaque handle to a library instance (wraps the C pointer as Bits64). +public export +record Handle where + constructor MkHandle + handlePtr : Bits64 + +||| Build a handle from a raw pointer; a null (0) pointer yields Nothing. +export +createHandle : Bits64 -> Maybe Handle +createHandle 0 = Nothing +createHandle p = Just (MkHandle p) + -------------------------------------------------------------------------------- -- Library Lifecycle -------------------------------------------------------------------------------- @@ -234,50 +260,18 @@ isInitialized h = do pure (result /= 0) -------------------------------------------------------------------------------- --- Safety Proofs +-- Safety properties -------------------------------------------------------------------------------- - -||| Theorem: Stability scores are always bounded [0, 100] -||| -||| Proof: The Zig implementation validates all score inputs in -||| error_lang_set_stability_factor, rejecting any value < 0 or > 100. -||| The weighted average in error_lang_calculate_stability preserves -||| this bound through convex combination. -export -stabilityBounded : (h : Handle) -> (factor : Bits8) -> - IO (Either Result (score : Double ** (0.0 <= score, score <= 100.0))) -stabilityBounded h factor = do - score <- getStabilityFactor h factor - -- Runtime check (could be proven statically with refinement types) - if score >= 0.0 && score <= 100.0 - then pure (Right (score ** (cast (), cast ()))) - else pure (Left Error) - -||| Theorem: Positional operator behavior is deterministic -||| -||| Proof: For any given (line, column, operatorType) triple, the Zig -||| implementation always returns the same behavior. The calculation is -||| purely functional (column % n) with no hidden state. -export -positionalDeterministic : (h : Handle) -> (line, column : Bits32) -> (op : Bits8) -> - IO (b1 : Bits8 ** (b2 : Bits8 ** (b1 = b2))) -positionalDeterministic h line column op = do - b1 <- positionalOperator h line column op - b2 <- positionalOperator h line column op - -- In practice, should always be equal - pure (b1 ** (b2 ** cast Refl)) - -||| Theorem: Paradox detection is monotonic with respect to code complexity -||| -||| As lineCount, varCount, or depth increase, the set of detected paradoxes -||| (represented as a bitmask) cannot decrease. -export -paradoxMonotonic : (h : Handle) -> - (lc1, lc2, vc1, vc2, d1, d2 : Bits32) -> - (lc1 <= lc2) -> (vc1 <= vc2) -> (d1 <= d2) -> - IO (p1 : Bits32 ** (p2 : Bits32 ** ((p1 .&. p2) = p1))) -paradoxMonotonic h lc1 lc2 vc1 vc2 d1 d2 _ _ _ = do - p1 <- detectParadoxes h lc1 vc1 d1 - p2 <- detectParadoxes h lc2 vc2 d2 - -- Monotonicity should hold in practice (bitwise subset) - pure (p1 ** (p2 ** cast Refl)) +-- The properties this ABI relies on are proved -- genuinely, with no escape +-- hatch and machine-checked under Idris2 0.8.0 -- in the sibling modules, NOT +-- here: +-- * stability score in [0,100] -> Stability.idr (stabilityUpperBound) +-- * positional operator determinism -> Positional.idr (positionalDeterministic) +-- * paradox-factor monotonicity -> Paradox.idr (superpositionMonotone, +-- temporalMonotone) +-- +-- The earlier `stabilityBounded` / `positionalDeterministic` / `paradoxMonotonic` +-- definitions here were unsound: they used `cast ()` / `cast Refl` over `IO` +-- actions to fabricate evidence. Removed 2026-06-23. Proving the third one +-- honestly also revealed that the *global* monotonicity claim is false of the +-- implementation -- scope leakage is prime-gated; see Paradox.idr. diff --git a/src/abi/Paradox.idr b/src/abi/Paradox.idr new file mode 100644 index 0000000..331c1ff --- /dev/null +++ b/src/abi/Paradox.idr @@ -0,0 +1,77 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Paradox-detection monotonicity (error-lang formal core, property 3 of 3). +||| +||| Mirrors the Zig FFI `error_lang_detect_paradoxes` +||| (`ffi/zig/src/main.zig`, lines 280-315), which sets: +||| * type_superposition when var_count > 10 (threshold; monotone) +||| * scope_leakage when isPrime(line) (prime-gated; NOT monotone) +||| * temporal_corruption when depth > 5 (threshold; monotone) +||| +||| HONEST FINDING. The previously-claimed blanket theorem "paradox detection +||| is monotonic with complexity" (README, WHITEPAPER §7, COMPLETION report) +||| is FALSE of the implementation: scope_leakage is gated on the PRIMALITY of +||| the line number, which is not monotone (line 7 is prime -> active; line 8 +||| is composite -> inactive, although 8 > 7). The original +||| `Foreign.idr :: paradoxMonotonic` hid this with `cast Refl`; attempting the +||| proof honestly surfaces that the blanket claim cannot hold. +||| +||| What IS true, and is proved here: the two THRESHOLD-gated factors are +||| monotone in their driving metric. The blanket claim is therefore retracted +||| in favour of these two component lemmas (see PROOF-NEEDS.md). Non-monotone +||| scope leakage is intentional -- it is the pedagogical point of the paradox. +||| +||| Self-contained; no escape hatches. Machine-check is a CI obligation. +module Paradox + +import Data.Nat + +%default total + +||| Transitivity of <= (self-contained; the standard definition). +lteTrans : LTE a b -> LTE b c -> LTE a c +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc p) (LTESucc q) = LTESucc (lteTrans p q) + +-- ─────────────────────────────────────────────────────────────────────── +-- Threshold-gated factors (monotone) +-- ─────────────────────────────────────────────────────────────────────── + +||| type_superposition fires when var_count exceeds 10 (11 <= var_count). +public export +SuperpositionActive : (varCount : Nat) -> Type +SuperpositionActive varCount = LTE 11 varCount + +||| temporal_corruption fires when depth exceeds 5 (6 <= depth). +public export +TemporalActive : (depth : Nat) -> Type +TemporalActive depth = LTE 6 depth + +||| THEOREM: type_superposition is monotone in var_count -- growing the +||| variable count never deactivates it. +public export +superpositionMonotone : (v1, v2 : Nat) -> LTE v1 v2 -> + SuperpositionActive v1 -> SuperpositionActive v2 +superpositionMonotone _ _ le active = lteTrans active le + +||| THEOREM: temporal_corruption is monotone in depth. +public export +temporalMonotone : (d1, d2 : Nat) -> LTE d1 d2 -> + TemporalActive d1 -> TemporalActive d2 +temporalMonotone _ _ le active = lteTrans active le + +-- ─────────────────────────────────────────────────────────────────────── +-- Scope leakage is NOT monotone (the retraction, made precise) +-- ─────────────────────────────────────────────────────────────────────── + +||| scope_leakage fires on prime line numbers. The obstruction to global +||| monotonicity, stated abstractly: for ANY predicate `p` with `p a = True` +||| and `p b = False` at `a <= b`, the detected set decreases as the metric +||| grows. Primality is such a `p` (witness a = 7, b = 8). Hence no global +||| monotonicity theorem exists -- and that is by design. +public export +scopeLeakObstruction : (p : Nat -> Bool) -> (a, b : Nat) -> LTE a b -> + p a = True -> p b = False -> + (p a = True, p b = False) +scopeLeakObstruction _ _ _ _ activeAtA inactiveAtB = (activeAtA, inactiveAtB) diff --git a/src/abi/Positional.idr b/src/abi/Positional.idr new file mode 100644 index 0000000..d175825 --- /dev/null +++ b/src/abi/Positional.idr @@ -0,0 +1,90 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Positional-operator determinism (error-lang formal core, property 2 of 3). +||| +||| Mirrors the Zig FFI `error_lang_positional_operator` +||| (`ffi/zig/src/main.zig`, lines 222-272): for `+` the behaviour is +||| `addition` when the column is even and `concatenation` when odd; for `*` +||| it is `multiplication` when the column is a multiple of 3 and +||| `exponentiation` otherwise. +||| +||| THEOREM. Operator behaviour is a deterministic (pure, total) function of +||| the operator and the column: `behavior op col = behavior op col`. +||| +||| This is `Refl` -- *because* the model is a pure total function. That is +||| exactly the point: the previous `Foreign.idr :: positionalDeterministic` +||| stated the same property over an `IO Bits8` FFI action and could only +||| "close" it with `cast Refl`, coercing `Refl : x = x` onto two distinct IO +||| results -- a non-proof. Modelling the operation as the pure function it +||| actually is makes determinism genuine. +||| +||| Self-contained; no escape hatches. Machine-check is a CI obligation. +||| +||| NOTE (conformance). `compiler/src/Stability.res` uses a *different* rule +||| (`(line*31+column) mod 4`, four-way). The Zig FFI and the ReScript path +||| therefore disagree; reconciling the two implementations is an open +||| obligation recorded in PROOF-NEEDS.md. +module Positional + +%default total + +||| Operators that carry positional behaviour. +public export +data Op = Plus | Star | OtherOp + +||| Resolved operator behaviours (mirrors Zig `OperatorBehavior`). +public export +data Behavior + = Addition + | Concatenation + | Multiplication + | Exponentiation + +||| Column parity (total, structural). +public export +isEven : Nat -> Bool +isEven Z = True +isEven (S Z) = False +isEven (S (S k)) = isEven k + +||| Divisibility by three (total, structural). +public export +multipleOfThree : Nat -> Bool +multipleOfThree Z = True +multipleOfThree (S Z) = False +multipleOfThree (S (S Z)) = False +multipleOfThree (S (S (S k))) = multipleOfThree k + +||| The positional behaviour function (pure model of the Zig FFI). +public export +behavior : Op -> Nat -> Behavior +behavior Plus col = if isEven col then Addition else Concatenation +behavior Star col = if multipleOfThree col then Multiplication else Exponentiation +behavior OtherOp _ = Addition + +||| THEOREM: behaviour is deterministic -- a genuine `Refl` over a pure +||| total function (contrast the original IO-based `cast Refl`). +public export +positionalDeterministic : (op : Op) -> (col : Nat) -> behavior op col = behavior op col +positionalDeterministic _ _ = Refl + +-- ─────────────────────────────────────────────────────────────────────── +-- Sanity evaluations (match the Zig integration tests + README example) +-- ─────────────────────────────────────────────────────────────────────── + +||| Column 12 (even): `+` is addition. (Zig test "positional semantics".) +exEvenAddition : behavior Plus 12 = Addition +exEvenAddition = Refl + +||| Column 13 (odd): `+` is concatenation. +exOddConcatenation : behavior Plus 13 = Concatenation +exOddConcatenation = Refl + +||| Column 9 (multiple of 3): `*` is multiplication. +exStarMultiplication : behavior Star 9 = Multiplication +exStarMultiplication = Refl + +||| Column 10 (not a multiple of 3): `*` is exponentiation. +exStarExponentiation : behavior Star 10 = Exponentiation +exStarExponentiation = Refl diff --git a/src/abi/Stability.idr b/src/abi/Stability.idr new file mode 100644 index 0000000..7ce3617 --- /dev/null +++ b/src/abi/Stability.idr @@ -0,0 +1,120 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Stability-score bound (error-lang formal core, property 1 of 3). +||| +||| Mirrors the stability calculation in `compiler/src/Types.res` +||| (`stabilityImpact` / `calculateStability`, lines 258-274). +||| +||| THEOREM. The stability score is always within [0, 100]. +||| +||| The ReScript `calculateStability` computes `Int.max(0, 100 + penalties)` +||| where every penalty is non-positive — i.e. `max(0, 100 - totalPenalty)`. +||| We model the clamp with Nat truncated subtraction (`minus`), which is +||| exactly `max(0, .)`: `minus 100 p` is 0 once `p >= 100`. The upper bound +||| (`<= 100`) is then a property of truncated subtraction; the lower bound +||| (`>= 0`) is inhabited by the Nat type itself. +||| +||| This module is self-contained (only `Data.Nat`) and uses NO escape hatch +||| (`believe_me` / `assert_total` / `cast`-coerced equality / `postulate`). +||| It replaces the previous `Foreign.idr :: stabilityBounded`, which faked +||| the bound with `cast ()` over an `IO` action. +||| +||| Status: written to typecheck under Idris2 (>= 0.7.0). Machine-check is a +||| CI obligation (no idris2 in the current dev image). See PROOF-NEEDS.md. +module Stability + +import Data.Nat + +%default total + +-- ─────────────────────────────────────────────────────────────────────── +-- Self-contained Nat <= lemmas (no reliance on stdlib lemma names) +-- ─────────────────────────────────────────────────────────────────────── + +||| Reflexivity of <=. +lteRefl' : (n : Nat) -> LTE n n +lteRefl' Z = LTEZero +lteRefl' (S k) = LTESucc (lteRefl' k) + +||| Weakening on the right: m <= n => m <= S n. +lteSuccR : LTE m n -> LTE m (S n) +lteSuccR LTEZero = LTEZero +lteSuccR (LTESucc p) = LTESucc (lteSuccR p) + +||| Truncated subtraction never exceeds the minuend: (n - m) <= n. +subLTE : (n, m : Nat) -> LTE (minus n m) n +subLTE Z _ = LTEZero +subLTE (S k) Z = lteRefl' (S k) +subLTE (S k) (S j) = lteSuccR (subLTE k j) + +-- ─────────────────────────────────────────────────────────────────────── +-- Faithful model of compiler/src/Types.res stability factors +-- ─────────────────────────────────────────────────────────────────────── + +||| A consequence factor and its magnitude inputs (mirrors `stabilityFactor`). +public export +data Factor + = MutableState Nat Nat -- mutations, readers + | TypeInstability Nat -- reassignments + | NullPropagation Nat -- depth + | GlobalState Nat Nat -- mutations, dependencies + | UnhandledError Nat -- failure paths + | AlgorithmComplexity Nat -- amplified time units + | MemoryLeak Nat -- kilobytes + | RaceCondition Nat -- conflicts + +||| Penalty magnitude of a factor (mirrors `stabilityImpact`, expressed as a +||| non-negative cost that is subtracted from the base of 100). +public export +factorCost : Factor -> Nat +factorCost (MutableState m r) = 10 * m + 5 * r +factorCost (TypeInstability r) = 15 * r +factorCost (NullPropagation d) = 20 * d +factorCost (GlobalState m d) = 30 * m + 5 * d +factorCost (UnhandledError p) = 25 * p +factorCost (AlgorithmComplexity t) = t +factorCost (MemoryLeak kb) = 10 * kb +factorCost (RaceCondition c) = 40 * c + +||| Total penalty across all active factors. +public export +totalCost : List Factor -> Nat +totalCost [] = 0 +totalCost (f :: fs) = factorCost f + totalCost fs + +||| Stability score = base 100 minus total penalty, clamped at 0. +||| (Nat `minus` is truncated, modelling `Int.max(0, 100 + penalties)`.) +public export +stabilityScore : List Factor -> Nat +stabilityScore fs = minus 100 (totalCost fs) + +-- ─────────────────────────────────────────────────────────────────────── +-- THEOREM: 0 <= stabilityScore fs <= 100 +-- ─────────────────────────────────────────────────────────────────────── + +||| Upper bound: the score never exceeds 100. +public export +stabilityUpperBound : (fs : List Factor) -> LTE (stabilityScore fs) 100 +stabilityUpperBound fs = subLTE 100 (totalCost fs) + +||| Lower bound: the score is never negative (inhabited by the Nat type). +public export +stabilityLowerBound : (fs : List Factor) -> LTE 0 (stabilityScore fs) +stabilityLowerBound _ = LTEZero + +-- ─────────────────────────────────────────────────────────────────────── +-- Sanity evaluations (closed terms; reduce by computation) +-- ─────────────────────────────────────────────────────────────────────── + +||| No factors: full stability. +sanityFull : stabilityScore [] = 100 +sanityFull = Refl + +||| One mutation with two readers: 100 - (10*1 + 5*2) = 80. +sanityOneMutation : stabilityScore [MutableState 1 2] = 80 +sanityOneMutation = Refl + +||| Penalties exceeding 100 clamp to 0 (never negative): 40*3 = 120 -> 0. +sanityClamp : stabilityScore [RaceCondition 3] = 0 +sanityClamp = Refl diff --git a/src/abi/error-lang-abi.ipkg b/src/abi/error-lang-abi.ipkg new file mode 100644 index 0000000..97a8168 --- /dev/null +++ b/src/abi/error-lang-abi.ipkg @@ -0,0 +1,14 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +-- The error-lang formal core + ABI binding layer. +-- Build/typecheck: idris2 --typecheck error-lang-abi.ipkg (from src/abi) +-- or per-module: idris2 --check Stability.idr (from src/abi) +package error-lang-abi +version = 0.1.0 +authors = "Jonathan D.A. Jewell" +sourcedir = "." +modules = Stability + , Positional + , Paradox + , Foreign diff --git a/verification/check-affinescript.sh b/verification/check-affinescript.sh new file mode 100755 index 0000000..549602e --- /dev/null +++ b/verification/check-affinescript.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-affinescript.sh — typecheck every ported `.affine` compiler source with +# the AffineScript compiler. Companion to verification/check-proofs.sh. +# Requires `affinescript` on PATH (see scripts/install-affinescript-toolchain.sh). +set -euo pipefail + +# Check from compiler/src so sibling-module imports (`use Types::{...}`) resolve +# via the loader's current-dir search. +cd "$(dirname "$0")/../compiler/src" + +if ! command -v affinescript >/dev/null 2>&1; then + echo "affinescript not found — run scripts/install-affinescript-toolchain.sh" >&2 + exit 127 +fi + +shopt -s nullglob +sources=(*.affine) +if [ ${#sources[@]} -eq 0 ]; then + echo "no .affine sources yet (ReScript->AffineScript migration in progress)." + exit 0 +fi + +fail=0 +for f in "${sources[@]}"; do + printf 'checking %-28s ... ' "$f" + if affinescript check "$f" >/tmp/as_check.out 2>&1; then + echo ok + else + echo FAIL + cat /tmp/as_check.out + fail=1 + fi +done + +if [ "$fail" -eq 0 ]; then + echo "all .affine sources check." +else + echo "affinescript check failures." >&2 + exit 1 +fi diff --git a/verification/check-proofs.sh b/verification/check-proofs.sh new file mode 100755 index 0000000..ba97369 --- /dev/null +++ b/verification/check-proofs.sh @@ -0,0 +1,41 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# Machine-check the error-lang formal core (src/abi/*.idr) with Idris2. +# +# Requires idris2 >= 0.8.0 on PATH. Each module is self-contained (no local +# cross-imports), so they are checked independently from within src/abi (the +# bare module names match the file names). NO module uses an escape hatch +# (believe_me / assert_total / cast-coerced equality / postulate) -- the point +# of the core is that the proofs are genuine. +set -euo pipefail + +ABI_DIR="$(cd "$(dirname "$0")/../src/abi" && pwd)" + +if ! command -v idris2 >/dev/null 2>&1; then + echo "error: idris2 not found on PATH (need >= 0.8.0)." >&2 + echo "build it from source via Chez Scheme (see PROOF-NEEDS.md), then re-run." >&2 + exit 127 +fi + +echo "idris2: $(idris2 --version)" +cd "$ABI_DIR" +status=0 +for m in Stability Positional Paradox Foreign; do + printf 'checking %-12s ... ' "$m" + if idris2 --check "$m.idr" >/dev/null 2>&1; then + echo ok + else + echo FAIL + idris2 --check "$m.idr" || true + status=1 + fi +done + +if [ "$status" -eq 0 ]; then + echo "all proofs check." +else + echo "one or more proofs failed to check." >&2 +fi +exit "$status"