From ef959f0b406ddf1b11c82f2ab856b0bd2958f3d3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 24 Jun 2026 09:59:09 +0000 Subject: [PATCH] fix(abi): remove duplicate allTake definition in Boj.SafetyLemmas allTake was defined twice (lines ~122-130 and ~213-221) with the same logical type (only the implicit-argument order differed), causing "Boj.SafetyLemmas.allTake is already defined" and failing the core ABI proof type-check (boj.ipkg: PASS=104 FAIL=1). Pre-existing bug, masked because the Idris2 type-check job is path-gated and skips unless a .idr changes (it surfaced on #234 and #236 when a .idr edit triggered the job). Fix: keep the first definition -- a complete, total proof (no postulates, no believe_me) -- and remove the redundant second copy. Both callers (SafePromptInjection, SafeHTTP) use `allTake prf` with inferred implicits, so the removed copy's implicit order is irrelevant to them. Expected: scripts/typecheck-proofs.sh -> PASS=105 FAIL=0. (Idris2 not available in the authoring env; the Idris2 CI job is the proof check.) Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01XrPAh7eBSUcVKauTVdXH9Y --- src/abi/Boj/SafetyLemmas.idr | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/abi/Boj/SafetyLemmas.idr b/src/abi/Boj/SafetyLemmas.idr index bbce315f..7629f90d 100644 --- a/src/abi/Boj/SafetyLemmas.idr +++ b/src/abi/Boj/SafetyLemmas.idr @@ -210,16 +210,6 @@ allNotImpliesAnyFalse {p} {xs = x :: xs'} prf with (p x) proof pEq allNotImpliesAnyFalse {p} {xs = x :: xs'} prf | False = allNotImpliesAnyFalse {xs = xs'} prf -||| If `allRec p xs = True`, then `allRec p (take n xs) = True`. -export -allTake : {p : a -> Bool} -> {xs : List a} -> {n : Nat} -> - allRec p xs = True -> allRec p (take n xs) = True -allTake {n = Z} _ = Refl -allTake {xs = []} {n = S _} _ = Refl -allTake {p} {xs = x :: xs'} {n = S n'} prf with (p x) proof eq - allTake {p} {xs = x :: xs'} {n = S n'} prf | True = allTake {xs = xs'} {n = n'} prf - allTake {p} {xs = x :: xs'} {n = S n'} prf | False = absurd prf - ||| Convert a Bool lte witness to LTE. export fromLteTrue : (a, b : Nat) -> (a <= b) = True -> LTE a b