From bde63f53ed2bb468218824b53717a7ecba1745ad Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Wed, 22 Jul 2026 23:54:03 +0200
Subject: [PATCH] phase 2 step 1: de-plumb the u32 range-loop machinery
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The verify cone iterates u32 ranges (for j in i..i+s). Aeneas.Std ships
a real Step instance only for usize (StepUsize), so u32 ranges extracted
as three opaque axioms (forward_checked / backward_checked /
steps_between) — which would poison every loop-bearing cone, i.e. chain
and everything above it.

Discharged in the hand-written external file (H4-sanctioned) with
FAITHFUL real definitions mirroring Rust's impl Step for u32
(core/src/iter/range.rs) and Aeneas.Std's StepUsize: forward/backward via
u32::try_from(n)-then-checked_{add,sub}, steps_between = saturating
difference. Verified in isolation (axiom-clean) and in place:
#print axioms on the u32 Step instance now reports exactly
[propext, Classical.choice, Quot.sound]. Model still compiles.

These are ordinary loop control, NOT the deployed hash boundary — the
five oracle axioms remain the only cryptographic externals.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 verification/gen/SlhVerify/FunsExternal.lean | 33 ++++++++++++++++----
 1 file changed, 27 insertions(+), 6 deletions(-)

diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean
index ca65070..122d691 100644
--- a/verification/gen/SlhVerify/FunsExternal.lean
+++ b/verification/gen/SlhVerify/FunsExternal.lean
@@ -87,10 +87,22 @@ axiom core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next
     Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
     Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
     Visibility: public -/
+-- DISCHARGED (2026-07-22, proof phase): Aeneas.Std ships a real `Step`
+-- instance only for `usize` (StepUsize); u32 ranges therefore extracted as
+-- opaque axioms. These are the FAITHFUL models of Rust's `impl Step for u32`
+-- (core/src/iter/range.rs), mirroring StepUsize: forward/backward via
+-- u32::try_from(n)-then-checked_{add,sub}; steps_between = saturating
+-- difference. Real defs, axiom-clean — so the range-loop cones (chain, and
+-- every layer above) carry no plumbing axiom, only the kernel three + the
+-- five hash oracles. NOT the deployed hash boundary; ordinary loop control.
 @[rust_fun
   "core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
-axiom U32.Insts.CoreIterRangeStep.backward_checked
-  : Std.U32 → Std.Usize → Result (Option Std.U32)
+def U32.Insts.CoreIterRangeStep.backward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32) :=
+  fun start n =>
+    if h : n.val < 2 ^ 32 then
+      ok (Std.U32.checked_sub start (Std.U32.ofNatCore n.val (by omega)))
+    else ok none
 
 /-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
     Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
@@ -98,16 +110,25 @@ axiom U32.Insts.CoreIterRangeStep.backward_checked
     Visibility: public -/
 @[rust_fun
   "core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
-axiom U32.Insts.CoreIterRangeStep.forward_checked
-  : Std.U32 → Std.Usize → Result (Option Std.U32)
+def U32.Insts.CoreIterRangeStep.forward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32) :=
+  fun start n =>
+    if h : n.val < 2 ^ 32 then
+      ok (Std.U32.checked_add start (Std.U32.ofNatCore n.val (by omega)))
+    else ok none
 
 /-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
     Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
     Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
     Visibility: public -/
 @[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
-axiom U32.Insts.CoreIterRangeStep.steps_between
-  : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
+def U32.Insts.CoreIterRangeStep.steps_between
+  : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize)) :=
+  fun start end_ =>
+    if h : start.val > end_.val then ok (0#usize, none)
+    else
+      let steps := Std.Usize.ofNatCore (end_.val - start.val) (by scalar_tac)
+      ok (steps, some steps)
 
 /-- [core::iter::traits::iterator::Iterator::take]:
     Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 1447:4-1449:20