Skip to content

Commit eb404ac

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proofs(idris2): Q1-C primitive-eq axiom pilot + equivRefl closure
Pilot for Q1 closure-path-C (believe_me axioms with CI allow-list). Lands the smallest possible footprint to demonstrate the unlock and gates further use behind a registry + CI check. New module: proofs/idris2/src/Filesystem/Axioms.idr * `axStringEqRefl : (s : String) -> (s == s) = True` `believe_me`-backed primitive-eq reflexivity. Operational reason: every Idris2 backend evaluates `prim__strEq s s` to True for any `s`; the type-checker cannot see through the primitive on opaque values. Same epistemic status as Agda funext or Coq Axiom is_empty_dir_dec (both already accepted). * `axBits8EqRefl : (b : Bits8) -> (b == b) = True` Same shape for the byte-level primitive. * `fileContentEqRefl : (xs : List Bits8) -> (xs == xs) = True` Derived (not an axiom) — structural induction over the list using axBits8EqRefl at the leaf. Model.idr — equivRefl closed (was ?equivReflProof) * `pathEqRefl` (structural induction over Path using axStringEqRefl) * `fsEntryEqRefl` (case-split on Dir / File with fileContentEqRefl) * `entryEqRefl` (tuple combinator) * Idris2 0.8.0's `elem` is `Foldable.any (==)` which desugars to a foldl form, not the textbook (x==y) || elem x ys recursion. The proof threads through foldlOrTrueIdempotent — once the accumulator hits True, the foldl stays True regardless of the tail. * `equivRefl` then derives via `allElemSelf` (every entry is in its own list under the propositional `Elem` witness). Hole inventory: 16 -> 15. CI guard: .github/scripts/check-idris2-believe-me.sh * Reject any believe_me in proofs/idris2/**/*.idr that is NOT in proofs/idris2/src/Filesystem/Axioms.idr. * Sanity-check: registered-axiom count matches the believe_me count in the allowed file. * Wired into idris-verification.yml as a pre-build gate. Registry: .machine_readable/IDRIS2_AXIOMS.a2ml * Single source of truth for the believe_me allow-list. * Each entry carries: type signature, operational justification, morally-equivalent existing axioms, downstream consumers. Tested locally: * `idris2 --build valence-shell.ipkg` exit 0 * Guard: 2 occurrences in Axioms.idr / 2 axioms in registry — pass * Guard rejection test (added believe_me in Model.idr): correctly flagged + script exits 1 PROOF-NEEDS.md reconciled: * Assumption Registry now lists the 2 Idris2 axioms. * Idris2 hole tally: 16 -> 15. * Model.idr row: equivReflProof moved from open to closed. Q4 policy implication: this commit takes Q4 option B (soft policy with named + gated axioms). If owner subsequently prefers option A (hard "never believe_me"), revert this commit + accept the Q1-B (Nat-interned Path) migration as the only path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 7c720a2 commit eb404ac

6 files changed

Lines changed: 330 additions & 3 deletions

File tree

