From f47663b8903920a229d61816e552a854f2210a96 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 19:55:38 +0200 Subject: [PATCH] S5.3 drill (2nd pass): anchor refactor-equivalence provenance to git history The previous drill's equivalence theorems were only as strong as their RHS matching the ACTUAL historical base (not a from-memory reconstruction) and 'nothing else changed' being true. Both now verified against the repository itself: git show cfde9b2 confirms the RHS forms verbatim; git diff cfde9b2..8795e82 confirms the refactor is base-only (eight lines). Provenance recorded in Refactor.lean's header so the argument is self-contained: unchanged remainder (git) + equal base (kernel) => whole-function equality. 26 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 --- verification/Proofs/Refactor.lean | 8 +++++++- verification/Proofs/Refactor.olean | Bin 42872 -> 42872 bytes 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/verification/Proofs/Refactor.lean b/verification/Proofs/Refactor.lean index 90bd5a7..7a19e22 100644 --- a/verification/Proofs/Refactor.lean +++ b/verification/Proofs/Refactor.lean @@ -3,7 +3,13 @@ SEMANTICS-PRESERVING — Opus's only evidence was "the chain recompiled". These two theorems machine-check the equivalence against the exact list-match forms that were replaced, so the refactor's faithfulness is - a permanent, cone-audited guarantee. -/ + a permanent, cone-audited guarantee. + + PROVENANCE (verified against git history, not memory): the RHS forms + below are verbatim the base of `ConsRec` at commit cfde9b2 (pre- + refactor), and `git diff cfde9b2 8795e82 -- Proofs/Basic.lean` shows + the refactor touched ONLY those eight base lines. Unchanged remainder + (git) + equal base (kernel) = the whole function is unchanged. -/ import Proofs.Basic namespace LTLAcc diff --git a/verification/Proofs/Refactor.olean b/verification/Proofs/Refactor.olean index 3dcdd5db6de09428a369bd35887d6e64f86ef1ca..c7ca4738766ef75ec39238d9b700e971c9f00632 100644 GIT binary patch delta 94 zcmexyj_JoarVR!?jK-4