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/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-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"