Skip to content

Commit 4ae38b1

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into proof-debt/standards-134-coq-preservation-admit
2 parents ec1e816 + 9bcde6c commit 4ae38b1

6 files changed

Lines changed: 757 additions & 0 deletions

File tree

‎.github/workflows/abi-verify.yml‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# abi-verify.yml — machine-checks the Ephapax Rust↔SPARK ABI seam.
5+
#
6+
# The seam (src/abi/Ephapax/ABI/{Types,Foreign,Invariants}.idr) states
7+
# the correctness-critical invariants E1–E6 (see PROOF-NEEDS.md and
8+
# RUST-SPARK-STANCE.adoc). Some properties have discharged proofs in
9+
# the broader formalisation (cited from Invariants.idr — e.g.
10+
# `splitLinearCoverage`, `noEscapeTheorem`); the rest are explicit
11+
# erased OWED obligations.
12+
#
13+
# This gate exists so the discharged proofs cannot silently regress
14+
# and an OWED postulate cannot quietly become a `believe_me`. Mirrors
15+
# the proof-of-work `abi-verify.yml` (snazzybucket/idris2 container,
16+
# the estate-standard image). HARD GATE.
17+
18+
name: ABI Seam Verification
19+
20+
on:
21+
pull_request:
22+
paths:
23+
- 'src/abi/**'
24+
- '.github/workflows/abi-verify.yml'
25+
push:
26+
branches: [main]
27+
paths:
28+
- 'src/abi/**'
29+
30+
permissions:
31+
contents: read
32+
33+
concurrency:
34+
group: ${{ github.workflow }}-${{ github.ref }}
35+
cancel-in-progress: true
36+
37+
jobs:
38+
idris2-abi:
39+
name: Idris2 ABI seam (ephapax-abi.ipkg)
40+
runs-on: ubuntu-latest
41+
container:
42+
image: snazzybucket/idris2:latest # estate-standard Idris2 image
43+
steps:
44+
- name: Checkout repository
45+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
46+
47+
- name: Build (typecheck) the ABI seam
48+
working-directory: src/abi
49+
run: |
50+
idris2 --version
51+
# --build typechecks every module in the .ipkg in dependency
52+
# order. A real regression (ill-typed lemma, a discharged
53+
# proof that stops reducing, a stray `?hole`/`believe_me`)
54+
# fails here. The intentional erased OWED postulates are
55+
# well-typed and do NOT fail the build — they are tracked in
56+
# PROOF-NEEDS.md, not hidden.
57+
idris2 --build ephapax-abi.ipkg

‎RUST-SPARK-STANCE.adoc‎