‎.github/scripts/check-idris2-believe-me.sh‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
#
5+
# CI guard: reject any `believe_me` in proofs/idris2/**/*.idr that is
6+
# not in the registered allow-list at
7+
# .machine_readable/IDRIS2_AXIOMS.a2ml.
8+
#
9+
# Rationale: Q1-C pilot accepts named axiomatic uses of `believe_me`
10+
# (e.g. primitive-eq reflexivity) but blocks ad-hoc closures that
11+
# silently inject unsound assumptions.
12+
#
13+
# The allow-list is the single file `Filesystem.Axioms`. Any other
14+
# file using `believe_me` is a policy violation.
15+
16+
set -euo pipefail
17+
18+
REPO_ROOT="$(git rev-parse --show-toplevel)"
19+
cd "$REPO_ROOT"
20+
21+
PROOFS_DIR="proofs/idris2/src"
22+
ALLOWED_FILE="${PROOFS_DIR}/Filesystem/Axioms.idr"
23+
REGISTRY=".machine_readable/IDRIS2_AXIOMS.a2ml"
24+
25+
if [[ ! -d "$PROOFS_DIR" ]]; then
26+
echo "ERROR: $PROOFS_DIR not found — wrong working directory?" >&2
27+
exit 2
28+
fi
29+
30+
if [[ ! -f "$REGISTRY" ]]; then
31+
echo "ERROR: axiom registry $REGISTRY missing." >&2
32+
exit 2
33+
fi
34+
35+
# Find every believe_me occurrence in proofs/idris2/**/*.idr, excluding
36+
# comments. We grep with -nH so the output includes file:line markers
37+
# usable by reviewers + CI logs.
38+
violations=$(
39+
grep -rn --include='*.idr' '\bbelieve_me\b' "$PROOFS_DIR" \
40+
| grep -v '^[^:]*:[0-9]*:[[:space:]]*--' \
41+
| grep -v '^[^:]*:[0-9]*:[[:space:]]*|||' \
42+
| { grep -v "^${ALLOWED_FILE}:" || true; }
43+
)
44+
45+
if [[ -n "$violations" ]]; then
46+
echo "❌ Idris2 believe_me policy violation:"
47+
echo
48+
echo "$violations"
49+
echo
50+
echo "Policy (Q1-C, see $REGISTRY):"
51+
echo " - believe_me is ONLY allowed in $ALLOWED_FILE."
52+
echo " - To add a new axiom, edit $ALLOWED_FILE AND $REGISTRY together."
53+
echo " - For any other proof, redesign the theorem-shape rather"
54+
echo " than close with believe_me (see #60/#61 precedent)."
55+
exit 1
56+
fi
57+
58+
# Sanity check: every believe_me in the allowed file should correspond
59+
# to a registry entry. Count code uses (skip lines that are pure
60+
# comments / docstrings).
61+
allowed_count=$(
62+
grep '\bbelieve_me\b' "$ALLOWED_FILE" \
63+
| grep -v '^[[:space:]]*--' \
64+
| grep -v '^[[:space:]]*|||' \
65+
| wc -l
66+
)
67+
registry_count=$(grep -c '^ - name:' "$REGISTRY" || true)
68+
69+
echo "✓ believe_me policy check passed."
70+
echo " - $allowed_count occurrence(s) in $ALLOWED_FILE"
71+
echo " - $registry_count axiom(s) declared in $REGISTRY"
72+
73+
if [[ "$allowed_count" -ne "$registry_count" ]]; then
74+
echo
75+
echo "⚠ WARNING: believe_me count ($allowed_count) does not match"
76+
echo " registered axiom count ($registry_count). Double-check that"
77+
echo " every Axioms.idr believe_me has a matching registry entry."
78+
fi

‎.github/workflows/idris-verification.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,14 @@ on:
1515
paths:
1616
- 'proofs/idris2/**'
1717
- '.github/workflows/idris-verification.yml'
18+
- '.github/scripts/check-idris2-believe-me.sh'
19+
- '.machine_readable/IDRIS2_AXIOMS.a2ml'
1820
pull_request:
1921
paths:
2022
- 'proofs/idris2/**'
2123
- '.github/workflows/idris-verification.yml'
24+
- '.github/scripts/check-idris2-believe-me.sh'
25+
- '.machine_readable/IDRIS2_AXIOMS.a2ml'
2226
workflow_dispatch:
2327

2428
permissions:
@@ -82,6 +86,13 @@ jobs:
8286
- name: Show Idris2 version
8387
run: idris2 --version
8488

89+
- name: believe_me policy gate (Q1-C axiom registry)
90+
# Reject any `believe_me` in proofs/idris2/ that is not registered
91+
# in .machine_readable/IDRIS2_AXIOMS.a2ml. The only allowed home
92+
# for axiomatic believe_me is Filesystem.Axioms. See PROOF-NEEDS.md
93+
# "Priority 2" and the Q1-C pilot rationale.
94+
run: .github/scripts/check-idris2-believe-me.sh
95+
8596
- name: List installed Idris2 packages
8697
run: idris2 --list-packages
8798

