galvanize(iter5c): counting defs + clz/ctz semantic theorems

Add u64-level counting function definitions to Interp.lean:
- u64CountLeadingZeros, u64CountTrailingZeros
- u64CountLeadingOnes, u64CountTrailingOnes

Prove u64_clz_semantic and u64_ctz_semantic showing the
_correct output matches the u64-level definitions.

Clo/cto semantic theorems deferred (ZMod/Bool conversion
complexity with 0xFFFFFFFF sentinel value).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: tob-joe

.galvanize/goal.md

@@ -78,10 +78,8 @@ types (toU64, toU128) rather than raw field elements.
 
 ### Tier 8: Semantic U64 Counting & Min/Max
 
-- [ ] AC-37: u64_clz_semantic [blocked: needs u64
-  clz definition]
-- [ ] AC-38: u64_ctz_semantic [blocked: needs u64
-  ctz definition]
+- [x] AC-37: u64_clz_semantic
+- [x] AC-38: u64_ctz_semantic
 - [ ] AC-39: u64_clo_semantic [blocked: needs u64
   clo definition]
 - [ ] AC-40: u64_cto_semantic [blocked: needs u64

MidenLean/Proofs/Interp.lean

@@ -358,4 +358,28 @@ theorem felt_lo32_hi32_toU64 (n : Nat)
     ZMod.val_natCast_of_lt h32_hi]
   omega
 
+/-- Count leading zeros of a 64-bit value represented
+    as two u32 limbs. If hi is zero, count all 32 bits
+    of hi plus leading zeros of lo. -/
+def u64CountLeadingZeros (lo hi : Nat) : Nat :=
+  if hi = 0 then u32CountLeadingZeros lo + 32
+  else u32CountLeadingZeros hi
+
+/-- Count trailing zeros of a 64-bit value represented
+    as two u32 limbs. If lo is zero, count all 32 bits
+    of lo plus trailing zeros of hi. -/
+def u64CountTrailingZeros (lo hi : Nat) : Nat :=
+  if lo = 0 then u32CountTrailingZeros hi + 32
+  else u32CountTrailingZeros lo
+
+/-- Count leading ones of a 64-bit value. -/
+def u64CountLeadingOnes (lo hi : Nat) : Nat :=
+  u64CountLeadingZeros (lo ^^^ (u32Max - 1))
+    (hi ^^^ (u32Max - 1))
+
+/-- Count trailing ones of a 64-bit value. -/
+def u64CountTrailingOnes (lo hi : Nat) : Nat :=
+  u64CountTrailingZeros (lo ^^^ (u32Max - 1))
+    (hi ^^^ (u32Max - 1))
+
 end MidenLean

MidenLean/Proofs/U64/Clz.lean

@@ -1,4 +1,5 @@
 import MidenLean.Proofs.Tactics
+import MidenLean.Proofs.Interp
 import MidenLean.Generated.U64
 
 namespace MidenLean.Proofs
@@ -61,4 +62,22 @@ theorem u64_clz_correct (lo hi : Felt) (rest : List Felt) (s : MidenState)
     rw [stepDrop]; miden_bind
     rw [stepU32Clz (ha := hhi)]
 
+/-- The _correct output equals u64CountLeadingZeros
+    applied to the limb values. -/
+theorem u64_clz_semantic (lo hi : Felt) :
+    (if hi == (0 : Felt)
+     then Felt.ofNat (u32CountLeadingZeros lo.val) + 32
+     else Felt.ofNat (u32CountLeadingZeros hi.val)) =
+    Felt.ofNat (u64CountLeadingZeros lo.val hi.val) := by
+  simp only [u64CountLeadingZeros]
+  by_cases h : hi.val = 0
+  · have : hi = (0 : Felt) := ZMod.val_injective _ h
+    simp only [this, beq_self_eq_true, ite_true,
+      ZMod.val_zero]
+    simp only [Felt.ofNat]
+    push_cast; ring
+  · have : hi ≠ (0 : Felt) := fun heq =>
+      h (by rw [heq]; simp)
+    simp [this, h]
+
 end MidenLean.Proofs

MidenLean/Proofs/U64/Ctz.lean

@@ -1,4 +1,5 @@
 import MidenLean.Proofs.Tactics
+import MidenLean.Proofs.Interp
 import MidenLean.Generated.U64
 
 namespace MidenLean.Proofs
@@ -56,4 +57,20 @@ theorem u64_ctz_correct (lo hi : Felt) (rest : List Felt) (s : MidenState)
     rw [stepDrop]; miden_bind
     rw [stepU32Ctz (ha := hlo)]
 
+/-- The _correct output equals u64CountTrailingZeros. -/
+theorem u64_ctz_semantic (lo hi : Felt) :
+    (if lo == (0 : Felt)
+     then Felt.ofNat (u32CountTrailingZeros hi.val) + 32
+     else Felt.ofNat (u32CountTrailingZeros lo.val)) =
+    Felt.ofNat (u64CountTrailingZeros lo.val hi.val) := by
+  simp only [u64CountTrailingZeros]
+  by_cases h : lo.val = 0
+  · have : lo = (0 : Felt) := ZMod.val_injective _ h
+    simp only [this, beq_self_eq_true, ite_true,
+      ZMod.val_zero, Felt.ofNat]
+    push_cast; ring
+  · have : lo ≠ (0 : Felt) := fun heq =>
+      h (by rw [heq]; simp)
+    simp [this, h]
+
 end MidenLean.Proofs