From 2cdedc1b858f20f90b5f5fad40fe931ca1130e0c Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 18:34:30 +0000 Subject: [PATCH 1/2] build(guix): add Agda, agda-stdlib, Rocq and Lean to the manifest (WO 1.4, in progress) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- build/manifest.scm | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/build/manifest.scm b/build/manifest.scm index 9d826210..a3470ac7 100644 --- a/build/manifest.scm +++ b/build/manifest.scm @@ -12,4 +12,8 @@ ;; Canon: hyperpolymath/standards 3-practice/provisioning/PROVISIONING-STANDARD.adoc (specifications->manifest (list "git" "bash" "coreutils" "nss-certs" "just" "mise" - "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig")) + "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig" + ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)): + ;; at the pinned Guix revision these are Agda 2.7.0.1 with agda-stdlib + ;; 2.3, Rocq (coq) 8.18.0 and Lean 4.29.0. + "agda" "agda-stdlib" "coq" "lean4")) From d3d46304726154652eb9bda0ea18e70b6b8264e9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:25:36 +0000 Subject: [PATCH 2/2] fix(proofs): Properties.agda on Agda.Builtin only; drop agda-stdlib (WO 1.4, in progress) The agda-stdlib 2.3 package of the pinned Guix does not build (it fails on the Guix build farm in every build since 2026-10-18). Owner ruling 2026-11-10: rewrite the template examples without the library. They now use Agda.Builtin.Nat, List and Equality only, and pass the canonical invocation with no library configured. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- build/manifest.scm | 8 +++---- verification/proofs/agda/MANIFEST | 2 +- verification/proofs/agda/Properties.agda | 30 +++++++++++++++++++----- 3 files changed, 29 insertions(+), 11 deletions(-) diff --git a/build/manifest.scm b/build/manifest.scm index a3470ac7..bddd6575 100644 --- a/build/manifest.scm +++ b/build/manifest.scm @@ -13,7 +13,7 @@ (specifications->manifest (list "git" "bash" "coreutils" "nss-certs" "just" "mise" "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig" - ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)): - ;; at the pinned Guix revision these are Agda 2.7.0.1 with agda-stdlib - ;; 2.3, Rocq (coq) 8.18.0 and Lean 4.29.0. - "agda" "agda-stdlib" "coq" "lean4")) + ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)). + ;; No agda-stdlib: its Guix package does not build, and no proof here + ;; imports it (owner ruling 2026-11-10). + "agda" "coq" "lean4")) diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index c5ad9701..3bb613a5 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -1,5 +1,5 @@ # Agda proof manifest — read by scripts/check-proofs.sh agda # Format: ||gated|quarantine| # Prior check (2026-07-17): agda --safe only; full 2026-11 policy pending CI. -verification/proofs/agda|Properties.agda|gated| previously checked under `agda --safe`; new full-mode recheck pending +verification/proofs/agda|Properties.agda|gated| template examples on Agda.Builtin only, no library (2026-11-10); passes the canonical invocation verification/proofs/agda|FeatureReachability.agda|gated| additive features: reachability monotone in the requested set (no library imports) diff --git a/verification/proofs/agda/Properties.agda b/verification/proofs/agda/Properties.agda index d78d9d0f..f3677b51 100644 --- a/verification/proofs/agda/Properties.agda +++ b/verification/proofs/agda/Properties.agda @@ -4,21 +4,39 @@ -- Agda Proof Template: Inductive and coinductive properties -- Replace with your project's domain-specific proofs. -- All proofs must be total (no postulate, no {-# TERMINATING #-}). +-- +-- No library imports: only the Agda.Builtin modules that ship with Agda. +-- The agda-stdlib 2.3 package of the pinned Guix does not build (re-anchoring +-- plan WO 1.4, owner ruling 2026-11-10), and these examples need little of it. module Properties where -open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) -open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) -open import Data.List using (List; []; _∷_; length; _++_) -open import Data.List.Properties using (length-++ ) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Equality using (_≡_; refl) + +cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong f refl = refl + +length : ∀ {A : Set} → List A → Nat +length [] = zero +length (_ ∷ xs) = suc (length xs) + +_++_ : ∀ {A : Set} → List A → List A → List A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ (xs ++ ys) + +data _≤_ : Nat → Nat → Set where + z≤n : ∀ {n} → zero ≤ n + s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n -- Example: Proof that list append preserves total length -- Replace with your project's domain proofs. append-length : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys -append-length xs ys = length-++ xs +append-length [] ys = refl +append-length (_ ∷ xs) ys = cong suc (append-length xs ys) -- Example: Monotonicity proof template -- Use for state machines, confidence scores, trust levels