‎.machine_readable/IDRIS2_AXIOMS.a2ml‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Registry of `believe_me`-backed axioms in the Idris2 proof layer.
5+
//
6+
// Any `believe_me` occurrence in `proofs/idris2/**/*.idr` that is NOT
7+
// listed here will be rejected by the CI guard at
8+
// `.github/scripts/check-idris2-believe-me.sh`.
9+
//
10+
// Adding a new axiom requires:
11+
// 1. Implementing it in `proofs/idris2/src/Filesystem/Axioms.idr`.
12+
// 2. Adding an entry to this file with:
13+
// - axiom name (matches the Idris2 identifier)
14+
// - location (file:line)
15+
// - justification (operational reason it is true)
16+
// - scope (which downstream proofs depend on it)
17+
18+
@a2ml-version: "0.1"
19+
@registry-kind: idris2-axioms
20+
@updated: "2026-06-02"
21+
@policy: "Q1-C pilot, soft believe_me policy with named + gated axioms"
22+
23+
axioms:
24+
- name: axStringEqRefl
25+
location: proofs/idris2/src/Filesystem/Axioms.idr:42
26+
type: "(s : String) -> (s == s) = True"
27+
justification: |
28+
Every Idris2 backend (Chez, Node, Racket) evaluates prim__strEq s s
29+
to True for any String s. The type-checker cannot reduce primitive
30+
String equality on opaque (non-literal) s, so we register the
31+
operational fact as a named axiom.
32+
morally-equivalent-to:
33+
- Agda postulate funext (FilesystemModel.agda:161)
34+
- Coq Axiom is_empty_dir_dec (posix_errors.v)
35+
used-by:
36+
- Filesystem.Model.pathEqRefl
37+
- Filesystem.Model.entryEqRefl
38+
- Filesystem.Model.equivRefl
39+
40+
- name: axBits8EqRefl
41+
location: proofs/idris2/src/Filesystem/Axioms.idr:55
42+
type: "(b : Bits8) -> (b == b) = True"
43+
justification: |
44+
Every Idris2 backend evaluates prim__eqBits8 b b to True for any
45+
Bits8 b. Same operational reasoning as axStringEqRefl applied to
46+
the byte-level primitive.
47+
morally-equivalent-to:
48+
- Agda postulate funext (FilesystemModel.agda:161)
49+
- Coq Axiom is_empty_dir_dec (posix_errors.v)
50+
used-by:
51+
- Filesystem.Axioms.fileContentEqRefl
52+
- Filesystem.Model.fsEntryEqRefl
53+
- Filesystem.Model.entryEqRefl
54+
- Filesystem.Model.equivRefl

‎proofs/idris2/src/Filesystem/Axioms.idr‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
-- Primitive-eq reflexivity axioms — Q1-C pilot
4+
--
5+
-- This module is the single registered home for `believe_me`-backed
6+
-- axioms in the Idris2 proof layer. Any other use of `believe_me` in
7+
-- `proofs/idris2/**` is rejected by the CI guard at
8+
-- `.github/scripts/check-idris2-believe-me.sh`.
9+
--
10+
-- The axioms here exist because Idris2 0.8.0 does NOT reduce primitive
11+
-- String / Bits8 `==` on opaque values at type-check time, even though
12+
-- every backend (Chez / Node / Racket) evaluates them correctly at
13+
-- runtime. We bridge this gap with two named, audited axioms — morally
14+
-- identical to Agda's `postulate funext` (already accepted) and Coq's
15+
-- `Axiom is_empty_dir_dec` (already accepted).
16+
--
17+
-- Adding a new axiom requires:
18+
-- 1. Adding it to this module (and ONLY this module).
19+
-- 2. Adding the matching entry to `.machine_readable/IDRIS2_AXIOMS.a2ml`.
20+
-- 3. The CI grep guard verifies the two stay in sync.
21+
22+
module Filesystem.Axioms
23+
24+
import Data.String
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Primitive equality reflexivity
30+
--------------------------------------------------------------------------------
31+
32+
||| AXIOM: primitive `String` equality is reflexive on opaque values.
33+
|||
34+
||| Operational justification: every Idris2 backend evaluates
35+
||| `prim__strEq s s` to `True` for any `s : String`. The type-checker
36+
||| cannot see through the primitive on opaque (non-literal) `s`, so
37+
||| we register the fact as a named axiom rather than block every
38+
||| downstream proof on the operational reality.
39+
|||
40+
||| Audit registry: `.machine_readable/IDRIS2_AXIOMS.a2ml` key
41+
||| `axStringEqRefl`.
42+
export
43+
axStringEqRefl : (s : String) -> (s == s) = True
44+
axStringEqRefl _ = believe_me (Refl {x = True})
45+
46+
||| AXIOM: primitive `Bits8` equality is reflexive on opaque values.
47+
|||
48+
||| Operational justification: every Idris2 backend evaluates
49+
||| `prim__eqBits8 b b` to `True` for any `b : Bits8`. As with
50+
||| `axStringEqRefl`, registered here so the type-checker has the
51+
||| fact available without seeing through the primitive.
52+
|||
53+
||| Audit registry: `.machine_readable/IDRIS2_AXIOMS.a2ml` key
54+
||| `axBits8EqRefl`.
55+
export
56+
axBits8EqRefl : (b : Bits8) -> (b == b) = True
57+
axBits8EqRefl _ = believe_me (Refl {x = True})
58+
59+
--------------------------------------------------------------------------------
60+
-- Derived: list reflexivity
61+
--------------------------------------------------------------------------------
62+
63+
||| `List Bits8` (= `FileContent`) equality reflexivity, lifted from
64+
||| `axBits8EqRefl` over the standard `Eq` instance for `List`.
65+
|||
66+
||| Not an axiom — proved structurally. Lives in this module purely
67+
||| to colocate with the axiom it depends on.
68+
export
69+
fileContentEqRefl : (xs : List Bits8) -> (xs == xs) = True
70+
fileContentEqRefl [] = Refl
71+
fileContentEqRefl (x :: rest) =
72+
rewrite axBits8EqRefl x in
73+
rewrite fileContentEqRefl rest in
74+
Refl

