Skip to content

Commit bcb7a4b

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into proofs/idris2-129-overwrite-irreversible-redesign
2 parents 758da65 + 8318f73 commit bcb7a4b

7 files changed

Lines changed: 378 additions & 32 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

‎PROOF-NEEDS.md‎

Lines changed: 48 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -113,42 +113,61 @@ primitive-eq blocker as the Cat-B set above. Each requires showing
113113
that the post-operation precondition holds, which reduces to
114114
`(p == p) = True` on opaque `Path` — blocked.
115115

116-
#### Priority 2 — primitive-eq groundwork (foundational, owner-decision required)
117-
118-
Every remaining tractable hole reduces to a `(s == s) = True` step on
119-
opaque `String` or `Bits8` — Idris2 0.8.0 only reduces these on
120-
literals. `DecEq Path` does NOT help because it transitively depends
121-
on `DecEq String`, which itself depends on primitive `==`.
122-
123-
Three closure paths, each requiring owner sign-off:
124-
125-
1. **Add `String` / `Bits8` reflexivity axioms** — `axStringEqRefl :
126-
(s : String) -> (s == s) = True := believe_me Refl`, gated by CI
127-
allow-list (per the Cat-D `believe_me` pattern). Smallest change,
128-
but introduces `believe_me` into the proof system which prior
129-
sessions explicitly avoided.
130-
2. **Migrate `Path` to a structural representation** — replace
131-
`String`-component paths with `Nat`-encoded interned identifiers.
132-
`Nat == Nat` IS reducible on opaque values. Bigger migration but
133-
no `believe_me`.
134-
3. **Reformulate every blocked theorem to use `decEq`-style branches**
135-
rather than `==`-style booleans. Avoids touching the `Eq` instance
136-
but ripples through ~20 theorem statements.
137-
138-
Until one path is chosen, the following holes are **frozen**:
139-
140-
- `equivReflProof` (Model.idr:216)
141-
- `equivTransProof` (Model.idr:244)
116+
#### Priority 2 — TWO blockers (primitive-eq UNBLOCKED; `all`/`foldMap` still blocked)
117+
118+
Status as of the 2026-06-02 PM Q1-C pilot (PR #133):
119+
120+
**Blocker 1 (primitive-eq) — UNBLOCKED.** The pilot adds
121+
`axStringEqRefl` + `axBits8EqRefl` in `Filesystem.Axioms` with a CI
122+
allow-list guard. `equivReflProof` closed as proof-of-concept. The
123+
axioms are operationally true and gated; soundness audit trail
124+
preserved via the `IDRIS2_AXIOMS.a2ml` registry.
125+
126+
**Blocker 2 (`all`/`foldMap` reduction) — DISCOVERED.** Attempting to
127+
close `equivTrans` in the same session revealed a second, independent
128+
problem: **`all p (x :: rest)` does NOT reduce to `(p x && all p rest)`
129+
by `Refl` in Idris2 0.8.0.** The `all` definition elaborates through
130+
`foldMap @{All}` — even though `foldMap`'s default body is `foldr`-
131+
based, the elaborator produces a `foldl`-shaped term that neither
132+
`Refl` nor any straightforward rewrite can directly destructure into
133+
the textbook `&&`-chain. Empirical witness:
134+
`example : all p (x :: rs) = (p x && all p rs) ; example = Refl`
135+
fails to typecheck — the unifier reports
136+
`foldl ... (neutral <+> p x) rs` on one side, `p x && Delay (all p rs)`
137+
on the other.
138+
139+
Consequently, **`equivTrans`, `cnoWriteSameContent`, and the 7
140+
reversibility theorems** are still blocked. The primitive-eq axioms
141+
unblock the LEAF reflexivity step but cannot bridge the foldMap-shaped
142+
reduction wall.
143+
144+
Three closure paths for blocker 2 (owner-decision required):
145+
146+
1. **Replace `equiv` with a structural `myAll`-based definition** that
147+
reduces by `Refl`. Touches the `equiv` shape but contained to
148+
`Model.idr`. Probably 1 PR.
149+
2. **Prove `allCons : all p (x :: rs) = (p x && all p rs)` via a chain
150+
of `foldl` lemmas** — `foldlAndAccTrue` + `foldlAndFalseStays` +
151+
careful with-clauses. Pure mathematics but ~50 lines of fiddly
152+
proof engineering against an opaque elaboration order.
153+
3. **Migrate `equiv` to a propositional `All`-based shape** (via
154+
`Data.List.Quantifiers.All`) — cleanest mathematically but ripples
155+
through every call-site of `equiv`.
156+
157+
Until one of these lands, the following holes remain frozen even with
158+
the axiom infrastructure live:
159+
160+
- `equivTransProof` (Model.idr:353)
142161
- `cnoWriteSameContentProof` (Operations.idr:254)
143162
- 4 `?XXXPrfAfter` sub-holes in Operations.idr
144163
- 7 reversibility theorems in Operations.idr (mkdirRmdir, rmdirMkdir,
145164
touchRm, rmTouch, writeFile, operationIndependence,
146165
cnoWriteSameContent)
147166

148167
Separately, `undoRedoIdentityProof` and `undoRedoCompositionProof`
149-
need a Cat-A redesign (missing `isReversible op = True` precondition;
150-
provably refuted for non-reversible `op`) before primitive-eq is even
151-
relevant.
168+
still need a Cat-A redesign (missing `isReversible op = True`
169+
precondition; provably refuted for non-reversible `op`) before either
170+
blocker is relevant.
152171

153172
#### Priority 3 — Tier-S foundational (research-level)
154173

‎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

0 commit comments

Comments
 (0)