proofs(agda): reach literal zero axioms (discharge funext + Conflicts postulates)

proofs/agda/Basic.agda

@@ -151,25 +151,18 @@ curry f x y = f (x , y)
 uncurry : {A B C : Set} → (A → B → C) → (A × B → C)
 uncurry f (x , y) = f x y
 
--- Proof that curry and uncurry are inverses
+-- Proof that curry and uncurry are inverses.
+--
+-- Stated *pointwise* (the functions agree on every input), which is
+-- provable in plain Agda by `refl` with ZERO axioms. The fully-extensional
+-- form `curry (uncurry f) ≡ f` would require function extensionality
+-- (funext) — a standard axiom, but an axiom nonetheless; the pointwise
+-- statements below are the axiom-free truth and need no postulate.
 module CurryUncurryLaws where
-  -- INTENTIONAL AXIOM: Function extensionality (funext)
-  -- Justification: funext is consistent with Agda's type theory and is
-  -- provable in Cubical Agda (--cubical). In plain Agda it must be
-  -- postulated. It is a standard mathematical axiom accepted by all
-  -- major proof assistants (Coq's Functional Extensionality, Lean's
-  -- funext, HoTT axiom). It does NOT compromise soundness.
-  -- See: HoTT Book, Section 2.9; nLab "function extensionality"
-  -- AXIOM: funext (see justification above; recognised by check-trusted-base.sh)
-  postulate
-    funext : {A B : Set} {f g : A → B}
-           → ((x : A) → f x ≡ g x)
-           → f ≡ g
-
-  curry-uncurry : {A B C : Set} → (f : A → B → C)
-                → curry (uncurry f) ≡ f
-  curry-uncurry f = funext λ x → funext λ y → refl
-
-  uncurry-curry : {A B C : Set} → (f : A × B → C)
-                → uncurry (curry f) ≡ f
-  uncurry-curry f = funext λ { (x , y) → refl }
+  curry-uncurry : {A B C : Set} → (f : A → B → C) → (x : A) → (y : B)
+                → curry (uncurry f) x y ≡ f x y
+  curry-uncurry f x y = refl
+
+  uncurry-curry : {A B C : Set} → (f : A × B → C) → (p : A × B)
+                → uncurry (curry f) p ≡ f p
+  uncurry-curry f (x , y) = refl

proofs/agda/SoundnessPreservation.agda

@@ -41,23 +41,15 @@ record Proof : Set where
 -- 2.  Conflict predicate
 ------------------------------------------------------------------------
 
--- Conflicts is an abstract binary predicate over two axiom lists.
--- We leave it as a postulate-free parameter: the caller supplies a
--- concrete proof of ¬ Conflicts when they know the sets are disjoint.
+-- "Conflicts" is an abstract binary predicate over two axiom lists. It is
+-- threaded as an *explicit parameter* of the composition theorem (§5)
+-- rather than a module-level postulate, so this file declares ZERO axioms.
 --
--- In practice ECHIDNA computes this via the danger-level tracker
--- (verification/axioms.rs): two axiom sets conflict when one contains
--- an axiom that the other marks Reject.
--- TRUSTED: Conflicts is an abstract parameter (see above), not an unsound
--- escape — the caller discharges it with a concrete proof.
-postulate
-  Conflicts : List Axiom → List Axiom → Set
-  -- ^ INTENTIONAL PARAMETER — "Conflicts" is domain knowledge about
-  --   which axiom combinations are unsound.  Leaving it abstract keeps
-  --   the composition theorem maximally reusable: any concrete conflict
-  --   definition satisfying ¬ Conflicts a1 a2 gives the same guarantee.
-  --   This is NOT a soundness hole: the theorem proves a conditional,
-  --   not an unconditional claim.
+-- In practice ECHIDNA instantiates it via the danger-level tracker
+-- (src/rust/verification/axioms.rs): two axiom sets conflict when one
+-- contains an axiom the other marks Reject. The theorem proves a
+-- conditional ("if the sets do not conflict …"), so any concrete conflict
+-- definition gives the same guarantee.
 
 ------------------------------------------------------------------------
 -- 3.  Proof composition
@@ -83,12 +75,13 @@ compose p1 p2 = MkProof
 --     conflict, then compose p1 p2 is sound.
 ------------------------------------------------------------------------
 
-compose-sound : (p1 p2 : Proof)
+compose-sound : (Conflicts : List Axiom → List Axiom → Set)
+              → (p1 p2 : Proof)
               → Proof.sound p1 ≡ true
               → Proof.sound p2 ≡ true
               → ¬ Conflicts (Proof.axioms p1) (Proof.axioms p2)
               → Proof.sound (compose p1 p2) ≡ true
-compose-sound p1 p2 s1 s2 _ = ∧-true s1 s2
+compose-sound _ p1 p2 s1 s2 _ = ∧-true s1 s2
 
 ------------------------------------------------------------------------
 -- 6.  Structural corollary: composing with an empty-axiom proof