‎proofs/idris2/src/Filesystem/Model.idr‎

Lines changed: 111 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,13 @@ module Filesystem.Model
1010

1111
import Data.Bool
1212
import Data.List
13+
import Data.List.Elem
1314
import Data.Maybe
1415
import Data.String
1516
import Decidable.Equality
1617

18+
import Filesystem.Axioms
19+
1720
%default total
1821

1922
--------------------------------------------------------------------------------
@@ -210,10 +213,116 @@ equiv (MkFS entries1) (MkFS entries2) =
210213
all (\e => elem e entries2) entries1 &&
211214
all (\e => elem e entries1) entries2
212215

213-
||| Reflexivity of equivalence
216+
--------------------------------------------------------------------------------
217+
-- Primitive-eq reflexivity (lifted from Filesystem.Axioms)
218+
--------------------------------------------------------------------------------
219+
220+
||| `Path` equality is reflexive — proved by structural induction over
221+
||| `Path`, using `axStringEqRefl` at the leaf for each `String` component.
222+
export
223+
pathEqRefl : (p : Path) -> (p == p) = True
224+
pathEqRefl Root = Refl
225+
pathEqRefl (Cons s rest) =
226+
rewrite axStringEqRefl s in
227+
rewrite pathEqRefl rest in
228+
Refl
229+
230+
||| `FSEntry` equality is reflexive — `Dir == Dir = True` by definition,
231+
||| `File c == File c = c == c = True` via `fileContentEqRefl`.
232+
export
233+
fsEntryEqRefl : (e : FSEntry) -> (e == e) = True
234+
fsEntryEqRefl Dir = Refl
235+
fsEntryEqRefl (File c) = fileContentEqRefl c
236+
237+
||| Tuple `(Path, FSEntry)` equality reflexivity — combines `pathEqRefl`
238+
||| and `fsEntryEqRefl` through the derived `Eq` instance.
239+
export
240+
entryEqRefl : (e : (Path, FSEntry)) -> (e == e) = True
241+
entryEqRefl (p, fe) =
242+
rewrite pathEqRefl p in
243+
rewrite fsEntryEqRefl fe in
244+
Refl
245+
246+
--------------------------------------------------------------------------------
247+
-- Internal helpers for `elem` / `all` reflexivity
248+
--
249+
-- Idris2 0.8.0's `elem` desugars through the `Foldable` interface to
250+
-- `foldl (\acc, e => acc || Delay (x == e)) False xs`, not the textbook
251+
-- `(x == y) || elem x ys` recursion. So the proofs below pattern-match
252+
-- the foldl form directly.
253+
--------------------------------------------------------------------------------
254+
255+
||| Once the foldl accumulator hits `True`, the result is `True`
256+
||| regardless of the remaining list. `True || _` reduces by the first
257+
||| pattern of `Prelude.Bool.||` without forcing the lazy argument.
258+
private
259+
foldlOrTrueIdempotent : (xs : List a) -> (g : a -> Lazy Bool) ->
260+
foldl (\acc, e => acc || g e) True xs = True
261+
foldlOrTrueIdempotent [] _ = Refl
262+
foldlOrTrueIdempotent (_ :: ys) g = foldlOrTrueIdempotent ys g
263+
264+
||| `elem x (x :: ys) = True` given `x == x = True`.
265+
||| Threads the accumulator from `False || (x == x)` to `True`, then
266+
||| relies on `foldlOrTrueIdempotent` for the tail.
267+
private
268+
elemHere : Eq a => (x : a) -> (refl : (x == x) = True) -> (ys : List a) ->
269+
elem x (x :: ys) = True
270+
elemHere x refl ys =
271+
rewrite refl in foldlOrTrueIdempotent ys (\e => x == e)
272+
273+
||| If the accumulator starts `True` instead of `False`, the foldl
274+
||| stays `True` regardless of the list / element comparisons. This is
275+
||| the structural lift used by `elemWeaken`.
276+
private
277+
foldlOrAccTrueStays : (xs : List a) -> (g : a -> Lazy Bool) -> (b : Bool) ->
278+
foldl (\acc, e => acc || g e) b xs = True ->
279+
foldl (\acc, e => acc || g e) (b || True) xs = True
280+
foldlOrAccTrueStays xs g True prf = prf
281+
foldlOrAccTrueStays xs g False prf = foldlOrTrueIdempotent xs g
282+
283+
||| `elem` weakens on the right via the foldl form: an extra cons in
284+
||| front does not change the result once the accumulator has been
285+
||| forced True somewhere in the tail.
286+
private
287+
elemWeaken : Eq a => (x, y : a) -> (ys : List a) ->
288+
elem x ys = True -> elem x (y :: ys) = True
289+
elemWeaken x y ys prf with (x == y)
290+
elemWeaken x y ys prf | True = foldlOrTrueIdempotent ys (\e => x == e)
291+
elemWeaken x y ys prf | False = prf
292+
293+
||| For a list of entries where `==` is reflexive on the element type,
294+
||| every element is `elem` of the list (with `Elem` witness).
295+
private
296+
allElemSelfHelper :
297+
(xs, fullList : List (Path, FSEntry)) ->
298+
((e : (Path, FSEntry)) -> Elem e xs -> elem e fullList = True) ->
299+
all (\e => elem e fullList) xs = True
300+
allElemSelfHelper [] _ _ = Refl
301+
allElemSelfHelper (x :: rs) fullList prf =
302+
rewrite prf x Here in
303+
allElemSelfHelper rs fullList (\e, isIn => prf e (There isIn))
304+
305+
||| Every element of an entries list is `elem` of itself.
306+
private
307+
allElemSelf :
308+
(xs : List (Path, FSEntry)) -> all (\e => elem e xs) xs = True
309+
allElemSelf xs = allElemSelfHelper xs xs (\e, isIn => elemSelfWitness e xs isIn)
310+
where
311+
elemSelfWitness :
312+
(e : (Path, FSEntry)) -> (ys : List (Path, FSEntry)) ->
313+
Elem e ys -> elem e ys = True
314+
elemSelfWitness e (e :: rest) Here =
315+
elemHere e (entryEqRefl e) rest
316+
elemSelfWitness e (y :: rest) (There later) =
317+
elemWeaken e y rest (elemSelfWitness e rest later)
318+
319+
||| Reflexivity of equivalence. Closure path (Q1-C pilot, 2026-06-02 PM):
320+
||| structural induction over the entries list using the primitive-eq
321+
||| axioms registered in `Filesystem.Axioms`.
214322
export
215323
equivRefl : (fs : Filesystem) -> equiv fs fs = True
216-
equivRefl (MkFS entries) = ?equivReflProof
324+
equivRefl (MkFS entries) =
325+
rewrite allElemSelf entries in Refl
217326

218327
||| Symmetry of equivalence.
219328
|||

‎proofs/idris2/valence-shell.ipkg‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ readme = "README.md"
1111
sourcedir = "src"
1212

1313
-- Core modules
14-
modules = Filesystem.Model
14+
modules = Filesystem.Axioms
15+
, Filesystem.Model
1516
, Filesystem.Operations
1617
, Filesystem.Composition
1718
, Filesystem.RMO

0 commit comments

Comments
 (0)