-- R8 opp-bank densified node supports (jfstack_23, dense d ↔ raw d+1).
-- Generated by notes/track_bitnb/gen/emit_sup_dense_pnd.py

import Definitions.Def_IntMul_Kappa_R6_Defs50
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense0_7
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense1_7
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense2_7
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_7
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankWireLayout

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option maxRecDepth 100000

namespace R6Chk.Bit

/-- Densified support BT (depth 12). Dense `d` ↔ jfstack raw node `d+1`. -/
noncomputable def densSupT : BT :=
  BT.node (BT.node densSupT0 densSupT1) (BT.node densSupT2 densSupT3)

noncomputable def densBtGet (t : BT) : ℕ → ℕ → ℕ :=
  BT.rec (motive := fun _ => ℕ → ℕ → ℕ) (fun x _ _ => x)
    (fun _ _ ihl ihr d i =>
      cond (Nat.testBit i (Nat.sub d 1)) (ihr (Nat.sub d 1) i) (ihl (Nat.sub d 1) i)) t

def densFieldOf (X w i : ℕ) : ℕ :=
  Nat.land (Nat.shiftRight X (Nat.mul w i)) (Nat.sub (Nat.shiftLeft 1 w) 1)

/-- Support mask of densified node `k` (`0 ≤ k < 62478`). -/
noncomputable def densSupG (k : ℕ) : ℕ :=
  densFieldOf (densBtGet densSupT 12 (Nat.shiftRight k 4)) 1792 (Nat.land k 15)

end R6Chk.Bit

namespace IntMul.Kappa.R8.Bit.Oppbank.SupG

open R6Chk.Bit

def nNodes : ℕ := 62478
def codeBound : ℕ := 64251
theorem nNodes_eq : nNodes = 62478 := rfl
theorem codeBound_eq : codeBound = 1773 + nNodes := by decide

noncomputable def densSupG (k : ℕ) : ℕ := R6Chk.Bit.densSupG k
noncomputable def densSupT : R6Chk.Bit.BT := R6Chk.Bit.densSupT

end IntMul.Kappa.R8.Bit.Oppbank.SupG