Lines changed: 182 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,182 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Rust/SPARK Stance — ephapax
3+
:toc: macro
4+
:toclevels: 2
5+
6+
toc::[]
7+
8+
== Summary
9+
10+
This repository implements a dyadic-linear programming language. The
11+
implementation is a 19-crate Rust pipeline (surface parser → discipline
12+
checker → IR → WASM backend, with a Zig FFI token buffer). Per the
13+
estate language policy
14+
(`standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc`
15+
§Terminology), *"Rust" means "Rust/SPARK"*: Rust is the primary
16+
implementation language now, but the project is *designed to admit
17+
SPARK/Ada verification modules* across a stable, Idris2-typed
18+
boundary, with Zig as the FFI layer. Rust here is never the ABI/API/FFI
19+
layer.
20+
21+
Before this PR (2026-05-20) the crate had a `formal/` Coq metatheory +
22+
a `src/formal/` Idris2 region/linearity metatheory + a `src/abi/`
23+
directory that did not exist — no named seam, no SPARK admission path,
24+
no stance doc. The `src/abi/` package below brings the project into
25+
structural compliance; the remaining proof work is tracked in
26+
`PROOF-NEEDS.md` and standards#134.
27+
28+
== What is correctness-critical here
29+
30+
This is a programming language whose claimed properties are *linear-type
31+
consumption*, *region safety*, *GC-freedom*, and *type preservation*.
32+
The boundaries where these can be silently broken are: the discipline
33+
check (typing pass), the IR lowering (qualifier erasure), the WASM
34+
backend (lowering to a different operational model), and the Zig FFI
35+
(non-typed integer marshalling).
36+
37+
[cols="1,2,3",options="header"]
38+
|===
39+
| Audit framing | Real counterpart | Where in code
40+
41+
| Type preservation
42+
| `well_typed t T && t ⇒ t' → well_typed t' T`
43+
| `formal/Semantics.v::preservation` (currently **`Admitted`** —
44+
earlier in-file comment claiming "Qed, closed 2026-04-27" was
45+
unsubstantiated; `coqc` rejects the proof script with remaining
46+
open goals — see ephapax#92).
47+
48+
| Linear consumption
49+
| Every linear binding used exactly once across a context split
50+
| `src/formal/Ephapax/Formal/Qualifier.idr::splitLinearCoverage`
51+
(DISCHARGED, MERGED 2026-05-19 via ephapax#85 — head/position form).
52+
Cross-control-flow form (conditionals, pattern-match arms, region
53+
exit) OWED.
54+
55+
| Region safety
56+
| Values scoped to `r` never escape `r` at runtime
57+
| `src/formal/Ephapax/Formal/RegionLinear.idr::noEscapeTheorem`
58+
(DISCHARGED — real proof, narrow form: `NoRegionInType r (Scoped r a)
59+
-> Void`). Operational form OWED.
60+
61+
| GC-freedom
62+
| No runtime collector needed — every heap value's lifetime is
63+
statically bounded by an enclosing region
64+
| `src/formal/Ephapax/Formal/RegionLinear.idr::noGCExtract`
65+
(**VACUOUS** — body is `(ne, lc)`, just returns its inputs; flagged
66+
in seam, real content OWED).
67+
68+
| WASM compilation correctness
69+
| Lowering preserves typing + semantics
70+
| `src/ephapax-wasm/` (no formalisation today — entire compiler
71+
metatheory OWED).
72+
|===
73+
74+
== The seam
75+
76+
[cols="1,3",options="header"]
77+
|===
78+
| File | Role
79+
80+
| `src/abi/Ephapax/ABI/Types.idr`
81+
| Idris2 boundary types — faithful total models of `Qual`, `Ty`, `Term`,
82+
`CtxEntry`/`TypeCtx`, `SExpr`, `WasmExpr`, `RegionId`. Constructor
83+
order is ABI-significant and matches the Rust enums in
84+
`src/ephapax-syntax/`, `src/ephapax-typing/`, `src/ephapax-ir/`,
85+
`src/ephapax-wasm/`.
86+
87+
| `src/abi/Ephapax/ABI/Invariants.idr`
88+
| Type-level statements of invariants E1–E6. **E2 head-form is
89+
DISCHARGED** at `Ephapax.Formal.Qualifier.splitLinearCoverage`
90+
(cited). **E3 narrow-form is DISCHARGED** at
91+
`Ephapax.Formal.RegionLinear.noEscapeTheorem` (cited). E1
92+
(preservation) is OWED on the Coq side and remains `Admitted`.
93+
E2 control-flow generalisation, E3 operational form, E4
94+
(no-runtime-GC), E5 (WASM compilation), E6 (IR lowering) are stated
95+
as erased postulates so the obligations are explicit and discoverable.
96+
Authoritative per-ID status: `PROOF-NEEDS.md` § Invariant register.
97+
98+
| `src/abi/Ephapax/ABI/Foreign.idr`
99+
| Zig/WASM-FFI boundary: u32/i32 range obligations for marshalling
100+
(function indices, local indices, literal magnitudes), the stable
101+
C-ABI `CompileResult` codes, and the contract tying a `CompileOk`
102+
return to an E5 `WasmTyped` certificate.
103+
104+
| `src/abi/ephapax-abi.ipkg`
105+
| Idris2 package mapping the `Ephapax.ABI.*` namespace to the source
106+
tree. Without this package the modules would not load
107+
(`import Ephapax.ABI.Types` would fail), so the seam would be
108+
structurally present but never machine-checked.
109+
|===
110+
111+
The seam is machine-checked: `idris2 --build ephapax-abi.ipkg` (run
112+
from `src/abi/`) typechecks all three modules, and a future
113+
`.github/workflows/abi-verify.yml` (filed alongside this seam) enforces
114+
it on every change to `src/abi/**`. The stated obligations therefore
115+
cannot silently regress, and an OWED postulate cannot quietly become
116+
a `believe_me`.
117+
118+
== Bounds encoding choice (Integer, not Nat)
119+
120+
`Foreign.idr` uses `Integer` for the u32/i32 bounds, not `Nat`. This
121+
is a deliberate carry-over from `proof-of-work#63`: a `Nat` constant
122+
of `2^32` placed under an `LT n bound` predicate inside a data
123+
constructor's type forces the Idris2 0.8.0 elaborator to reduce the
124+
literal to ~4×10⁹ `S` constructors during the data declaration's
125+
elaboration, which hangs `--build` indefinitely. The boundary
126+
predicate is `So (natToInteger n < bound)` instead — propositionally
127+
equivalent (the Rust `u32` round-trips to precisely the Nats with
128+
`natToInteger n < 2^32`) but without unary expansion. Do not rewrite
129+
back to `LT n bound`.
130+
131+
== SPARK/Ada admission path
132+
133+
The boundary is the Idris2 seam above. A future SPARK/Ada
134+
re-implementation of any of:
135+
136+
* the discipline checker (would discharge a refined E2),
137+
* the IR lowering (would discharge E6),
138+
* the WASM backend (would discharge E5),
139+
140+
sits on the far side of `Foreign.compileOkImpliesWasmTyped` without
141+
changing the contract: it must return `CompileOk` only when it can
142+
produce a `WasmTyped (compile t) T` certificate. No SPARK code exists
143+
yet; the seam exists so it *can* be added without redesign, which is
144+
exactly what §Terminology requires of a "designed to admit SPARK/Ada"
145+
Rust project.
146+
147+
== Honest gaps
148+
149+
* `formal/Semantics.v::preservation` is **`Admitted`** — the proof
150+
script at L3215–L3326 leaves residual open goals (`coqc` 8.18.0
151+
rejects `Qed.` with "Attempt to save an incomplete proof"). PR#87
152+
(earlier today) propagated an in-file comment's "Qed, closed
153+
2026-04-27" claim into ROADMAP + PROOF-NEEDS without running the
154+
build; **the comment was the lie**. ephapax#92 (open) reverts that
155+
doc drift and marks the source `Admitted.` honestly so the Coq CI
156+
goes green.
157+
* `src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract`
158+
and `noGCExtract` are **vacuous wrappers** — body is the input
159+
unchanged (`= ne`, `= (ne, lc)`). The proofs are sound (no escape
160+
hatches) but the *content* is vacuous: they don't establish region
161+
safety or GC-freedom, they just extract a witness already given.
162+
The honest seam invariants E3 (operational region-no-escape) and
163+
E4 (no-runtime-GC) are therefore OWED, not "complete".
164+
* No formalisation of WASM lowering exists anywhere in the repo. E5
165+
is the highest-leverage compiler-correctness gap.
166+
* `ephapax-parse-tests.ipkg` fails on origin/main
167+
(`testLexPositions` / `parseWithBuf` undefined). Independent of the
168+
seam, flagged here for awareness — separate issue.
169+
170+
== References
171+
172+
* `standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc`
173+
§Terminology, §"Rust is never the ABI"
174+
* `PROOF-NEEDS.md` (this repo) — invariant ledger and priorities
175+
* `ROADMAP.adoc` (this repo) — Coq/Idris2 dual formalisation status
176+
* Estate exemplar seam: `proof-of-work/src/abi/{Types,Foreign,Invariants}.idr`
177+
+ `RUST-SPARK-STANCE.adoc`
178+
* standards#134 — estate proof-debt sub-issue tracking ephapax
179+
* ephapax#85 — `splitLinearCoverage` discharge (MERGED 2026-05-19)
180+
* ephapax#88 — `idris2/src/*.idr` SPDX headers (OPEN)
181+
* ephapax#92 — `Qed.` → `Admitted.` on `preservation` (OPEN — companion
182+
to this PR; the doc-honesty fix this stance doc cites)

‎src/abi/Ephapax/ABI/Foreign.idr‎

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
||| SPDX-License-Identifier: PMPL-1.0-or-later
2+
||| Ephapax ABI: FFI Boundary Obligations
3+
|||
4+
||| The Zig/WASM-FFI side of the Ephapax ABI seam. The Rust pipeline
5+
||| uses fixed-width integers across two boundaries:
6+
||| 1. Zig FFI token buffer (`Ephapax.Parse.ZigBuffer` in the Idris2
7+
||| Parse package) — `u32` offsets/lengths into the input source.
8+
||| 2. WASM lowering (`src/ephapax-wasm/`) — `u32` function indices,
9+
||| `u32` local indices, `i32` literal values.
10+
|||
11+
||| The Idris2 model in Types.idr uses `Nat` for these. This module
12+
||| states the range obligations that the boundary must discharge when
13+
||| marshalling between the Rust representation and the typed model,
14+
||| plus the C-ABI result codes any FFI entry-point should expose.
15+
|||
16+
||| Per LANGUAGE-POLICY.adoc §Terminology and §"Rust is never the ABI":
17+
||| the boundary is Idris2 (this seam) + Zig (FFI). Rust/SPARK is the
18+
||| application logic on one side; a future SPARK/Ada code generator
19+
||| could sit on the other side of THIS contract without changing it.
20+
21+
module Ephapax.ABI.Foreign
22+
23+
import Ephapax.ABI.Types
24+
import Ephapax.ABI.Invariants
25+
import Data.Nat
26+
import Data.So
27+
28+
%default total
29+
30+
--------------------------------------------------------------------------------
31+
-- Fixed-width range obligations
32+
--
33+
-- Bounds are `Integer`, not `Nat` — the proof-of-work `Foreign.idr`
34+
-- learned the hard way (PR proof-of-work#63, 2026-05-20) that a `Nat`
35+
-- bound of 2^32 forces the Idris2 0.8.0 data-constructor elaborator to
36+
-- reduce the literal under `LT n bound` inside the constructor's type,
37+
-- which expands ~4×10^9 `S` ctors and hangs `--build`. The boundary
38+
-- predicate is therefore expressed as `So (natToInteger n < bound)`,
39+
-- propositionally equivalent (the Rust `u32` round-trips to precisely
40+
-- the Nats with `natToInteger n < 2^32`) but does not trigger unary
41+
-- expansion. Do not rewrite back to `LT n bound`.
42+
--------------------------------------------------------------------------------
43+
44+
||| u32 upper bound (2^32). WASM function indices, local indices and
45+
||| Zig token-buffer offsets/lengths crossing the FFI must fit; the
46+
||| Rust types guarantee this, the Idris2 Nat model does not, so the
47+
||| obligation is made explicit here.
48+
public export
49+
u32Max : Integer
50+
u32Max = 4294967296
51+
52+
||| Proof-carrying "this Nat fits in a u32".
53+
public export
54+
data InU32 : Nat -> Type where
55+
MkInU32 : (n : Nat) -> So (natToInteger n < Foreign.u32Max) -> InU32 n
56+
57+
||| i32 signed-range upper bound (2^31). WASM `i32.const` literals must
58+
||| fit; the magnitude bound below is the absolute value (sign is
59+
||| tracked separately by the producer).
60+
public export
61+
i32Max : Integer
62+
i32Max = 2147483648
63+
64+
public export
65+
data InI32Magnitude : Nat -> Type where
66+
MkInI32Mag : (n : Nat) -> So (natToInteger n < Foreign.i32Max) -> InI32Magnitude n
67+
68+
||| A WASM function index is FFI-marshalable iff it fits in u32.
69+
public export
70+
MarshalableFuncIdx : FuncIdx -> Type
71+
MarshalableFuncIdx fi = InU32 fi
72+
73+
--------------------------------------------------------------------------------
74+
-- C-ABI result codes for compile/typecheck entry points
75+
--------------------------------------------------------------------------------
76+
77+
||| Stable C integer result for a typecheck/compile call across the FFI.
78+
||| Constructor order is ABI-significant.
79+
public export
80+
data CompileResult : Type where
81+
CompileOk : CompileResult -- typecheck + lowering succeeded
82+
CompileTypeError : CompileResult -- discipline check rejected the term
83+
CompileRegionError : CompileResult -- region-safety check rejected the term
84+
CompileLowerError : CompileResult -- IR/WASM lowering failed (should never
85+
-- happen on a well-typed term — E6)
86+
CompileMalformed : CompileResult -- input failed surface parse
87+
88+
public export
89+
compileResultToInt : CompileResult -> Nat
90+
compileResultToInt CompileOk = 0
91+
compileResultToInt CompileTypeError = 1
92+
compileResultToInt CompileRegionError = 2
93+
compileResultToInt CompileLowerError = 3
94+
compileResultToInt CompileMalformed = 4
95+
96+
public export
97+
compileResultFromInt : Nat -> Maybe CompileResult
98+
compileResultFromInt 0 = Just CompileOk
99+
compileResultFromInt 1 = Just CompileTypeError
100+
compileResultFromInt 2 = Just CompileRegionError
101+
compileResultFromInt 3 = Just CompileLowerError
102+
compileResultFromInt 4 = Just CompileMalformed
103+
compileResultFromInt _ = Nothing
104+
105+
||| Round-trip proof for the result-code mapping (the one property
106+
||| fully dischargeable here, by case analysis).
107+
public export
108+
compileResultRoundTrip :
109+
(r : CompileResult) -> compileResultFromInt (compileResultToInt r) = Just r
110+
compileResultRoundTrip CompileOk = Refl
111+
compileResultRoundTrip CompileTypeError = Refl
112+
compileResultRoundTrip CompileRegionError = Refl
113+
compileResultRoundTrip CompileLowerError = Refl
114+
compileResultRoundTrip CompileMalformed = Refl
115+
116+
--------------------------------------------------------------------------------
117+
-- The FFI contract any compile entry-point must honour
118+
--------------------------------------------------------------------------------
119+
120+
||| The boundary obligation: a `CompileOk` result handed back across the
121+
||| FFI must be backed by an E5 `WasmTyped (compile t) T` certificate
122+
||| for the submitted term. This ties the C-ABI return value to the
123+
||| Idris2 compiler-correctness statement. The Rust does not yet
124+
||| *produce* the witness (PROOF-NEEDS.md E5); the type records exactly
125+
||| what is owed.
126+
public export
127+
0 compileOkImpliesWasmTyped :
128+
(g : TypeCtx) -> (t : Term) -> (T : Ty) ->
129+
(r : CompileResult) ->
130+
r = CompileOk ->
131+
WellTyped g t T ->
132+
WasmTyped (compile t) T

0 commit comments

Comments
 (0)