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

Discharges the **only two `postulate`s** in echidna's own proof corpus,
so the tree is now **literally axiom-free**.

## Changes
- **`SoundnessPreservation.agda`** — `Conflicts` was a module-level
`postulate` used only in `compose-sound`'s hypothesis (which the proof
discards). Made it an **explicit parameter of `compose-sound`** —
strictly more general (works for any conflict predicate), no axiom
declared, no burden on the other lemmas.
- **`Basic.agda` (`CurryUncurryLaws`)** — dropped the **`funext`**
postulate. The curry/uncurry inverse laws are now stated **pointwise**
and proved by `refl` (the axiom-free plain-Agda formulation). The full
`curry (uncurry f) ≡ f` form would need funext — a standard axiom, or
Cubical Agda + the cubical library; pointwise needs neither, so no new
CI dep.

## Why this form (not Cubical)
Cubical Agda would preserve the fully-extensional statement but requires
adding the cubical library to the Agda CI (an addition we're avoiding)
and couldn't be verified in the authoring sandbox. The pointwise
statement is the honest axiom-free truth and is `refl`-trivial.

## Verification
- `grep` confirms **zero `postulate` declarations** across `proofs/`,
`meta-checker/`, `verification/proofs/`, `src/abi/`, `src/idris/`; no
dangling `funext`/`Conflicts` refs.
- Compilation is checked by the **gated dogfood Agda CI on this PR**
(`just proofs-agda` type-checks both files), since I can't run Agda
locally.

Net: every echidna-owned proof (Agda + Idris2 ABI +
Coq/Lean/Isabelle/Mizar dogfood) is now axiom-free — no postulate /
sorry / admit / believe_me anywhere. Draft until the Agda job goes
green.

https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv

---
_Generated by [Claude
Code](https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

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