def selectZ {c k} (L : LogicalBasis c k) (S : List (Fin k)) : BoolVec

def selectX {c k} (L : LogicalBasis c k) (S : List (Fin k)) : BoolVec

def addressedTargetZ {c k} (L : LogicalBasis c k) (S : List (Fin k))
    (ancilla_n : Nat) : BoolVec

def addressedTargetX {c k} (L : LogicalBasis c k) (S : List (Fin k))
    (ancilla_n : Nat) : BoolVec

theorem selectZ_nil {c k} (L : LogicalBasis c k) :
    L.selectZ [] = zero_vec c.n

theorem selectZ_cons {c k} (L : LogicalBasis c k) (i : Fin k)
    (S : List (Fin k)) :
    L.selectZ (i :: S) = vec_xor (L.lz i) (L.selectZ S)

theorem selectX_nil {c k} (L : LogicalBasis c k) :
    L.selectX [] = zero_vec c.n

theorem selectX_cons {c k} (L : LogicalBasis c k) (i : Fin k)
    (S : List (Fin k)) :
    L.selectX (i :: S) = vec_xor (L.lx i) (L.selectX S)

theorem selectZ_single {c k} (L : LogicalBasis c k) (i : Fin k) :
    L.selectZ [i] = vec_xor (L.lz i) (zero_vec c.n)

theorem selectX_single {c k} (L : LogicalBasis c k) (i : Fin k) :
    L.selectX [i] = vec_xor (L.lx i) (zero_vec c.n)

example : code422Logical.valid = true

example :
    code422Logical.selectZ [0, 1]
      = vec_xor (code422Logical.lz 0) (code422Logical.lz 1)

example : code422Logical.selectZ [0, 1] = [false, true, true, false]

example : code422Logical.selectZ [0] = code422Logical.lz 0

example : (code422Logical.addressedTargetZ [0, 1] 2).length = 6

example : code422Logical.selectX [0, 1] = [false, true, true, false]

theorem addressing_demo :
    code422Logical.addressedTargetZ [0, 1] 2
      = [false, true, true, false, false, false]

def bitsToVec (w : Nat) (bits : Nat) : BoolVec

def vecToBits (v : BoolVec) : Nat

example :
    bitsToVec 5 (vecToBits [true, false, true, true, false])
      = [true, false, true, true, false]

structure CodeBlock

structure LogicalAddr

structure BlockLayout

def totalN (L : BlockLayout) : Nat

def totalLogical (L : BlockLayout) : Nat

def wfAddr (L : BlockLayout) (a : LogicalAddr) : Bool

def wfStructural (L : BlockLayout) : Bool

def wf (L : BlockLayout) : Bool

theorem wf_of (L : BlockLayout) (hs : L.wfStructural = true)
    (hb : L.blocks.all (fun b => b.basis.valid) = true) : L.wf = true

abbrev VirtualPPM

abbrev ResolvedPPM

def resolve (L : BlockLayout) (p : VirtualPPM) : ResolvedPPM

def inRange (L : BlockLayout) (p : VirtualPPM) : Bool

def render (L : BlockLayout) (p : VirtualPPM) : String

def CodeBlock.logicalSupport (blk : CodeBlock) (b : MeasBasis) (i : Nat) : BoolVec

def globalPauli (L : BlockLayout) (a : LogicalAddr) (b : MeasBasis) : PauliString

def jointPauli (L : BlockLayout) (p : VirtualPPM) : PauliString

def compositeCode (L : BlockLayout) : CSSCode

def ppmTargetsLogical (L : BlockLayout) (p : VirtualPPM) : Bool

def blocksFor (Q k : Nat) : Nat

def naiveMap (Q k : Nat) : List LogicalAddr

def uniformLayout (b : CodeBlock) (Q : Nat) : BlockLayout

private theorem nodup_map_range {α : Type} (f : Nat → α)
    (hf : ∀ a b, f a = f b → a = b) (Q : Nat) :
    ((List.range Q).map f).Nodup

private theorem naiveMap_nodup (Q k : Nat) :
    (naiveMap Q k).Nodup

theorem uniformLayout_wfStructural (b : CodeBlock) (Q : Nat) (hk : 0 < b.k) :
    (uniformLayout b Q).wfStructural = true

private theorem foldl_add_init' (l : List Nat) :
    ∀ (n : Nat), l.foldl (· + ·) n = n + l.foldl (· + ·) 0

theorem uniformLayout_totalN (b : CodeBlock) (Q : Nat) :
    (uniformLayout b Q).totalN = blocksFor Q b.k * b.code.n

def demoB0 : CodeBlock

def demoB1 : CodeBlock

def demoLayout : BlockLayout

theorem demoLayout_totals :
    demoLayout.totalLogical = 4 ∧ demoLayout.totalN = 36

theorem demoLayout_wf : demoLayout.wf = true

def demoPPM : BlockLayout.VirtualPPM

theorem demoPPM_inRange : demoLayout.inRange demoPPM = true

theorem demoPPM_resolves :
    demoLayout.resolve demoPPM = [(⟨0, 1⟩, .x), (⟨1, 1⟩, .z)]

theorem demoPPM_renders :
    demoLayout.render demoPPM = "Measure X[B0(1)] Z[B1(1)] "

theorem demoPPM_targets_logical :
    demoLayout.ppmTargetsLogical demoPPM = true

structure CSSCode

def well_shaped (c : CSSCode) : Bool

def css_condition (c : CSSCode) : Bool

def valid (c : CSSCode) : Bool

def is_qldpc_code (c : CSSCode) (Δ : Nat) : Bool

def xStab (l : BoolVec) : PauliString

def zStab (l : BoolVec) : PauliString

def toStabilizers (c : CSSCode) : StabilizerState

def toQECCode (c : CSSCode) (k d : Nat) : Framework.QECCode

def ofQECCodeChecked (q : Framework.QECCode) : Option CSSCode

theorem xbit_commutes (x y : Bool) : Pauli.commutes (xbit x) (xbit y) = true

theorem zbit_commutes (x y : Bool) : Pauli.commutes (zbit x) (zbit y) = true

theorem xStab_commutes (a b : BoolVec) : (xStab a).commutes (xStab b) = true

theorem zStab_commutes (a b : BoolVec) : (zStab a).commutes (zStab b) = true

theorem xz_anti_count (a b : BoolVec) :
    ((a.map xbit).zip (b.map zbit)).countP (fun p => ! p.1.commutes p.2)
      = (a.zip b).countP (fun p => p.1 && p.2)

theorem xStab_zStab_commutes (a b : BoolVec) :
    (xStab a).commutes (zStab b) = ! dotBit a b

theorem syndrome_circuit_implements_code (c : CSSCode) (hws : c.well_shaped = true) :
    StabilizerState.valid (c.toStabilizers) c.n = true ↔ c.css_condition = true

def conjOp : PhysOp → PauliString → PauliString
  | .cx c t,   p => cnotConj c t p
  | .prep _ _, p => p
  | .meas _ _, p => p

def conjOps (ops : PhysCircuit) (p : PauliString) : PauliString

def MeasBasis.toPauli : MeasBasis → Pauli
  | .z => Pauli.Z
  | .x => Pauli.X

def ancillaObs (b : MeasBasis) (w anc : Nat) : PauliString

def CheckBlock.measuredObs (w : Nat) (b : CheckBlock) : PauliString

def dataPart (n : Nat) (p : PauliString) : PauliString

def Round.measuredDataObs (w n : Nat) (r : Round) : List PauliString

theorem Round.measuredDataObs_append (w n : Nat) (r s : Round) :
    Round.measuredDataObs w n (r ++ s)
      = Round.measuredDataObs w n r ++ Round.measuredDataObs w n s

theorem conjOps_zBlock (anc : Nat) (supp : List Nat) (p : PauliString) :
    conjOps (CheckBlock.ops ⟨.z, anc, supp⟩) p = measGadgetConj supp anc p

theorem conjOps_xBlock (anc : Nat) (supp : List Nat) (p : PauliString) :
    conjOps (CheckBlock.ops ⟨.x, anc, supp⟩) p = xMeasGadgetConj supp anc p

private theorem ancillaObs_len (b : MeasBasis) (w anc : Nat) :
    (ancillaObs b w anc).ops.length = w

private theorem ancillaObs_at_anc (b : MeasBasis) (w anc : Nat) (h : anc < w) :
    (ancillaObs b w anc).ops.getD anc .I = b.toPauli

private theorem ancillaObs_other (b : MeasBasis) (w anc j : Nat) (hj : j ≠ anc) :
    (ancillaObs b w anc).ops.getD j .I = Pauli.I

private theorem pauliString_ext (p q : PauliString)
    (hphase : p.phase = q.phase) (hlen : p.ops.length = q.ops.length)
    (hpos : ∀ j, j < p.ops.length → p.ops.getD j .I = q.ops.getD j .I) :
    p = q

private theorem getD_take_eq (l : List Pauli) (n j : Nat) (hj : j < n)
    (hl : j < l.length) :
    (l.take n).getD j .I = l.getD j .I

private theorem map_bit_getD (f : Bool → Pauli) (row : List Bool) (j : Nat)
    (hjr : j < row.length) :
    (row.map f).getD j .I = f (row.getD j false)

theorem measuredObs_zBlock (w n anc : Nat) (row : List Bool)
    (hrow : row.length = n) (hlo : n ≤ anc) (hhi : anc < w) :
    dataPart n (CheckBlock.measuredObs w ⟨.z, anc, rowSupport row⟩)
      = FormalRV.QEC.CSSCode.zStab row

theorem measuredObs_xBlock (w n anc : Nat) (row : List Bool)
    (hrow : row.length = n) (hlo : n ≤ anc) (hhi : anc < w) :
    dataPart n (CheckBlock.measuredObs w ⟨.x, anc, rowSupport row⟩)
      = FormalRV.QEC.CSSCode.xStab row

private theorem measuredDataObs_xBlocksFrom (n w : Nat) (rows : BoolMat) :
    ∀ (a : Nat), n ≤ a → a + rows.length ≤ w →
      (∀ row ∈ rows, row.length = n) →
      Round.measuredDataObs w n (xBlocksFrom rows a)
        = rows.map FormalRV.QEC.CSSCode.xStab

private theorem measuredDataObs_zBlocksFrom (n w : Nat) (rows : BoolMat) :
    ∀ (a : Nat), n ≤ a → a + rows.length ≤ w →
      (∀ row ∈ rows, row.length = n) →
      Round.measuredDataObs w n (zBlocksFrom rows a)
        = rows.map FormalRV.QEC.CSSCode.zStab

theorem extractionRound_measures_code (c : FormalRV.QEC.CSSCode)
    (hws : c.well_shaped = true) :
    Round.measuredDataObs (c.n + c.hx.length + c.hz.length) c.n
        (FormalRV.QEC.CSSCode.extractionRound c)
      = c.toStabilizers

theorem xRow_eq_xStab (l : List Bool) :
    FormalRV.Framework.SurgeryReadout.xRow l = FormalRV.QEC.CSSCode.xStab l

theorem zRow_eq_zStab (l : List Bool) :
    FormalRV.Framework.SurgeryCorrect.zRow l = FormalRV.QEC.CSSCode.zStab l

theorem extractionRound_measures_merged (g : SurgeryGadget)
    (hxr : ∀ row ∈ g.merged_hx, row.length = g.merged_n)
    (hzr : ∀ row ∈ g.merged_hz, row.length = g.merged_n) :
    Round.measuredDataObs (g.merged_n + g.merged_hx.length + g.merged_hz.length)
        g.merged_n (SurgeryGadget.extractionRound g)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X g
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z g

theorem extraction_implements_merge (g : SurgeryGadget)
    (hxr : ∀ row ∈ g.merged_hx, row.length = g.merged_n)
    (hzr : ∀ row ∈ g.merged_hz, row.length = g.merged_n)
    (s : StabilizerState) :
    FormalRV.Framework.SurgeryCorrect.measureChecks
        (Round.measuredDataObs (g.merged_n + g.merged_hx.length + g.merged_hz.length)
          g.merged_n (SurgeryGadget.extractionRound g)) s
      = FormalRV.Framework.SurgeryCorrect.measureChecks
          (FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z g)
          (FormalRV.Framework.SurgeryCorrect.measureChecks
            (FormalRV.Framework.SurgeryReadout.merged_stabilizers_X g) s)

theorem extraction_preserves_commuting (g : SurgeryGadget)
    (hxr : ∀ row ∈ g.merged_hx, row.length = g.merged_n)
    (hzr : ∀ row ∈ g.merged_hz, row.length = g.merged_n)
    (s : StabilizerState) (L : PauliString) (hmem : L ∈ s)
    (hcomm : ∀ P ∈ FormalRV.Framework.SurgeryReadout.merged_stabilizers_X g
                ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z g,
        L.commutes P = true) :
    L ∈ FormalRV.Framework.SurgeryCorrect.measureChecks
          (Round.measuredDataObs
            (g.merged_n + g.merged_hx.length + g.merged_hz.length)
            g.merged_n (SurgeryGadget.extractionRound g)) s

theorem extraction_measures_readout (g : SurgeryGadget) (hn : 0 < g.merged_n)
    (signs : List Bool)
    (hxr : ∀ row ∈ g.merged_hx, row.length = g.merged_n)
    (hzr : ∀ row ∈ g.merged_hz, row.length = g.merged_n)
    (hsig : signs.length = g.merged_hx.length)
    (hker : g.targets_logical_correctly = true) :
    ((Round.measuredDataObs
        (g.merged_n + g.merged_hx.length + g.merged_hz.length)
        g.merged_n (SurgeryGadget.extractionRound g)).take g.merged_hx.length
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X g)
    ∧ FormalRV.Framework.SurgeryCorrect.selectedSignedProduct
        g.span_witness g.merged_hx signs

theorem surface3_circuit_measures_merged_and_verifies :
    (Round.measuredDataObs
        (FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery.merged_n
          + FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery.merged_hx.length
          + FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery.merged_hz.length)
        FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery.merged_n
        (SurgeryGadget.extractionRound
          FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X
          FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z
          FormalRV.LatticeSurgery.SurgeryDemoSurface.surface3_x_surgery)

private theorem cxCountC_map_ctrl (a : Nat) (supp : List Nat) :
    cxCountC (supp.map (fun s => PhysOp.cx a s)) = supp.length

private theorem cxCountC_map_tgt (a : Nat) (supp : List Nat) :
    cxCountC (supp.map (fun s => PhysOp.cx s a)) = supp.length

private theorem measCountC_map_ctrl (a : Nat) (supp : List Nat) :
    measCountC (supp.map (fun s => PhysOp.cx a s)) = 0

private theorem measCountC_map_tgt (a : Nat) (supp : List Nat) :
    measCountC (supp.map (fun s => PhysOp.cx s a)) = 0

theorem cxCountC_block (b : CheckBlock) : cxCountC b.ops = b.supp.length

theorem measCountC_block (b : CheckBlock) : measCountC b.ops = 1

theorem measCountC_round (r : Round) : measCountC (Round.ops r) = r.length

theorem cxCountC_round (r : Round) :
    cxCountC (Round.ops r) = (r.map (fun b => b.supp.length)).foldl (· + ·) 0

private def weightSum : BoolMat → Nat
  | []          => 0
  | row :: rest => rowWeight row + weightSum rest

private theorem foldl_add_init (l : List Nat) :
    ∀ (n : Nat), l.foldl (· + ·) n = n + l.foldl (· + ·) 0

private theorem map_rowWeight_foldl (rows : BoolMat) :
    (rows.map rowWeight).foldl (· + ·) 0 = weightSum rows

private theorem cxCountC_xBlocksFrom (rows : BoolMat) :
    ∀ (a : Nat), cxCountC (Round.ops (xBlocksFrom rows a)) = weightSum rows

private theorem cxCountC_zBlocksFrom (rows : BoolMat) :
    ∀ (a : Nat), cxCountC (Round.ops (zBlocksFrom rows a)) = weightSum rows

theorem cxCountC_extractionRound (g : SurgeryGadget) :
    cxCountC (Round.ops (SurgeryGadget.extractionRound g)) = surgeryCNOTs g

theorem measCountC_extractionRound (g : SurgeryGadget) :
    measCountC (Round.ops (SurgeryGadget.extractionRound g)) = surgeryMeasPerRound g

private theorem widthC_map_ctrl (a : Nat) (supp : List Nat) (h : ∀ s ∈ supp, s ≤ a) :
    widthC (supp.map (fun s => PhysOp.cx a s)) ≤ a + 1

private theorem widthC_map_tgt (a : Nat) (supp : List Nat) (h : ∀ s ∈ supp, s ≤ a) :
    widthC (supp.map (fun s => PhysOp.cx s a)) ≤ a + 1

theorem widthC_block (b : CheckBlock) (h : ∀ s ∈ b.supp, s ≤ b.anc) :
    widthC b.ops = b.anc + 1

private theorem widthC_xBlocksFrom (rows : BoolMat) :
    ∀ (a : Nat), (∀ row ∈ rows, row.length ≤ a) → rows ≠ [] →
      widthC (Round.ops (xBlocksFrom rows a)) = a + rows.length

private theorem widthC_zBlocksFrom (rows : BoolMat) :
    ∀ (a : Nat), (∀ row ∈ rows, row.length ≤ a) → rows ≠ [] →
      widthC (Round.ops (zBlocksFrom rows a)) = a + rows.length

private theorem widthC_xBlocksFrom_le (rows : BoolMat) :
    ∀ (a : Nat), (∀ row ∈ rows, row.length ≤ a) →
      widthC (Round.ops (xBlocksFrom rows a)) ≤ a + rows.length

theorem widthC_extractionBlocks (n : Nat) (hx hz : BoolMat)
    (hxr : ∀ row ∈ hx, row.length ≤ n) (hzr : ∀ row ∈ hz, row.length ≤ n)
    (hnz : hz ≠ []) :
    widthC (Round.ops (extractionBlocks n hx hz)) = n + hx.length + hz.length

theorem widthC_extractionRound (g : SurgeryGadget)
    (hxr : ∀ row ∈ g.merged_hx, row.length ≤ g.merged_n)
    (hzr : ∀ row ∈ g.merged_hz, row.length ≤ g.merged_n)
    (hnz : g.merged_hz ≠ []) :
    widthC (Round.ops (SurgeryGadget.extractionRound g)) = surgeryPhysQubits g

private theorem measCountC_replicate (r : Round) :
    ∀ (k : Nat),
      measCountC ((List.replicate k r).flatMap Round.ops) = k * measCountC (Round.ops r)

theorem measCountC_extractionCircuit (g : SurgeryGadget) :
    measCountC (SurgeryGadget.extractionCircuit g) = surgeryTotalMeas g

theorem surface3_extraction_width :
    widthC (Round.ops (SurgeryGadget.extractionRound surface3_x_surgery)) = 28

theorem surface3_extraction_cnots :
    cxCountC (Round.ops (SurgeryGadget.extractionRound surface3_x_surgery)) = 45

theorem surface3_extraction_meas :
    measCountC (Round.ops (SurgeryGadget.extractionRound surface3_x_surgery)) = 14

theorem surface3_extraction_stim_eq :
    toStim (Round.ops (SurgeryGadget.extractionRound surface3_x_surgery))
      = FormalRV.LatticeSurgery.StimEmit.surgeryToStim surface3_x_surgery

theorem cycleOp_ppmVia_size (g : SurgeryGadget) (b : Nat) :
    (FormalRV.QEC.Time.CycleOp.ppmVia g b).size = surgeryPhysQubits g

theorem cycleOp_extractRound_size (c : FormalRV.QEC.CSSCode) (b : Nat) :
    (FormalRV.QEC.Time.CycleOp.extractRound c b).size
      = c.n + c.hx.length + c.hz.length

inductive MeasBasis

inductive PhysOp

abbrev PhysCircuit

def touches : PhysOp → List Nat
  | .prep _ q => [q]
  | .cx c t   => [c, t]
  | .meas _ q => [q]

def isCX : PhysOp → Bool
  | .cx _ _ => true
  | _       => false

def isMeas : PhysOp → Bool
  | .meas _ _ => true
  | _         => false

def isPrep : PhysOp → Bool
  | .prep _ _ => true
  | _         => false

def rowSupportFrom : List Bool → Nat → List Nat
  | [],        _ => []
  | b :: rest, i =>
      if b then i :: rowSupportFrom rest (i + 1)
      else rowSupportFrom rest (i + 1)

def rowSupport (row : List Bool) : List Nat

theorem rowSupportFrom_ge (row : List Bool) :
    ∀ (i : Nat), ∀ j ∈ rowSupportFrom row i, i ≤ j

theorem rowSupportFrom_lt (row : List Bool) :
    ∀ (i : Nat), ∀ j ∈ rowSupportFrom row i, j < i + row.length

theorem rowSupportFrom_nodup (row : List Bool) :
    ∀ (i : Nat), (rowSupportFrom row i).Nodup

theorem rowSupport_lt (row : List Bool) : ∀ j ∈ rowSupport row, j < row.length

theorem rowSupport_nodup (row : List Bool) : (rowSupport row).Nodup

theorem mem_rowSupportFrom (row : List Bool) :
    ∀ (i j : Nat), j ∈ rowSupportFrom row i ↔
      ∃ k, k < row.length ∧ j = i + k ∧ row.getD k false = true

theorem mem_rowSupport (row : List Bool) (j : Nat) :
    j ∈ rowSupport row ↔ j < row.length ∧ row.getD j false = true

theorem rowSupportFrom_length (row : List Bool) :
    ∀ (i : Nat), (rowSupportFrom row i).length = (row.filter (fun b => b)).length

theorem rowSupport_length (row : List Bool) :
    (rowSupport row).length = (row.filter (fun b => b)).length

structure CheckBlock

def ops (b : CheckBlock) : PhysCircuit

theorem ops_length (b : CheckBlock) : b.ops.length = b.supp.length + 2

abbrev Round

def ops (r : Round) : PhysCircuit

theorem ops_append (r s : Round) : Round.ops (r ++ s) = r.ops ++ s.ops

def MeasBasis.prepStim : MeasBasis → String
  | .z => "R"
  | .x => "RX"

def MeasBasis.measStim : MeasBasis → String
  | .z => "M"
  | .x => "MX"

def PhysOp.toStim : PhysOp → String
  | .prep b q => b.prepStim ++ " " ++ toString q ++ "\n"
  | .cx c t   => "CX " ++ toString c ++ " " ++ toString t ++ "\n"
  | .meas b q => b.measStim ++ " " ++ toString q ++ "\n"

def toStim : PhysCircuit → String
  | []        => ""
  | op :: ops => op.toStim ++ toStim ops

def xBlocksFrom : BoolMat → Nat → Round
  | [],          _ => []
  | row :: rest, a => ⟨.x, a, rowSupport row⟩ :: xBlocksFrom rest (a + 1)

def zBlocksFrom : BoolMat → Nat → Round
  | [],          _ => []
  | row :: rest, a => ⟨.z, a, rowSupport row⟩ :: zBlocksFrom rest (a + 1)

def extractionBlocks (n : Nat) (hx hz : BoolMat) : Round

theorem extractionBlocks_length (n : Nat) (hx hz : BoolMat) :
    (extractionBlocks n hx hz).length = hx.length + hz.length

def _root_.FormalRV.QEC.CSSCode.extractionRound (c : FormalRV.QEC.CSSCode) : Round

def _root_.FormalRV.Framework.LDPC.SurgeryGadget.extractionRound
    (g : SurgeryGadget) : Round

def _root_.FormalRV.Framework.LDPC.SurgeryGadget.extractionCircuit
    (g : SurgeryGadget) : PhysCircuit

theorem steane_extraction_stim_eq :
    toStim (Round.ops
        (SurgeryGadget.extractionRound
          FormalRV.LatticeSurgery.SurgeryDemoSteane.steane_x_surgery))
      = FormalRV.LatticeSurgery.StimEmit.surgeryToStim
          FormalRV.LatticeSurgery.SurgeryDemoSteane.steane_x_surgery

private theorem countP_zip_zero_right (a : BoolVec) (m : Nat) :
    (a.zip (zero_vec m)).countP (fun p => p.1 && p.2) = 0

private theorem countP_zip_zero_left (a : BoolVec) (m : Nat) :
    ((zero_vec m).zip a).countP (fun p => p.1 && p.2) = 0

private theorem dotBit_pad_suffix (a b : BoolVec) (m : Nat)
    (h : a.length = b.length) :
    dotBit (a ++ zero_vec m) (b ++ zero_vec m) = dotBit a b

private theorem dotBit_pad_prefix (a b : BoolVec) (m : Nat) :
    dotBit (zero_vec m ++ a) (zero_vec m ++ b) = dotBit a b

private theorem dotBit_cross (a b : BoolVec) (n₁ m₂ : Nat)
    (h : a.length = n₁) :
    dotBit (a ++ zero_vec m₂) (zero_vec n₁ ++ b) = false

def CSSCode.directSum (c₁ c₂ : CSSCode) : CSSCode

def CSSCode.dual (c : CSSCode) : CSSCode

private theorem rows_have_n_cols (mat : BoolMat) (n : Nat)
    (h : matrix_has_n_cols mat n = true) :
    ∀ row ∈ mat, row.length = n

theorem CSSCode.dual_well_shaped (c : CSSCode) (h : c.well_shaped = true) :
    c.dual.well_shaped = true

theorem CSSCode.dual_css_condition (c : CSSCode) (h : c.css_condition = true) :
    c.dual.css_condition = true

theorem CSSCode.dual_valid (c : CSSCode) (h : c.valid = true) :
    c.dual.valid = true

theorem CSSCode.directSum_well_shaped (c₁ c₂ : CSSCode)
    (h₁ : c₁.well_shaped = true) (h₂ : c₂.well_shaped = true) :
    (c₁.directSum c₂).well_shaped = true

theorem CSSCode.directSum_css_condition (c₁ c₂ : CSSCode)
    (h₁ws : c₁.well_shaped = true) (h₂ws : c₂.well_shaped = true)
    (h₁ : c₁.css_condition = true) (h₂ : c₂.css_condition = true) :
    (c₁.directSum c₂).css_condition = true

theorem CSSCode.directSum_valid (c₁ c₂ : CSSCode)
    (h₁ : c₁.valid = true) (h₂ : c₂.valid = true) :
    (c₁.directSum c₂).valid = true

theorem surface3x2_hx_eq_directSum :
    surface3x2_qec.hx = ((surface3.directSum surface3).hx)

theorem surface3x2_hz_eq_directSum :
    surface3x2_qec.hz = ((surface3.directSum surface3).hz)

theorem surface3x2_dual_hx_eq :
    surface3x2_dual.hx = ((surface3.directSum surface3).dual.hx)

theorem surface3x2_dual_hz_eq :
    surface3x2_dual.hz = ((surface3.directSum surface3).dual.hz)

theorem surface3x2_n_eq :
    surface3x2_qec.n = (surface3.directSum surface3).n

theorem surface3x2_dual_n_eq :
    surface3x2_dual.n = ((surface3.directSum surface3).dual).n

def derivedK (c : CSSCode) : Nat

theorem bbSmall_n : bbSmall.n = 18

theorem bbSmall_well_shaped : bbSmall.well_shaped = true

theorem bbSmall_css : bbSmall.css_condition = true

theorem bbSmall_stabilizer_valid : bbSmall.toStabilizerCode.valid = true

theorem bbSmall_k : numLogicals bbSmall = 2

theorem bbSmall_lx_genuine : logicalX_genuine bbSmall = true

theorem bbSmall_lz_genuine : logicalZ_genuine bbSmall = true

def bbSmall_lx : BoolVec

def bbSmallXSurgery : SurgeryGadget

theorem bbSmallXSurgery_verifies :
    SurgeryGadget.verify_surgery_gadget bbSmallXSurgery = true

theorem bbSmall_lx_certified :
    (bbSmall.hz.all (fun r => ! gf2dot r bbSmall_lx)
      && ! inRowspace bbSmall.hx bbSmall_lx) = true

def bbSmallXSurgery_merged_css : FormalRV.QEC.CSSCode

theorem bbSmallXSurgery_merged_syndrome_valid :
    StabilizerState.valid bbSmallXSurgery_merged_css.toStabilizers bbSmallXSurgery_merged_css.n = true

theorem bbSmall_circuit_measures_merged :
    Round.measuredDataObs
        (bbSmallXSurgery.merged_n + bbSmallXSurgery.merged_hx.length
          + bbSmallXSurgery.merged_hz.length)
        bbSmallXSurgery.merged_n (SurgeryGadget.extractionRound bbSmallXSurgery)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X bbSmallXSurgery
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z bbSmallXSurgery

theorem bbSmall_circuit_readout (signs : List Bool)
    (hsig : signs.length = bbSmallXSurgery.merged_hx.length) :
    ((Round.measuredDataObs
        (bbSmallXSurgery.merged_n + bbSmallXSurgery.merged_hx.length
          + bbSmallXSurgery.merged_hz.length)
        bbSmallXSurgery.merged_n
        (SurgeryGadget.extractionRound bbSmallXSurgery)).take
          bbSmallXSurgery.merged_hx.length
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X bbSmallXSurgery)
    ∧ FormalRV.Framework.SurgeryCorrect.selectedSignedProduct
        bbSmallXSurgery.span_witness bbSmallXSurgery.merged_hx signs
      = FormalRV.Framework.SurgeryCorrect.signedXRow

theorem bbSmall_circuit_width :
    FormalRV.Resource.widthC
        (Round.ops (SurgeryGadget.extractionRound bbSmallXSurgery)) = 39

theorem bbSmall_circuit_cnots :
    FormalRV.Resource.cxCountC
        (Round.ops (SurgeryGadget.extractionRound bbSmallXSurgery)) = 77

theorem bbSmall_circuit_meas :
    FormalRV.Resource.measCountC
        (Round.ops (SurgeryGadget.extractionRound bbSmallXSurgery)) = 20

def bbTwoPPMpar : CycleSchedule

theorem bb_par_wellFormed : bbTwoPPMpar.wellFormed = true

theorem bb_par_duration : bbTwoPPMpar.duration = 4

abbrev code (l m : Nat) (a b : List (Nat × Nat)) : FormalRV.QEC.CSSCode

abbrev checkMatrixX (l m : Nat) (a b : List (Nat × Nat)) : BoolMat

abbrev checkMatrixZ (l m : Nat) (a b : List (Nat × Nat)) : BoolMat

abbrev stabilizers (l m : Nat) (a b : List (Nat × Nat)) : List PauliString

abbrev extractionRound (l m : Nat) (a b : List (Nat × Nat)) : Round

abbrev extractionStim (l m : Nat) (a b : List (Nat × Nat)) : String

theorem code_n (l m : Nat) (a b : List (Nat × Nat)) :
    (code l m a b).n = 2 * l * m

theorem family_extraction_measures (l m : Nat) (a b : List (Nat × Nat))
    (h : (code l m a b).well_shaped = true) :
    Round.measuredDataObs
        ((code l m a b).n + (code l m a b).hx.length + (code l m a b).hz.length)
        (code l m a b).n (extractionRound l m a b)
      = (code l m a b).toStabilizers

def bb16 : FormalRV.QEC.CSSCode

theorem bb16_n : bb16.n = 16

theorem bb16_valid : bb16.valid = true

theorem bb16_extraction_measures :
    Round.measuredDataObs
        (bb16.n + bb16.hx.length + bb16.hz.length)
        bb16.n (FormalRV.QEC.CSSCode.extractionRound bb16)
      = bb16.toStabilizers

def hgp73 : FormalRV.QEC.CSSCode

theorem hgp73_n : hgp73.n = 27

theorem hgp73_well_shaped : hgp73.well_shaped = true

theorem hgp73_css : hgp73.css_condition = true

theorem hgp73_stabilizer_valid : hgp73.toStabilizerCode.valid = true

theorem hgp73_k : numLogicals hgp73 = 4

theorem hgp73_logicalX_genuine : logicalX_genuine hgp73 = true

theorem hgp73_logicalZ_genuine : logicalZ_genuine hgp73 = true

def hgp73_lx : BoolVec

def hgp73XSurgery : SurgeryGadget

theorem hgp73XSurgery_verifies :
    SurgeryGadget.verify_surgery_gadget hgp73XSurgery = true

theorem hgp73_lx_certified :
    (hgp73.hz.all (fun r => ! gf2dot r hgp73_lx)
      && ! inRowspace hgp73.hx hgp73_lx) = true

def hgp73XSurgery_merged_css : FormalRV.QEC.CSSCode

theorem hgp73XSurgery_merged_syndrome_valid :
    StabilizerState.valid hgp73XSurgery_merged_css.toStabilizers hgp73XSurgery_merged_css.n = true

theorem hgp73_circuit_measures_merged :
    Round.measuredDataObs
        (hgp73XSurgery.merged_n + hgp73XSurgery.merged_hx.length
          + hgp73XSurgery.merged_hz.length)
        hgp73XSurgery.merged_n (SurgeryGadget.extractionRound hgp73XSurgery)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X hgp73XSurgery
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z hgp73XSurgery

theorem hgp73_circuit_readout (signs : List Bool)
    (hsig : signs.length = hgp73XSurgery.merged_hx.length) :
    ((Round.measuredDataObs
        (hgp73XSurgery.merged_n + hgp73XSurgery.merged_hx.length
          + hgp73XSurgery.merged_hz.length)
        hgp73XSurgery.merged_n
        (SurgeryGadget.extractionRound hgp73XSurgery)).take
          hgp73XSurgery.merged_hx.length
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X hgp73XSurgery)
    ∧ FormalRV.Framework.SurgeryCorrect.selectedSignedProduct
        hgp73XSurgery.span_witness hgp73XSurgery.merged_hx signs
      = FormalRV.Framework.SurgeryCorrect.signedXRow

theorem hgp73_circuit_width :
    FormalRV.Resource.widthC
        (Round.ops (SurgeryGadget.extractionRound hgp73XSurgery)) = 53

theorem hgp73_circuit_cnots :
    FormalRV.Resource.cxCountC
        (Round.ops (SurgeryGadget.extractionRound hgp73XSurgery)) = 105

theorem hgp73_circuit_meas :
    FormalRV.Resource.measCountC
        (Round.ops (SurgeryGadget.extractionRound hgp73XSurgery)) = 25

def hgp73TwoPPMpar : CycleSchedule

theorem hgp73_par_wellFormed : hgp73TwoPPMpar.wellFormed = true

theorem hgp73_par_duration : hgp73TwoPPMpar.duration = 2

abbrev code (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : FormalRV.QEC.CSSCode

abbrev checkMatrixX (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : BoolMat

abbrev checkMatrixZ (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : BoolMat

abbrev stabilizers (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : List PauliString

abbrev extractionRound (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : Round

abbrev extractionStim (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : String

theorem code_n (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) :
    (code h1 h2 m1 n1 m2 n2).n = n1 * n2 + m1 * m2

theorem family_extraction_measures (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat)
    (h : (code h1 h2 m1 n1 m2 n2).well_shaped = true) :
    Round.measuredDataObs
        ((code h1 h2 m1 n1 m2 n2).n + (code h1 h2 m1 n1 m2 n2).hx.length
          + (code h1 h2 m1 n1 m2 n2).hz.length)
        (code h1 h2 m1 n1 m2 n2).n (extractionRound h1 h2 m1 n1 m2 n2)
      = (code h1 h2 m1 n1 m2 n2).toStabilizers

def hgp_rep34 : FormalRV.QEC.CSSCode

theorem hgp_rep34_n : hgp_rep34.n = 18

theorem hgp_rep34_valid : hgp_rep34.valid = true

theorem hgp_rep34_extraction_measures :
    Round.measuredDataObs
        (hgp_rep34.n + hgp_rep34.hx.length + hgp_rep34.hz.length)
        hgp_rep34.n (FormalRV.QEC.CSSCode.extractionRound hgp_rep34)
      = hgp_rep34.toStabilizers

theorem lp16ImportedBasis_valid : (lp16ImportedBasis).valid = true

def lp16Imported_lzBits : List Nat

def lp16Imported_lxBits : List Nat

def lp16Imported_lz : List FormalRV.Framework.LDPC.BoolVec

def lp16Imported_lx : List FormalRV.Framework.LDPC.BoolVec

def lp16ImportedBasis : LogicalBasis FormalRV.QEC.Instances.lp16 744

theorem lp16_basis_bitsCert :
    validBitsCert (matBits FormalRV.QEC.Instances.lp16.hx)
        (matBits FormalRV.QEC.Instances.lp16.hz)
        lp16Imported_lxBits lp16Imported_lzBits = true

def lp16_lz0 : BoolVec

def lp16_lx0 : BoolVec

theorem lp16_lz0_in_ker_hx :
    (FormalRV.QEC.Instances.lp16.hx.all (fun r => ! dotBit r lp16_lz0)) = true

theorem lp16_lx0_in_ker_hz :
    (FormalRV.QEC.Instances.lp16.hz.all (fun r => ! dotBit r lp16_lx0)) = true

theorem lp16_lx0_lz0_paired : dotBit lp16_lx0 lp16_lz0 = true

def lp16Block : CodeBlock

def lp16Layout : BlockLayout

theorem lp16Layout_wfStructural : lp16Layout.wfStructural = true

theorem lp16Layout_wf (hvalid : lp16ImportedBasis.valid = true) :
    lp16Layout.wf = true

def lp16DemoPPM : VirtualPPM

theorem lp16DemoPPM_inRange : lp16Layout.inRange lp16DemoPPM = true

theorem lp16DemoPPM_resolves :
    lp16Layout.resolve lp16DemoPPM = [(⟨0, 2⟩, .x), (⟨0, 3⟩, .z)]

theorem lp16DemoPPM_renders :
    lp16Layout.render lp16DemoPPM = "Measure X[LP0(2)] Z[LP0(3)] "

theorem lp20ImportedBasis_valid : (lp20ImportedBasis).valid = true

def lp20Imported_lzBits : List Nat

def lp20Imported_lxBits : List Nat

def lp20Imported_lz : List FormalRV.Framework.LDPC.BoolVec

def lp20Imported_lx : List FormalRV.Framework.LDPC.BoolVec

def lp20ImportedBasis : LogicalBasis FormalRV.QEC.Instances.lp20 1224

theorem lpTiny_n : lpTiny.n = 15

theorem lpTiny_well_shaped : lpTiny.well_shaped = true

theorem lpTiny_css : lpTiny.css_condition = true

theorem lpTiny_stabilizer_valid : lpTiny.toStabilizerCode.valid = true

theorem lp_corpus_well_shaped :
    FormalRV.QEC.Instances.lp16.well_shaped = true
    ∧ FormalRV.QEC.Instances.lp20.well_shaped = true
    ∧ FormalRV.QEC.Instances.lp24.well_shaped = true

theorem lpTiny_k : numLogicals lpTiny = 3

theorem lpTiny_lx_genuine : logicalX_genuine lpTiny = true

theorem lpTiny_lz_genuine : logicalZ_genuine lpTiny = true

def lpTiny_lx : BoolVec

def lpTinyXSurgery : SurgeryGadget

theorem lpTinyXSurgery_verifies :
    SurgeryGadget.verify_surgery_gadget lpTinyXSurgery = true

theorem lpTiny_lx_certified :
    (lpTiny.hz.all (fun r => ! gf2dot r lpTiny_lx)
      && ! inRowspace lpTiny.hx lpTiny_lx) = true

def lpTinyXSurgery_merged_css : FormalRV.QEC.CSSCode

theorem lpTinyXSurgery_merged_syndrome_valid :
    StabilizerState.valid lpTinyXSurgery_merged_css.toStabilizers lpTinyXSurgery_merged_css.n = true

theorem lpTiny_circuit_measures_merged :
    Round.measuredDataObs
        (lpTinyXSurgery.merged_n + lpTinyXSurgery.merged_hx.length
          + lpTinyXSurgery.merged_hz.length)
        lpTinyXSurgery.merged_n (SurgeryGadget.extractionRound lpTinyXSurgery)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X lpTinyXSurgery
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z lpTinyXSurgery

theorem lpTiny_circuit_readout (signs : List Bool)
    (hsig : signs.length = lpTinyXSurgery.merged_hx.length) :
    ((Round.measuredDataObs
        (lpTinyXSurgery.merged_n + lpTinyXSurgery.merged_hx.length
          + lpTinyXSurgery.merged_hz.length)
        lpTinyXSurgery.merged_n
        (SurgeryGadget.extractionRound lpTinyXSurgery)).take
          lpTinyXSurgery.merged_hx.length
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X lpTinyXSurgery)
    ∧ FormalRV.Framework.SurgeryCorrect.selectedSignedProduct
        lpTinyXSurgery.span_witness lpTinyXSurgery.merged_hx signs
      = FormalRV.Framework.SurgeryCorrect.signedXRow

theorem lpTiny_circuit_width :
    FormalRV.Resource.widthC
        (Round.ops (SurgeryGadget.extractionRound lpTinyXSurgery)) = 30

theorem lpTiny_circuit_cnots :
    FormalRV.Resource.cxCountC
        (Round.ops (SurgeryGadget.extractionRound lpTinyXSurgery)) = 40

theorem lpTiny_circuit_meas :
    FormalRV.Resource.measCountC
        (Round.ops (SurgeryGadget.extractionRound lpTinyXSurgery)) = 14

def lpTwoPPMpar : CycleSchedule

theorem lp_par_wellFormed : lpTwoPPMpar.wellFormed = true

theorem lp_par_duration : lpTwoPPMpar.duration = 2

abbrev code (l : Nat) (A : List (List Circ)) (rA nA : Nat) : FormalRV.QEC.CSSCode

abbrev checkMatrixX (l : Nat) (A : List (List Circ)) (rA nA : Nat) : BoolMat

abbrev checkMatrixZ (l : Nat) (A : List (List Circ)) (rA nA : Nat) : BoolMat

abbrev stabilizers (l : Nat) (A : List (List Circ)) (rA nA : Nat) : List PauliString

abbrev extractionRound (l : Nat) (A : List (List Circ)) (rA nA : Nat) : Round

abbrev extractionStim (l : Nat) (A : List (List Circ)) (rA nA : Nat) : String

theorem code_n (l : Nat) (A : List (List Circ)) (rA nA : Nat) :
    (code l A rA nA).n = (rA * rA + nA * nA) * l

theorem family_extraction_measures (l : Nat) (A : List (List Circ)) (rA nA : Nat)
    (h : (code l A rA nA).well_shaped = true) :
    Round.measuredDataObs
        ((code l A rA nA).n + (code l A rA nA).hx.length
          + (code l A rA nA).hz.length)
        (code l A rA nA).n (extractionRound l A rA nA)
      = (code l A rA nA).toStabilizers

def lp25 : FormalRV.QEC.CSSCode

theorem lp25_n : lp25.n = 25

theorem lp25_valid : lp25.valid = true

theorem lp25_extraction_measures :
    Round.measuredDataObs
        (lp25.n + lp25.hx.length + lp25.hz.length)
        lp25.n (FormalRV.QEC.CSSCode.extractionRound lp25)
      = lp25.toStabilizers

theorem lpTinyImportedBasis_valid : (lpTinyImportedBasis).valid = true

def lpTinyImported_lzBits : List Nat

def lpTinyImported_lxBits : List Nat

def lpTinyImported_lz : List FormalRV.Framework.LDPC.BoolVec

def lpTinyImported_lx : List FormalRV.Framework.LDPC.BoolVec

def lpTinyImportedBasis : LogicalBasis FormalRV.QEC.Algebraic.lpTiny 3

def colSupp (d col : Nat) : List Nat

def rowSupp' (d row : Nat) : List Nat

def logicalXSupp (d : Nat) : List Nat

def logicalZSupp (d : Nat) : List Nat

def logicalX (d : Nat) : BoolVec

def logicalZ (d : Nat) : BoolVec

def isXLogical (d : Nat) (v : BoolVec) : Bool

def isZLogical (d : Nat) (v : BoolVec) : Bool

theorem logicalX3_valid : isXLogical 3 (logicalX 3) = true

theorem logicalZ3_valid : isZLogical 3 (logicalZ 3) = true

theorem logicalX5_valid : isXLogical 5 (logicalX 5) = true

theorem logicalZ5_valid : isZLogical 5 (logicalZ 5) = true

theorem logicalX7_valid : isXLogical 7 (logicalX 7) = true

theorem logicalZ7_valid : isZLogical 7 (logicalZ 7) = true

theorem logicalX27_valid : isXLogical 27 (logicalX 27) = true

theorem logicalZ27_valid : isZLogical 27 (logicalZ 27) = true

theorem logicalXZ27_anticommute : gf2dot (logicalX 27) (logicalZ 27) = true

theorem logicalXSupp27_length : (logicalXSupp 27).length = 27

def ridx (d r c : Nat) : Nat

def faceSupp (d a b : Nat) : List Nat

def faceActive (d a b : Nat) : Bool

def colourFaces (d : Nat) (xColour : Bool) : List (Nat × Nat)

def suppRow (d : Nat) (supp : List Nat) : BoolVec

def colourChecks (d : Nat) (xColour : Bool) : BoolMat

def rotatedSurface (d : Nat) : CSSCode

theorem suppRow_length (d : Nat) (supp : List Nat) :
    (suppRow d supp).length = d * d

theorem colourChecks_rows_len (d : Nat) (xColour : Bool) :
    ∀ row ∈ colourChecks d xColour, row.length = d * d

theorem rotatedSurface_well_shaped (d : Nat) :
    (rotatedSurface d).well_shaped = true

theorem rotatedSurface3_valid : (rotatedSurface 3).valid = true

theorem rotatedSurface3_counts :
    (rotatedSurface 3).hx.length = 4 ∧ (rotatedSurface 3).hz.length = 4

theorem rotatedSurface5_valid : (rotatedSurface 5).valid = true

theorem rotatedSurface7_valid : (rotatedSurface 7).valid = true

def rotatedSyndromeQubits (d : Nat) : Nat

def rotatedPhysicalQubits (d : Nat) : Nat

theorem rotated3_physical : rotatedPhysicalQubits 3 = 17

theorem rotated5_physical : rotatedPhysicalQubits 5 = 49

theorem rotatedSurface27_valid : (rotatedSurface 27).valid = true

theorem rotatedSurface27_counts :
    (rotatedSurface 27).n = 729
      ∧ (rotatedSurface 27).hx.length = 364
      ∧ (rotatedSurface 27).hz.length = 364

theorem rotated27_physical : rotatedPhysicalQubits 27 = 1457

theorem rotated27_vs_paper_footprint :
    rotatedPhysicalQubits 27 = 1457        -- data + syndrome (this code)
      ∧ 2 * (27 + 1) * (27 + 1) = 1568     -- paper per-patch (with spacing)
      ∧ 1568 - 1457 = 111

theorem surface3_n : surface3.n = 13

theorem surface3_well_shaped : surface3.well_shaped = true

theorem surface3_css : surface3.css_condition = true

theorem surface3_stabilizer_valid : surface3.toStabilizerCode.valid = true

theorem surface3_k : numLogicals surface3 = 1

theorem surface3_lx_genuine : logicalX_genuine surface3 = true

theorem surface3_lz_genuine : logicalZ_genuine surface3 = true

theorem surface3_x_surgery_is_canonical :
    SurgeryGadget.merged_hx
        (canonicalXSurgery surface3_qec
          [false, false, false, false, false, false, true, true, true,
           false, false, false, false] 2 4)
      = SurgeryGadget.merged_hx surface3_x_surgery

theorem surface3_x_surgery_canonical_fields :
    (SurgeryGadget.merged_hz
        (canonicalXSurgery surface3_qec
          [false, false, false, false, false, false, true, true, true,
           false, false, false, false] 2 4)
      = SurgeryGadget.merged_hz surface3_x_surgery)
    ∧ ((canonicalXSurgery surface3_qec
          [false, false, false, false, false, false, true, true, true,
           false, false, false, false] 2 4).target_pauli
      = surface3_x_surgery.target_pauli)
    ∧ ((canonicalXSurgery surface3_qec
          [false, false, false, false, false, false, true, true, true,

theorem surface3_gadget_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_x_surgery = true

theorem surface3_circuit_measures_merged :
    Round.measuredDataObs
        (surface3_x_surgery.merged_n + surface3_x_surgery.merged_hx.length
          + surface3_x_surgery.merged_hz.length)
        surface3_x_surgery.merged_n
        (SurgeryGadget.extractionRound surface3_x_surgery)
      = FormalRV.Framework.SurgeryReadout.merged_stabilizers_X surface3_x_surgery
        ++ FormalRV.Framework.SurgeryCorrect.merged_stabilizers_Z surface3_x_surgery

theorem surface3_circuit_width_28 :
    FormalRV.Resource.widthC
        (Round.ops (SurgeryGadget.extractionRound surface3_x_surgery)) = 28

theorem surface3_par_duration :
    FormalRV.QEC.Time.CycleSchedule.duration
      FormalRV.QEC.Time.CycleSchedule.twoPPMpar = 2

abbrev code (d : Nat) : FormalRV.QEC.CSSCode

abbrev checkMatrixX (d : Nat) : FormalRV.Framework.LDPC.BoolMat

abbrev checkMatrixZ (d : Nat) : FormalRV.Framework.LDPC.BoolMat

abbrev stabilizers (d : Nat) : List PauliString

abbrev extractionRound (d : Nat) : Round

abbrev extractionStim (d : Nat) : String

theorem code_n (d : Nat) : (code d).n = d * d + (d - 1) * (d - 1)

theorem family_extraction_measures (d : Nat)
    (h : (code d).well_shaped = true) :
    Round.measuredDataObs
        ((code d).n + (code d).hx.length + (code d).hz.length)
        (code d).n (extractionRound d)
      = (code d).toStabilizers

theorem code3_valid : (code 3).valid = true

theorem code5_well_shaped : (code 5).well_shaped = true

theorem code5_css : (code 5).css_condition = true

theorem code5_extraction_measures :
    Round.measuredDataObs
        ((code 5).n + (code 5).hx.length + (code 5).hz.length)
        (code 5).n (extractionRound 5)
      = (code 5).toStabilizers

def colorCodeD3 : CSSCode

theorem colorCodeD3_selfDual : colorCodeD3.hx = colorCodeD3.hz

theorem transversalH_is_logicalH :
    colorCodeD3.hx = colorCodeD3.hz ∧
      steaneLogical.lx = steaneLogical.lz

inductive Step
  | inject       -- create the encoded `|T⟩` in a `d=3` color code (fault distance 1)
  | check        -- the double-cat controlled-`H_XY` check (raises fault distance)
  | grow         -- enlarge the color code via Bell-pair preparation
  | stabilize    -- superdense color-code cycles (×3) to settle new stabilizers
  | escape       -- graft into a large matchable surface code
  deriving DecidableEq, Repr

def cultivationCycle : List Step

def cultivationPipeline (d : Nat) : List Step

theorem cultivationPipeline_d3 :
    cultivationPipeline 3 = [.inject, .check, .grow, .stabilize, .escape]

theorem cultivationPipeline_d5 :
    cultivationPipeline 5 =
      [.inject, .check, .grow, .stabilize, .check, .grow, .stabilize, .escape]

theorem check_step_correct :
    ctrlHXY * plusT = plusT
      ∧ ctrlHXY * plusTm = minusTm
      ∧ hXY * magicT = magicT

def d3CatCheckQubits : Nat

def d3CatCheckLayers : Nat

def stabilizeCycles : Nat

structure TFactory

def TFactory.correct (F : TFactory) : Prop

def TFactory.volume (F : TFactory) : Nat

def colorCodeQubits (d : Nat) : Nat

def cultivationMinDistance : Nat

noncomputable def cultivationFactory (d : Nat) : TFactory

theorem cultivationFactory_correct (d : Nat) : (cultivationFactory d).correct

noncomputable def cultivationTFactory : TFactory

theorem cultivationTFactory_correct : cultivationTFactory.correct

theorem cultivationFactory_d3 :
    (cultivationFactory 3).qubits = 15
      ∧ (cultivationFactory 3).rounds = 24
      ∧ (cultivationFactory 3).attempts = 4

theorem factory_tGate_correct (F : TFactory) (hF : F.correct) (ψ : StateVec 1) :
    (projLow0 * (cnotMatrix * (ψ ⊗ᵥ F.output))
        = (1 / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1)))
    ∧ (Shigh * (projLow1 * (cnotMatrix * (ψ ⊗ᵥ F.output)))
        = (EightTToCCZ.ω / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1)))

theorem cultivation_tGate_correct (ψ : StateVec 1) :
    (projLow0 * (cnotMatrix * (ψ ⊗ᵥ cultivationTFactory.output))
        = (1 / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1)))
    ∧ (Shigh * (projLow1 * (cnotMatrix * (ψ ⊗ᵥ cultivationTFactory.output)))
        = (EightTToCCZ.ω / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1)))

theorem cultivationFactory_tGate_correct (d : Nat) (ψ : StateVec 1) :
    (projLow0 * (cnotMatrix * (ψ ⊗ᵥ (cultivationFactory d).output))
        = (1 / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1)))
    ∧ (Shigh * (projLow1 * (cnotMatrix * (ψ ⊗ᵥ (cultivationFactory d).output)))
        = (EightTToCCZ.ω / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1)))

structure Cost

def Cost.zero : Cost

def Cost.add (a b : Cost) : Cost

instance : Add Cost

instance : Zero Cost

def cliffordSurgeryVol : Nat

def TFactory.perT (F : TFactory) : Cost

def tBlockCost (F : TFactory) : Cost

inductive Op
  | tGate
  | clifford
deriving DecidableEq, Repr

def opCost (F : TFactory) : Op → Cost
  | .tGate    => tBlockCost F
  | .clifford => ⟨0, 0, cliffordSurgeryVol⟩

def circuitCost (F : TFactory) : List Op → Cost
  | [] => 0
  | o :: t => opCost F o + circuitCost F t

def numTGates (c : List Op) : Nat

def exampleCircuit : List Op

theorem exampleCircuit_numT : numTGates exampleCircuit = 3

theorem exampleCircuit_cost_cultivation :
    circuitCost cultivationTFactory exampleCircuit
      = ⟨3, 3 * (15 * 24 * 4), 7 * 6⟩

theorem circuitCost_magic (F : TFactory) (c : List Op) :
    (circuitCost F c).magic = numTGates c

theorem circuitCost_factoryVol (F : TFactory) (c : List Op) :
    (circuitCost F c).factoryVol = numTGates c * F.volume

theorem cultivationFactory_volume (d : Nat) :
    (cultivationFactory d).volume = (2 * colorCodeQubits d + 1) * (8 * d) * 4

theorem circuitCost_cultivation_factoryVol (d : Nat) (c : List Op) :
    (circuitCost (cultivationFactory d) c).factoryVol
      = numTGates c * ((2 * colorCodeQubits d + 1) * (8 * d) * 4)

theorem exampleCircuit_factoryVol (d : Nat) :
    (circuitCost (cultivationFactory d) exampleCircuit).factoryVol
      = 3 * ((2 * colorCodeQubits d + 1) * (8 * d) * 4)

noncomputable def s : ℂ

noncomputable def ω : ℂ

noncomputable def cω : ℂ

lemma omega_eq_exp : ω = Complex.exp (↑(Real.pi / 4) * I)

def hXY : Matrix (Fin 2) (Fin 2) ℂ

lemma hXY_eq_sum : hXY = s • σx + s • σy

def tGate : Matrix (Fin 2) (Fin 2) ℂ

def magicT : Matrix (Fin 2) (Fin 1) ℂ

def magicTm : Matrix (Fin 2) (Fin 1) ℂ

def plusKet : Matrix (Fin 2) (Fin 1) ℂ

lemma magicT_eq : magicT = tGate * plusKet

theorem hXY_stabilizes_magicT : hXY * magicT = magicT

theorem hXY_antistabilizes_magicTm : hXY * magicTm = -magicTm

theorem tConj_X_eq_hXY : tGate * σx * tGateᴴ = hXY

def ctrlHXY : Matrix (Fin 4) (Fin 4) ℂ

noncomputable def c : ℂ

def plusT  : Matrix (Fin 4) (Fin 1) ℂ

def plusTm : Matrix (Fin 4) (Fin 1) ℂ

def minusTm : Matrix (Fin 4) (Fin 1) ℂ

theorem ctrlHXY_check_passes : ctrlHXY * plusT = plusT

theorem ctrlHXY_check_detects : ctrlHXY * plusTm = minusTm

def identMat (n : Nat) : BoolMat

def kron (A B : BoolMat) : BoolMat

example : kron [[true]] (identMat 3) = identMat 3

example : (kron (identMat 2) (identMat 3)).length = 2 * 3

example : kron (identMat 2) (identMat 2) = identMat 4

def hypergraphProduct (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : CSSCode

def repCode (d : Nat) : BoolMat

def surfaceHGP (d : Nat) : CSSCode

example : (surfaceHGP 3).n = 13

example : (surfaceHGP 3).well_shaped = true

example : (surfaceHGP 3).css_condition = true

def shiftMat (l : Nat) : BoolMat

def shiftPow (l k : Nat) : BoolMat

def matXor (A B : BoolMat) : BoolMat

def biCirculant (l m : Nat) (terms : List (Nat × Nat)) : BoolMat

def bivariateBicycle (l m : Nat) (a b : List (Nat × Nat)) : CSSCode

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).n = 18

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).well_shaped = true

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).css_condition = true

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).n = 72

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).well_shaped = true

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).css_condition = true

abbrev Circ

def circulant (l : Nat) (p : Circ) : BoolMat

def circDagger (l : Nat) (p : Circ) : Circ

example : circulant 3 [1] = shiftMat 3

example : circDagger 3 [1] = [2]

example : circulant 3 (circDagger 3 [1]) = transpose (circulant 3 [1]) 3

example : circulant 4 (circDagger 4 [1, 2]) = transpose (circulant 4 [1, 2]) 4

def liftMat (ℓ : Nat) (A : List (List Circ)) : BoolMat

def pIdent (n : Nat) : List (List Circ)

def pDagger (ℓ : Nat) (A : List (List Circ)) : List (List Circ)

def circMul (ℓ : Nat) (p q : Circ) : Circ

def pKron (ℓ : Nat) (A B : List (List Circ)) : List (List Circ)

def pHcat (L R : List (List Circ)) : List (List Circ)

def liftedProduct (ℓ : Nat) (A : List (List Circ)) (rA nA : Nat) : CSSCode

def lpTiny : CSSCode

example : lpTiny.n = (1 * 1 + 2 * 2) * 3

example : lpTiny.well_shaped = true

example : lpTiny.css_condition = true

example : StabilizerState.valid (lpTiny.toStabilizers) lpTiny.n = true

theorem surfaceHGP3_circuit_implements :
    StabilizerState.valid ((surfaceHGP 3).toStabilizers) (surfaceHGP 3).n = true

theorem tinyBB_circuit_implements :
    StabilizerState.valid
      ((bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).toStabilizers)
      (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).n = true

def parityFold (x : Nat) : Bool

def dotBitN (a b : Nat) : Bool

def allOrthoBits (rows : List Nat) (v : Nat) : Bool

def pairsDeltaBits (lxs lzs : List Nat) : Bool

def matBits (m : BoolMat) : List Nat

def validBitsCert (hxB hzB : List Nat) (lxs lzs : List Nat) : Bool

example : dotBitN 0b1011 0b1110 = false

example : dotBitN 0b1011 0b0110 = true

example : parityFold 0 = false

example : parityFold (2 ^ 4095) = true

example :
    dotBitN (vecToBits [true, false, true]) (vecToBits [true, true, true])
      = dotBit [true, false, true] [true, true, true]

def dotBit (a b : BoolVec) : Bool

def transpose (mat : BoolMat) (ncols : Nat) : BoolMat

def mat_mul_transpose (a b : BoolMat) : BoolMat

def orthogonal (a b : BoolMat) : Bool

theorem orthogonal_iff (a b : BoolMat) :
    orthogonal a b = true ↔
      ∀ ra ∈ a, ∀ rb ∈ b, dotBit ra rb = false

example : dotBit [true, false, true] [true, true, true] = false

example : dotBit [true, true, false] [true, true, true] = false

example : dotBit [true, false, false] [true, true, true] = true

example :
    orthogonal
      [ [false, false, false, true,  true,  true,  true ]
      , [false, true,  true,  false, false, true,  true ]
      , [true,  false, true,  false, true,  false, true ] ]
      [ [false, false, false, true,  true,  true,  true ]
      , [false, true,  true,  false, false, true,  true ]
      , [true,  false, true,  false, true,  false, true ] ] = true

theorem vec_xor_cons (x y : Bool) (xs ys : BoolVec) :
    vec_xor (x :: xs) (y :: ys) = (x != y) :: vec_xor xs ys

theorem count_xor_parity (a c b : BoolVec) (hac : a.length = c.length) (hab : a.length = b.length) :
    ((vec_xor a c).zip b).countP (fun p => p.1 && p.2) % 2
      = (((a.zip b).countP (fun p => p.1 && p.2)) + ((c.zip b).countP (fun p => p.1 && p.2))) % 2

theorem parity_add (m n : Nat) :
    decide ((m + n) % 2 = 1) = xor (decide (m % 2 = 1)) (decide (n % 2 = 1))

theorem dotBit_vec_xor (a c b : BoolVec) (hac : a.length = c.length) (hab : a.length = b.length) :
    dotBit (vec_xor a c) b = xor (dotBit a b) (dotBit c b)

def leadIdx (v : BoolVec) : Option Nat

def reduceVec (pivots : BoolMat) (v : BoolVec) : BoolVec

def rowReduce (mat : BoolMat) : BoolMat

def rank (mat : BoolMat) : Nat

def inRowspace (mat : BoolMat) (v : BoolVec) : Bool

def steaneH : BoolMat

example : rank steaneH = 3

example : inRowspace steaneH [false, false, false, true, true, true, true] = true

example :
    inRowspace steaneH
      (vec_xor [false, false, false, true, true, true, true]
               [false, true,  true,  false, false, true, true]) = true

example : inRowspace steaneH [true, true, true, true, true, true, true] = false

example : rank (steaneH ++ [[true, true, true, true, true, true, true]]) = 4

example : measGadgetConj [0, 1, 2, 3] 4
      ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.I, Pauli.I, Pauli.Z]⟩
    = ⟨Phase.plus, [Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z]⟩

example : xMeasGadgetConj [0, 1, 2, 3] 4
      ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.I, Pauli.I, Pauli.X]⟩
    = ⟨Phase.plus, [Pauli.X, Pauli.X, Pauli.X, Pauli.X, Pauli.X]⟩

example : code422.toStabilizers
    = [⟨Phase.plus, [Pauli.X, Pauli.X, Pauli.X, Pauli.X]⟩,
       ⟨Phase.plus, [Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z]⟩]

example : StabilizerState.valid code422.toStabilizers code422.n = true

theorem code422_syndrome_circuit_valid :
    StabilizerState.valid code422.toStabilizers code422.n = true

structure PhysResources

def physQubits (r : PhysResources) : Nat

def rowWeight (row : BoolVec) : Nat

def syndromeCost (c : CSSCode) : PhysResources

example : syndromeCost code422
    = { data_qubits

example : physQubits (syndromeCost code422) = 6

def gadgetDataQubits (g : Gate) : Nat

theorem gadgetDataQubits_eq (g : Gate) :
    gadgetDataQubits g = Resource.width g * (Codes.Surface.rotatedSurface 27).n

def gadgetSyndromeQubits (g : Gate) : Nat

theorem gadgetSyndromeQubits_eq_measCount (g : Gate) :
    gadgetSyndromeQubits g = measCountC (gadgetPhysical g)

def gadgetMergeCount (g : Gate) : Nat

def mergeAncillaFootprint : Nat

theorem mergeAncillaFootprint_eq :
    mergeAncillaFootprint
      = (Codes.Surface.rotatedSurface 27).n
        + 27 * ((Codes.Surface.rotatedSurface 27).hx.length
            + (Codes.Surface.rotatedSurface 27).hz.length)

def gadgetMergeAncilla (g : Gate) : Nat

structure PhysReport

def gadgetTotalPhysQubits (g : Gate) : Nat

def gadgetReport (g : Gate) : PhysReport

theorem lattice_surgery_not_free (g : Gate) (h : 0 < gadgetMergeCount g) :
    gadgetDataQubits g + gadgetSyndromeQubits g < gadgetTotalPhysQubits g

def stmtMeasurements : PPMStmt → List PauliProduct
  | .measure _ P              => [P]
  | .measureSel _ _ Pt Pe     => [Pt, Pe]
  | .measureSel2 _ _ _ a b c d => [a, b, c, d]
  | _                         => []

def programMeasurements (prog : PPMProg) : List PauliProduct

def factorAxis (f : PFactor) : MergeAxis

def productMerge (P : PauliProduct) : SurgeryGadget

def fullSchedule (prog : PPMProg) : List SurgeryGadget

theorem fullSchedule_fully_correct (prog : PPMProg) :
    ScheduleFullyCorrect (fullSchedule prog)

theorem productMerge_fully_correct (P : PauliProduct) :
    MergeFullyCorrect (productMerge P)

def piEighthSel : PPMStmt

theorem piEighthSel_branches_verified :
    SurgeryGadget.verify_surgery_gadget (productMerge [⟨0, .y⟩]) = true
      ∧ SurgeryGadget.verify_surgery_gadget (productMerge [⟨0, .x⟩]) = true

theorem piEighthSel_branches_fully_correct :
    (∀ P ∈ stmtMeasurements piEighthSel, MergeFullyCorrect (productMerge P))

def cczSel2 : PPMStmt

theorem cczSel2_branches_verified :
    (stmtMeasurements cczSel2).all (fun P => SurgeryGadget.verify_surgery_gadget (productMerge P))
      = true

theorem cczSel2_branches_fully_correct :
    (∀ P ∈ stmtMeasurements cczSel2, MergeFullyCorrect (productMerge P))

def scheduleCircuit (sched : List SurgeryGadget) : PhysCircuit

def ScheduleFullyCorrect (sched : List SurgeryGadget) : Prop

theorem scheduleFullyCorrect_of (sched : List SurgeryGadget) :
    ScheduleFullyCorrect sched

theorem surface3_cnot_fully_correct : ScheduleFullyCorrect surface3_cnot

theorem cnot_zz_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS surface3_zz_merge).n
          + (mergedCSS surface3_zz_merge).hx.length
          + (mergedCSS surface3_zz_merge).hz.length)
        (mergedCSS surface3_zz_merge).n
        (SurgeryGadget.extractionRound surface3_zz_merge)
      = (mergedCSS surface3_zz_merge).toStabilizers

theorem cnot_zz_logical_correct (signs : List Bool)
    (hsig : signs.length = surface3_zz_merge.merged_hx.length) :
    selectedSignedProduct surface3_zz_merge.span_witness
        surface3_zz_merge.merged_hx signs
      = signedXRow (selectedParity surface3_zz_merge.span_witness signs)
          surface3_zz_merge.target_pauli

theorem cnot_xx_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS surface3_xx_merge).n
          + (mergedCSS surface3_xx_merge).hx.length
          + (mergedCSS surface3_xx_merge).hz.length)
        (mergedCSS surface3_xx_merge).n
        (SurgeryGadget.extractionRound surface3_xx_merge)
      = (mergedCSS surface3_xx_merge).toStabilizers

theorem cnot_xx_logical_correct (signs : List Bool)
    (hsig : signs.length = surface3_xx_merge.merged_hx.length) :
    selectedSignedProduct surface3_xx_merge.span_witness
        surface3_xx_merge.merged_hx signs
      = signedXRow (selectedParity surface3_xx_merge.span_witness signs)
          surface3_xx_merge.target_pauli

theorem surface3_ccx_fully_correct : ScheduleFullyCorrect surface3_ccx_injection

theorem ccx_zzz_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS surface3_zzz_merge).n
          + (mergedCSS surface3_zzz_merge).hx.length
          + (mergedCSS surface3_zzz_merge).hz.length)
        (mergedCSS surface3_zzz_merge).n
        (SurgeryGadget.extractionRound surface3_zzz_merge)
      = (mergedCSS surface3_zzz_merge).toStabilizers

theorem scheduleCircuit_measCount (sched : List SurgeryGadget) :
    measCountC (scheduleCircuit sched)
      = (sched.map surgeryTotalMeas).sum

theorem surface3_cnot_resource_on_verified :
    measCountC (scheduleCircuit surface3_cnot)
      = (surface3_cnot.map surgeryTotalMeas).sum

theorem surface3_cnot_measCount_value :
    FormalRV.Resource.measCountC (scheduleCircuit surface3_cnot) = 104

def basisFramePorts (layer : List PlacedGadget) : List (Nat × Pauli)

theorem basisFramePorts_zy :
    basisFramePorts [⟨GadgetKind.zMerge, [0, 1]⟩, ⟨GadgetKind.mY1, [2]⟩]
      = [(0, Pauli.Z), (1, Pauli.Z), (2, Pauli.Y)]

def bzyLaS : LaSre

def bzySurf : Surf

def bzyPorts : List Port

def bzyPaulis : Nat → Nat → Pauli

theorem bzy_correct :
    LaSCorrectFull bzyLaS bzySurf bzyPorts bzyPaulis 4 = true

def bzyPaulisAllZ : Nat → Nat → Pauli

theorem bzy_allZ_rejected :
    LaSCorrectFull bzyLaS bzySurf bzyPorts bzyPaulisAllZ 4 = false

theorem bzy_basis_is_the_discriminator :
    bzyPaulis 3 4 = Pauli.Y ∧ bzyPaulisAllZ 3 4 = Pauli.Z
      ∧ bzyPaulis 0 0 = bzyPaulisAllZ 0 0 ∧ bzyPaulis 1 0 = bzyPaulisAllZ 1 0

def bzxyLaS : LaSre

def bzxySurf : Surf

def bzxyPorts : List Port

def bzxyPaulis : Nat → Nat → Pauli

theorem bzxy_correct :
    LaSCorrectFull bzxyLaS bzxySurf bzxyPorts bzxyPaulis 5 = true

def bzxyPaulisAllZ : Nat → Nat → Pauli

theorem bzxy_allZ_rejected :
    LaSCorrectFull bzxyLaS bzxySurf bzxyPorts bzxyPaulisAllZ 5 = false

theorem basisFramePorts_zxy :
    basisFramePorts [⟨GadgetKind.zMerge, [0, 1]⟩, ⟨GadgetKind.mX1, [2]⟩, ⟨GadgetKind.mY1, [3]⟩]
      = [(0, Pauli.Z), (1, Pauli.Z), (2, Pauli.X), (3, Pauli.Y)]

def colorBasis (c : Bool) : Pauli

def seamColorOf (L : LaSre) : Option Bool

def gadgetColorFaithful (k : GadgetKind) : Bool

theorem zMerge_color_faithful  : gadgetColorFaithful .zMerge  = true

theorem xMerge_color_faithful  : gadgetColorFaithful .xMerge  = true

theorem mZ3_color_faithful     : gadgetColorFaithful .mZ3     = true

theorem mX3_color_faithful     : gadgetColorFaithful .mX3     = true

theorem mZ4_color_faithful     : gadgetColorFaithful .mZ4     = true

theorem mZ1_color_faithful     : gadgetColorFaithful .mZ1     = true

theorem mX1_color_faithful     : gadgetColorFaithful .mX1     = true

theorem mxzMerge_not_color_faithful : gadgetColorFaithful .mxzMerge = false

theorem mzxMerge_not_color_faithful : gadgetColorFaithful .mzxMerge = false

theorem mxzz3_not_color_faithful    : gadgetColorFaithful .mxzz3    = false

theorem mY1_not_color_faithful      : gadgetColorFaithful .mY1      = false

theorem color_check_strictly_stronger :
    ScheduleImplementsSpec (gadgetFor .mxzMerge) = true
      ∧ gadgetColorFaithful .mxzMerge = false

theorem promotion_blocks_faithful :
    gadgetColorFaithful .xMerge = true        -- M_{X₁X₂} for the H-conjugation
      ∧ gadgetColorFaithful .mZ1 = true       -- the X-readout's basis sibling
      ∧ gadgetColorFaithful .mX1 = true

def progColorFaithful (prog : FormalRV.PPM.Prog.PPMProg) : Bool

def colorFaithfulCount (prog : FormalRV.PPM.Prog.PPMProg) : Nat × Nat

def isFaithfulGate : GadgetKind → Bool
  | .hgate | .sgate | .cnot | .cz | .ccz | .mem => true
  | _ => false

def gadgetIsPhysical (k : GadgetKind) : Bool

def conjH : Pauli → Pauli | .Z => .X | .X => .Z | .Y => .Y | .I => .I

def conjS : Pauli → Pauli | .X => .Y | .Y => .X | .Z => .Z | .I => .I

def conjAt (i : Nat) (f : Pauli → Pauli) : List Pauli → List Pauli
  | []      => []
  | p :: ps => if i = 0 then f p :: ps else p :: conjAt (i - 1) f ps

def faithfulDecomp : GadgetKind → List GadgetKind
  | .mxzMerge => [.hgate, .zMerge, .hgate]
  | .mzxMerge => [.hgate, .zMerge, .hgate]
  | .mxzz3    => [.hgate, .mZ3,   .hgate]
  | .mzxz3    => [.hgate, .mZ3,   .hgate]
  | .mzzx3    => [.hgate, .mZ3,   .hgate]
  | .mY1      => [.sgate, .mX1,   .sgate]
  | k         => [k]

theorem faithfulDecomp_all_physical (k : GadgetKind) :
    (faithfulDecomp k).all gadgetIsPhysical = true

theorem mxzMerge_promoted_realizes :
    conjAt 0 conjH (gadgetObservable .zMerge) = gadgetObservable .mxzMerge

theorem mzxMerge_promoted_realizes :
    conjAt 1 conjH (gadgetObservable .zMerge) = gadgetObservable .mzxMerge

theorem mxzz3_promoted_realizes :
    conjAt 0 conjH (gadgetObservable .mZ3) = gadgetObservable .mxzz3

theorem mY1_promoted_realizes :
    conjAt 0 conjS (gadgetObservable .mX1) = gadgetObservable .mY1

def progGadgetsFaithful (prog : FormalRV.PPM.Prog.PPMProg) : List GadgetKind

def progPhysical (prog : FormalRV.PPM.Prog.PPMProg) : Bool

theorem modexp_physically_faithful : progPhysical modexpPPM = true

theorem adder_physically_faithful  : progPhysical adderPPM  = true

def surface27 : CodeBlock

def gadgetBoard (g : Gate) : List CodeBlock

def compileToPhysical (board : List CodeBlock)
    (ppm : FormalRV.PPM.Prog.PPMProg) : PhysCircuit

def gadgetPPM (g : Gate) : FormalRV.PPM.Prog.PPMProg

def gadgetPhysical (g : Gate) : PhysCircuit

def gadgetStim (g : Gate) : String

def kindToPauli : FormalRV.PPM.Prog.PKind → Pauli
  | .x => .X | .z => .Z | .y => .Y

def productObservable (P : FormalRV.PPM.Prog.PauliProduct) : List Pauli

def productQubitObservable (P : FormalRV.PPM.Prog.PauliProduct) : List (Nat × Pauli)

def gadgetObservable (k : GadgetKind) : List Pauli

def measurementFaithful (prog : FormalRV.PPM.Prog.PPMProg) : Bool

def measurementFaithfulPlaced (prog : FormalRV.PPM.Prog.PPMProg) : Bool

theorem gadgetObservable_zMerge : gadgetObservable .zMerge = [.Z, .Z]

theorem gadgetObservable_mxzMerge : gadgetObservable .mxzMerge = [.X, .Z]

theorem gadgetObservable_mzxz3 : gadgetObservable .mzxz3 = [.Z, .X, .Z]

theorem gadgetObservable_mY1 : gadgetObservable .mY1 = [.Y]

theorem shorCCZ_faithful : measurementFaithful shorCCZ = true

theorem adder_faithful : measurementFaithful adderPPM = true

theorem modmult_faithful : measurementFaithful modmultPPM = true

theorem modexp_faithful : measurementFaithful modexpPPM = true

theorem shorCCZ_faithful_placed : measurementFaithfulPlaced shorCCZ = true

theorem adder_faithful_placed : measurementFaithfulPlaced adderPPM = true

theorem modexp_faithful_placed : measurementFaithfulPlaced modexpPPM = true

theorem modexp_composed_realized :
    (∀ k ∈ progGadgets modexpPPM, ScheduleImplementsSpec (gadgetFor k) = true)
    ∧ uncoveredMeasurements modexpPPM = []
    ∧ measurementFaithfulPlaced modexpPPM = true

theorem adder_composed_realized :
    (∀ k ∈ progGadgets adderPPM, ScheduleImplementsSpec (gadgetFor k) = true)
    ∧ uncoveredMeasurements adderPPM = []
    ∧ measurementFaithfulPlaced adderPPM = true

theorem patch_extraction_correct :
    Round.measuredDataObs
        ((Codes.Surface.rotatedSurface 27).n
          + (Codes.Surface.rotatedSurface 27).hx.length
          + (Codes.Surface.rotatedSurface 27).hz.length)
        (Codes.Surface.rotatedSurface 27).n
        (CSSCode.extractionRound surface27.code)
      = surface27.code.toStabilizers

def GadgetCompiledOK (g : Gate) : Prop

theorem gadgetCompiledOK_of (g : Gate) (hppm : LoweredOK g) :
    GadgetCompiledOK g

def cuccaroadderGate : FormalRV.Framework.Gate

theorem cuccaroadder_compiled : GadgetCompiledOK cuccaroadderGate

theorem cuccaroadder_measCount :
    measCountC (gadgetPhysical cuccaroadderGate)
      = physicalStmtCount (gadgetPPM cuccaroadderGate)
          * (27 * (Resource.width cuccaroadderGate * 728))

theorem cuccaroadder_qubits :
    boardPhysQubits (gadgetBoard cuccaroadderGate)
      = Resource.width cuccaroadderGate * 1457

def majPPM : FormalRV.PPM.Prog.PPMProg

theorem majPPM_fully_covered : uncoveredMeasurements majPPM = []

theorem majPPM_routes_to_verified :
    (∀ k ∈ progGadgets majPPM, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements majPPM = []

def adderPPM : FormalRV.PPM.Prog.PPMProg

theorem adderPPM_fully_covered : uncoveredMeasurements adderPPM = []

theorem adderPPM_routes_to_verified :
    (∀ k ∈ progGadgets adderPPM, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements adderPPM = []

structure VerifiedQECProgram

def compileToQEC (prog : PPMProg) : VerifiedQECProgram

def VerifiedQECProgram.circuit (v : VerifiedQECProgram) : PhysCircuit

theorem compileToQEC_correct (prog : PPMProg) :
    ScheduleFullyCorrect (compileToQEC prog).schedule

def VerifiedQECProgram.numMerges (v : VerifiedQECProgram) : Nat

def VerifiedQECProgram.measurements (v : VerifiedQECProgram) : Nat

def VerifiedQECProgram.gates (v : VerifiedQECProgram) : Nat

def VerifiedQECProgram.dataQubits (v : VerifiedQECProgram) : Nat

def VerifiedQECProgram.syndromeQubits (v : VerifiedQECProgram) : Nat

theorem VerifiedQECProgram.measurements_eq (v : VerifiedQECProgram) :
    v.measurements = v.syndromeQubits

theorem compileToQEC_measurements (prog : PPMProg) :
    (compileToQEC prog).measurements
      = ((fullSchedule prog).map surgeryTotalMeas).sum

structure QECResourceReport

def VerifiedQECProgram.report (v : VerifiedQECProgram) : QECResourceReport

def demoProgram : PPMProg

theorem demoProgram_compiled_correct :
    ScheduleFullyCorrect (compileToQEC demoProgram).schedule

def foldLaSList (prog : PPMProg) : List LaSre

def foldSurfList (prog : PPMProg) : List Surf

def foldPPMProgLaS (h : Nat) (conn : List (Nat × Nat)) (prog : PPMProg) : LaSre

theorem foldPPMProg_LaSCorrectFull
    (h n : Nat) (conn : List (Nat × Nat)) (w wj : Nat) (prog : PPMProg)
    (ss : List Surf) (ports : List Port) (paulis : Nat → Nat → Pauli)
    (hc : chainOK h n conn w wj (foldLaSList prog) ss = true)
    (hPorts : portsOK (weldChainSurf h ss) ports paulis n = true) :
    LaSCorrectFull (foldPPMProgLaS h conn prog) (weldChainSurf h ss) ports paulis n = true

def demoZZProg : PPMProg

theorem demoZZ_gadgets : progGadgets demoZZProg = [GadgetKind.mZ1, GadgetKind.mZ1]

theorem demoZZ_diagrams : foldLaSList demoZZProg = [memoryLaS, memoryLaS]

def demoZZSurfs : List Surf

def demoZZPorts : List Port

def demoZZPaulis : Nat → Nat → Pauli

theorem demoZZ_chainOK :
    chainOK 3 1 [(0, 0)] 1 1 (foldLaSList demoZZProg) demoZZSurfs = true

theorem demoZZ_ports :
    portsOK (weldChainSurf 3 demoZZSurfs) demoZZPorts demoZZPaulis 1 = true

theorem demoZZ_correct :
    LaSCorrectFull (foldPPMProgLaS 3 [(0, 0)] demoZZProg)
      (weldChainSurf 3 demoZZSurfs) demoZZPorts demoZZPaulis 1 = true

theorem mergeZLaS_eq : mergeZLaS = zMerge 2

theorem mergeZSurf_eq : mergeZSurf = zMergeSurf 2

theorem measConn_eq : measConn = zChainConn 2

def zMeasStmt (dst : Nat) : PPMStmt

def zMeasProg (N : Nat) : PPMProg

theorem stmtGadgets_zMeas (d : Nat) : stmtGadgets (zMeasStmt d) = [GadgetKind.zMerge]

theorem progGadgets_zMeas_list (l : List Nat) :
    progGadgets (l.map zMeasStmt) = List.replicate l.length GadgetKind.zMerge

theorem zMeasProg_gadgets (N : Nat) :
    progGadgets (zMeasProg N) = List.replicate N GadgetKind.zMerge

theorem foldLaSList_zMeas (N : Nat) :
    foldLaSList (zMeasProg N) = List.replicate N (zMerge 2)

theorem foldSurfList_zMeas (N : Nat) :
    foldSurfList (zMeasProg N) = List.replicate N (zMergeSurf 2)

theorem kindChain_g_replicate (N : Nat) :
    ((List.replicate N true).map (kindEntry 2)).map (·.g) = List.replicate N (zMerge 2)

theorem kindChain_sg_replicate (N : Nat) :
    ((List.replicate N true).map (kindEntry 2)).map (·.sg) = List.replicate N (zMergeSurf 2)

theorem foldPPMProg_zMeas_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N))
      (weldChainSurf 3 (foldSurfList (zMeasProg N)))
      (heteroStackPorts 2 (List.replicate N true)) (zMergePaulis 2) 3 = true

def mxzMeasStmt (dst : Nat) : PPMStmt

def mxzMeasProg (N : Nat) : PPMProg

theorem stmtGadgets_mxz (d : Nat) : stmtGadgets (mxzMeasStmt d) = [GadgetKind.mxzMerge]

theorem progGadgets_mxz_list (l : List Nat) :
    progGadgets (l.map mxzMeasStmt) = List.replicate l.length GadgetKind.mxzMerge

theorem mxzMeasProg_gadgets (N : Nat) :
    progGadgets (mxzMeasProg N) = List.replicate N GadgetKind.mxzMerge

theorem foldLaSList_mxz (N : Nat) :
    foldLaSList (mxzMeasProg N) = List.replicate N (zMerge 2)

theorem foldSurfList_mxz (N : Nat) :
    foldSurfList (mxzMeasProg N) = List.replicate N (zMergeSurf 2)

theorem replicate_chainOK (N : Nat) (hN : 0 < N) :
    chainOK 3 3 (zChainConn 2) 2 1
      (List.replicate N (zMerge 2)) (List.replicate N (zMergeSurf 2)) = true

def mxzStackPorts (N : Nat) : List Port

theorem mxzStack_portsOK (N : Nat) (hN : 0 < N) :
    portsOK (weldChainSurf 3 (List.replicate N (zMergeSurf 2)))
      (mxzStackPorts N) mxzPaulis 3 = true

theorem foldPPMProg_mxz_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 2) (mxzMeasProg N))
      (weldChainSurf 3 (foldSurfList (mxzMeasProg N)))
      (mxzStackPorts N) mxzPaulis 3 = true

theorem progGadgets_map_const {k : GadgetKind} {f : Nat → PPMStmt}
    (hf : ∀ d, stmtGadgets (f d) = [k]) (l : List Nat) :
    progGadgets (l.map f) = List.replicate l.length k

theorem mergeXLaS_eq : mergeXLaS = xMerge 2

theorem mergeXSurf_eq : mergeXSurf = xMergeSurf 2

def xMeasStmt (dst : Nat) : PPMStmt

def xMeasProg (M : Nat) : PPMProg

theorem stmtGadgets_xMeas (d : Nat) : stmtGadgets (xMeasStmt d) = [GadgetKind.xMerge]

theorem xMeasProg_gadgets (M : Nat) :
    progGadgets (xMeasProg M) = List.replicate M GadgetKind.xMerge

theorem foldLaSList_xMerge (M : Nat) :
    foldLaSList (xMeasProg M) = List.replicate M (xMerge 2)

theorem foldSurfList_xMerge (M : Nat) :
    foldSurfList (xMeasProg M) = List.replicate M (xMergeSurf 2)

theorem foldPPMProg_xMerge_scales (N : Nat) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (xConn 2) (xMeasProg (N + 1)))
      (weldChainSurf 3 (foldSurfList (xMeasProg (N + 1))))
      (xStackPorts 2 N) (xMergePaulis 2) 3 = true

def mzxMeasStmt (dst : Nat) : PPMStmt

def mzxMeasProg (M : Nat) : PPMProg

theorem stmtGadgets_mzx (d : Nat) : stmtGadgets (mzxMeasStmt d) = [GadgetKind.mzxMerge]

theorem mzxMeasProg_gadgets (M : Nat) :
    progGadgets (mzxMeasProg M) = List.replicate M GadgetKind.mzxMerge

theorem foldLaSList_mzx (M : Nat) :
    foldLaSList (mzxMeasProg M) = List.replicate M (zMerge 2)

theorem foldSurfList_mzx (M : Nat) :
    foldSurfList (mzxMeasProg M) = List.replicate M (zMergeSurf 2)

def mzxStackPorts (N : Nat) : List Port

theorem mzxStack_portsOK (N : Nat) (hN : 0 < N) :
    portsOK (weldChainSurf 3 (List.replicate N (zMergeSurf 2)))
      (mzxStackPorts N) mzxPaulis 3 = true

theorem foldPPMProg_mzx_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 2) (mzxMeasProg N))
      (weldChainSurf 3 (foldSurfList (mzxMeasProg N)))
      (mzxStackPorts N) mzxPaulis 3 = true

theorem rep_chainOK (g : LaSre) (s : Surf) (n w wj : Nat) (conn : List (Nat × Nat))
    (hi : g.maxI = w) (hj : g.maxJ = wj) (hk : g.maxK = 3)
    (hv : g.valid = true) (hf : g.funcOK s n = true)
    (rfv : weldInterfaceValidOK2 3 g g conn w wj = true)
    (rff : weldInterfaceOK2 3 g g s s conn n w wj = true)
    (hbL : BotEqL g g) (hbS : BotEqS s s) :
    ∀ N, 0 < N → chainOK 3 n conn w wj (List.replicate N g) (List.replicate N s) = true

theorem mY1_funcOK : memoryLaS.funcOK mY1Surf 1 = true

theorem yRead_refValid : weldInterfaceValidOK2 3 memoryLaS memoryLaS [(0, 0)] 1 1 = true

theorem yRead_refFunc :
    weldInterfaceOK2 3 memoryLaS memoryLaS mY1Surf mY1Surf [(0, 0)] 1 1 1 = true

def botEqL_mem : BotEqL memoryLaS memoryLaS

def botEqS_mY1 : BotEqS mY1Surf mY1Surf

theorem yReadout_chainOK (N : Nat) (hN : 0 < N) :
    chainOK 3 1 [(0, 0)] 1 1 (List.replicate N memoryLaS) (List.replicate N mY1Surf) = true

def yMeasStmt (dst : Nat) : PPMStmt

def yMeasProg (M : Nat) : PPMProg

theorem stmtGadgets_yMeas (d : Nat) : stmtGadgets (yMeasStmt d) = [GadgetKind.mY1]

theorem yMeasProg_gadgets (M : Nat) :
    progGadgets (yMeasProg M) = List.replicate M GadgetKind.mY1

theorem foldLaSList_yMeas (M : Nat) :
    foldLaSList (yMeasProg M) = List.replicate M memoryLaS

theorem foldSurfList_yMeas (M : Nat) :
    foldSurfList (yMeasProg M) = List.replicate M mY1Surf

def yStackPorts (N : Nat) : List Port

theorem yReadout_portsOK (N : Nat) (hN : 0 < N) :
    portsOK (weldChainSurf 3 (List.replicate N mY1Surf)) (yStackPorts N) mY1Paulis 1 = true

theorem foldPPMProg_yMeas_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 [(0, 0)] (yMeasProg N))
      (weldChainSurf 3 (foldSurfList (yMeasProg N)))
      (yStackPorts N) mY1Paulis 1 = true

theorem kindChain_g_repl (w N : Nat) :
    ((List.replicate N true).map (kindEntry w)).map (·.g) = List.replicate N (zMerge w)

theorem kindChain_sg_repl (w N : Nat) :
    ((List.replicate N true).map (kindEntry w)).map (·.sg) = List.replicate N (zMergeSurf w)

theorem replicate_chainOK_w (w N : Nat) (hN : 0 < N) :
    chainOK 3 (w + 1) (zChainConn w) w 1
      (List.replicate N (zMerge w)) (List.replicate N (zMergeSurf w)) = true

theorem mergeZ3LaS_eq : mergeZ3LaS = zMerge 3

theorem mergeZ3Surf_eq : mergeZ3Surf = zMergeSurf 3

def z3MeasStmt (dst : Nat) : PPMStmt

def z3MeasProg (M : Nat) : PPMProg

theorem stmtGadgets_z3 (d : Nat) : stmtGadgets (z3MeasStmt d) = [GadgetKind.mZ3]

theorem z3MeasProg_gadgets (M : Nat) :
    progGadgets (z3MeasProg M) = List.replicate M GadgetKind.mZ3

theorem foldLaSList_z3 (M : Nat) :
    foldLaSList (z3MeasProg M) = List.replicate M (zMerge 3)

theorem foldSurfList_z3 (M : Nat) :
    foldSurfList (z3MeasProg M) = List.replicate M (zMergeSurf 3)

theorem foldPPMProg_z3Meas_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 3) (z3MeasProg N))
      (weldChainSurf 3 (foldSurfList (z3MeasProg N)))
      (heteroStackPorts 3 (List.replicate N true)) (zMergePaulis 3) 4 = true

def mxzz3MeasStmt (dst : Nat) : PPMStmt

def mxzz3MeasProg (M : Nat) : PPMProg

theorem stmtGadgets_mxzz3 (d : Nat) : stmtGadgets (mxzz3MeasStmt d) = [GadgetKind.mxzz3]

theorem mxzz3MeasProg_gadgets (M : Nat) :
    progGadgets (mxzz3MeasProg M) = List.replicate M GadgetKind.mxzz3

theorem foldLaSList_mxzz3 (M : Nat) :
    foldLaSList (mxzz3MeasProg M) = List.replicate M (zMerge 3)

theorem foldSurfList_mxzz3 (M : Nat) :
    foldSurfList (mxzz3MeasProg M) = List.replicate M (zMergeSurf 3)

def mxzz3StackPorts (N : Nat) : List Port

theorem mxzz3Stack_portsOK (N : Nat) (hN : 0 < N) :
    portsOK (weldChainSurf 3 (List.replicate N (zMergeSurf 3)))
      (mxzz3StackPorts N) mxzz3Paulis 4 = true

theorem foldPPMProg_mxzz3_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 3) (mxzz3MeasProg N))
      (weldChainSurf 3 (foldSurfList (mxzz3MeasProg N)))
      (mxzz3StackPorts N) mxzz3Paulis 4 = true

def foldTimedLaS (t : List Bool) : LaSre

def foldTimedSurf (t : List Bool) : Surf

theorem foldTimed_LaSCorrectFull (t : List Bool) (ht : t ≠ []) :
    LaSCorrectFull (foldTimedLaS t) (foldTimedSurf t)
      (heteroStackPorts 2 t) (zMergePaulis 2) 3 = true

theorem foldTimed_allMerge_eq_zMeas (N : Nat) :
    foldTimedLaS (List.replicate N true) = foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)

def demoSched : List Bool

theorem demoSched_genuinely_mixed :
    demoSched.count true = 3 ∧ demoSched.count false = 2

theorem demoSched_correct :
    LaSCorrectFull (foldTimedLaS demoSched) (foldTimedSurf demoSched)
      (heteroStackPorts 2 demoSched) (zMergePaulis 2) 3 = true

theorem demoSched_has_merge_layer : (foldTimedLaS demoSched).ExistI 0 0 1 = true

theorem demoSched_has_idle_layer : (foldTimedLaS demoSched).ExistI 0 0 4 = false

def gadgetLogicalSchedule (g : Gate) : List SurgeryGadget

theorem gadgetLogicalSchedule_length (g : Gate) :
    (gadgetLogicalSchedule g).length = gadgetMergeCount g

theorem gadgetLogicalSchedule_fully_correct (g : Gate) :
    ScheduleFullyCorrect (gadgetLogicalSchedule g)

theorem gadgetLogicalSchedule_each_logical (g : Gate)
    (mg : SurgeryGadget) (hmem : mg ∈ gadgetLogicalSchedule g)
    (signs : List Bool) (hsig : signs.length = mg.merged_hx.length) :
    selectedSignedProduct mg.span_witness mg.merged_hx signs
      = signedXRow (selectedParity mg.span_witness signs) mg.target_pauli

theorem gadgetLogicalSchedule_measCount (g : Gate) :
    measCountC (scheduleCircuit (gadgetLogicalSchedule g))
      = gadgetMergeCount g
          * FormalRV.LatticeSurgery.SurfaceShorResourceCount.surgeryTotalMeas
              (rotatedXMerge 27 18 40)

inductive MergeAxis

def classifyAxis (P : PauliProduct) : Option MergeAxis

def axisMerge : MergeAxis → SurgeryGadget
  | MergeAxis.xAxis => rotatedXMerge 27 18 40
  | MergeAxis.zAxis => rotatedZMerge 27 18 40

theorem axisMerge_fully_correct (a : MergeAxis) : MergeFullyCorrect (axisMerge a)

def axisSchedule (axes : List MergeAxis) : List SurgeryGadget

theorem axisSchedule_fully_correct (axes : List MergeAxis) :
    ScheduleFullyCorrect (axisSchedule axes)

def programAxes : PPMProg → List MergeAxis
  | [] => []
  | st :: rest =>
      (match st with
        | .measure _ P => (classifyAxis P).toList
        | _ => [])
      ++ programAxes rest

def programSchedule (prog : PPMProg) : List SurgeryGadget

theorem programSchedule_fully_correct (prog : PPMProg) :
    ScheduleFullyCorrect (programSchedule prog)

example : classifyAxis [⟨0, .x⟩, ⟨1, .x⟩] = some MergeAxis.xAxis

example : classifyAxis [⟨0, .z⟩, ⟨2, .z⟩] = some MergeAxis.zAxis

example : classifyAxis [⟨0, .x⟩, ⟨1, .z⟩] = none

example : classifyAxis [⟨0, .y⟩] = none

def memSurf : Surf

def memPorts : List Port

def memPaulis : Nat → Nat → Pauli

theorem memory_fully_correct :
    LaSCorrectFull memoryLaS memSurf memPorts memPaulis 2 = true

def memScheduleLaS : ScheduleLaS

theorem memory_implements_spec : ScheduleImplementsSpec memScheduleLaS = true

def memSurf_swapped : Surf

theorem memory_swapped_rejected :
    LaSCorrectFull memoryLaS memSurf_swapped memPorts memPaulis 2 = false

def mergeZLaS : LaSre

def mergeZSurf : Surf

def mergeZPorts : List Port

def mergeZPaulis : Nat → Nat → Pauli

theorem mergeZ_fully_correct :
    LaSCorrectFull mergeZLaS mergeZSurf mergeZPorts mergeZPaulis 3 = true

def mergeZScheduleLaS : ScheduleLaS

theorem mergeZ_implements_spec : ScheduleImplementsSpec mergeZScheduleLaS = true

def mergeZSurf_unjoined : Surf

theorem mergeZ_unjoined_rejected :
    LaSCorrectFull mergeZLaS mergeZSurf_unjoined mergeZPorts mergeZPaulis 3 = false

def mergeXLaS : LaSre

def mergeXSurf : Surf

def mergeXPorts : List Port

def mergeXPaulis : Nat → Nat → Pauli

theorem mergeX_fully_correct :
    LaSCorrectFull mergeXLaS mergeXSurf mergeXPorts mergeXPaulis 3 = true

def mergeXScheduleLaS : ScheduleLaS

theorem mergeX_implements_spec : ScheduleImplementsSpec mergeXScheduleLaS = true

def mergeXSurf_unjoined : Surf

theorem mergeX_unjoined_rejected :
    LaSCorrectFull mergeXLaS mergeXSurf_unjoined mergeXPorts mergeXPaulis 3 = false

def mxzPorts : List Port

def mxzPaulis : Nat → Nat → Pauli

theorem mxzMerge_fully_correct :
    LaSCorrectFull mergeZLaS mergeZSurf mxzPorts mxzPaulis 3 = true

def m1Ports : List Port

def mZ1Surf : Surf

def mZ1Paulis : Nat → Nat → Pauli

theorem mZ1_fully_correct :
    LaSCorrectFull memoryLaS mZ1Surf m1Ports mZ1Paulis 1 = true

def mX1Surf : Surf

def mX1Paulis : Nat → Nat → Pauli

theorem mX1_fully_correct :
    LaSCorrectFull memoryLaS mX1Surf m1Ports mX1Paulis 1 = true

def mergeZ3LaS : LaSre

def mergeZ3Surf : Surf

def mergeZ3Ports : List Port

def mergeZ3Paulis : Nat → Nat → Pauli

theorem mergeZ3_fully_correct :
    LaSCorrectFull mergeZ3LaS mergeZ3Surf mergeZ3Ports mergeZ3Paulis 4 = true

def mergeX3LaS : LaSre

def mergeX3Surf : Surf

def mergeX3Ports : List Port

def mergeX3Paulis : Nat → Nat → Pauli

theorem mergeX3_fully_correct :
    LaSCorrectFull mergeX3LaS mergeX3Surf mergeX3Ports mergeX3Paulis 4 = true

def mzxPorts : List Port

def mzxPaulis : Nat → Nat → Pauli

theorem mzxMerge_fully_correct :
    LaSCorrectFull mergeZLaS mergeZSurf mzxPorts mzxPaulis 3 = true

def mxzz3Ports : List Port

def mxzz3Paulis : Nat → Nat → Pauli

theorem mxzz3_fully_correct :
    LaSCorrectFull mergeZ3LaS mergeZ3Surf mxzz3Ports mxzz3Paulis 4 = true

def mzxz3Ports : List Port

def mzxz3Paulis : Nat → Nat → Pauli

theorem mzxz3_fully_correct :
    LaSCorrectFull mergeZ3LaS mergeZ3Surf mzxz3Ports mzxz3Paulis 4 = true

def mzzx3Ports : List Port

def mzzx3Paulis : Nat → Nat → Pauli

theorem mzzx3_fully_correct :
    LaSCorrectFull mergeZ3LaS mergeZ3Surf mzzx3Ports mzzx3Paulis 4 = true

def mY1Surf : Surf

def mY1Paulis : Nat → Nat → Pauli

theorem mY1_fully_correct :
    LaSCorrectFull memoryLaS mY1Surf m1Ports mY1Paulis 1 = true

def mergeZ4LaS : LaSre

def mergeZ4Surf : Surf

def mergeZ4Ports : List Port

def mergeZ4Paulis : Nat → Nat → Pauli

theorem mergeZ4_fully_correct :
    LaSCorrectFull mergeZ4LaS mergeZ4Surf mergeZ4Ports mergeZ4Paulis 5 = true

def cnotScheduleLaS : ScheduleLaS

def czScheduleLaS : ScheduleLaS

def hScheduleLaS : ScheduleLaS

def sScheduleLaS : ScheduleLaS

def mxzScheduleLaS : ScheduleLaS

def mZ1ScheduleLaS : ScheduleLaS

def mX1ScheduleLaS : ScheduleLaS

def mergeZ3ScheduleLaS : ScheduleLaS

def mergeX3ScheduleLaS : ScheduleLaS

def mzxScheduleLaS : ScheduleLaS

def mxzz3ScheduleLaS : ScheduleLaS

def mzxz3ScheduleLaS : ScheduleLaS

def mzzx3ScheduleLaS : ScheduleLaS

def mY1ScheduleLaS : ScheduleLaS

def mergeZ4ScheduleLaS : ScheduleLaS

inductive GadgetKind
  | mem      -- idle patch (identity)
  | mZ1      -- weight-1 M_Z (single-patch)
  | mX1      -- weight-1 M_X
  | mY1      -- weight-1 M_Y (flow-level, §3½ caveat)
  | mZ4      -- weight-4 M_{Z₁Z₂Z₃Z₄}
  | zMerge   -- joint Z̄₁Z̄₂ measurement
  | xMerge   -- joint X̄₁X̄₂ measurement
  | mxzMerge -- joint X̄₁Z̄₂ MIXED measurement (flow-level, §3½)
  | mzxMerge -- joint Z̄₁X̄₂ MIXED measurement (mirror)
  | mZ3      -- weight-3 M_{Z₁Z₂Z₃}
  | mX3      -- weight-3 M_{X₁X₂X₃}

def gadgetFor : GadgetKind → ScheduleLaS
  | .mem      => memScheduleLaS
  | .mZ1      => mZ1ScheduleLaS
  | .mX1      => mX1ScheduleLaS
  | .mY1      => mY1ScheduleLaS
  | .mZ4      => mergeZ4ScheduleLaS
  | .zMerge   => mergeZScheduleLaS
  | .xMerge   => mergeXScheduleLaS
  | .mxzMerge => mxzScheduleLaS
  | .mzxMerge => mzxScheduleLaS
  | .mZ3      => mergeZ3ScheduleLaS
  | .mX3      => mergeX3ScheduleLaS

theorem gadgetFor_implements_spec (k : GadgetKind) :
    ScheduleImplementsSpec (gadgetFor k) = true

theorem gadgetFor_realizes (k : GadgetKind) : RealizesSpecFlows (gadgetFor k)

def productGadgets (P : FormalRV.PPM.Prog.PauliProduct) :
    Option (List GadgetKind)

theorem productGadgets_each_verified
    (P : FormalRV.PPM.Prog.PauliProduct) (gs : List GadgetKind)
    (_h : productGadgets P = some gs) :
    ∀ k ∈ gs, ScheduleImplementsSpec (gadgetFor k) = true

def stmtGadgets (st : FormalRV.PPM.Prog.PPMStmt) : List GadgetKind

def progGadgets (prog : FormalRV.PPM.Prog.PPMProg) : List GadgetKind

theorem progGadgets_each_verified (prog : FormalRV.PPM.Prog.PPMProg) :
    ∀ k ∈ progGadgets prog, ScheduleImplementsSpec (gadgetFor k) = true

theorem progGadgets_each_realize (prog : FormalRV.PPM.Prog.PPMProg) :
    ∀ k ∈ progGadgets prog, RealizesSpecFlows (gadgetFor k)

theorem composition_machinery_verified : True

def productCovered (P : FormalRV.PPM.Prog.PauliProduct) : Bool

def uncoveredMeasurements (prog : FormalRV.PPM.Prog.PPMProg) : List FormalRV.PPM.Prog.PauliProduct

theorem fully_covered_program_routes_to_verified (prog : FormalRV.PPM.Prog.PPMProg)
    (hcov : uncoveredMeasurements prog = []) :
    (∀ k ∈ progGadgets prog, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements prog = []

def exampleProg : PPMProg

theorem exampleProg_gadgets :
    progGadgets exampleProg
      = [.zMerge, .xMerge, .mxzMerge, .mZ1, .mZ3]

theorem exampleProg_fully_covered :
    uncoveredMeasurements exampleProg = []

theorem exampleProg_routes_to_verified :
    (∀ k ∈ progGadgets exampleProg, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements exampleProg = []

def mergeZWeld : LaSre

def mergeZWeldSurf : Surf

def mergeZWeldPorts : List Port

def mergeZWeldPaulis : Nat → Nat → Pauli

theorem mergeZWeld_fully_correct :
    LaSCorrectFull mergeZWeld mergeZWeldSurf mergeZWeldPorts mergeZWeldPaulis 3 = true

def cnotWeld : LaSre

def cnotWeldSurf : Surf

def cnotWeldPorts : List Port

def cnotWeldPaulis : Nat → Nat → Pauli

theorem cnotWeld_is_identity :
    LaSCorrectFull cnotWeld cnotWeldSurf cnotWeldPorts cnotWeldPaulis 4 = true

structure PlacedGadget

def productPlaced (P : FormalRV.PPM.Prog.PauliProduct) : Option (List PlacedGadget)

theorem productPlaced_kinds (P : FormalRV.PPM.Prog.PauliProduct) :
    (productPlaced P).map (fun gs => gs.map (·.kind)) = productGadgets P

theorem productPlaced_verified
    (P : FormalRV.PPM.Prog.PauliProduct) (gs : List PlacedGadget)
    (_h : productPlaced P = some gs) :
    ∀ g ∈ gs, ScheduleImplementsSpec (gadgetFor g.kind) = true

def stmtPlaced (st : FormalRV.PPM.Prog.PPMStmt) : List PlacedGadget

def progPlaced (prog : FormalRV.PPM.Prog.PPMProg) : List PlacedGadget

theorem progPlaced_verified (prog : FormalRV.PPM.Prog.PPMProg) :
    ∀ g ∈ progPlaced prog, ScheduleImplementsSpec (gadgetFor g.kind) = true

def cssDualC (c : CSSCode) : CSSCode

def orientedCSS : MergeAxis → Nat → CSSCode
  | MergeAxis.xAxis, d => rotatedSurface d
  | MergeAxis.zAxis, d => cssDualC (rotatedSurface d)

def orientedSupp : MergeAxis → Nat → BoolVec
  | MergeAxis.xAxis, d => logicalX d
  | MergeAxis.zAxis, d => logicalZ d

def mixedComposite (axes : List MergeAxis) (d : Nat) : CSSCode

def mixedSupport (axes : List MergeAxis) (d : Nat) : BoolVec

def mixedMerge (axes : List MergeAxis) (d tau bound : Nat) : SurgeryGadget

def xzAxes : List MergeAxis

theorem mixedXZ3_verifies :
    SurgeryGadget.verify_surgery_gadget (mixedMerge xzAxes 3 2 30) = true

theorem mixedXZ3_fully_correct : MergeFullyCorrect (mixedMerge xzAxes 3 2 30)

theorem mixedXZ3_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS (mixedMerge xzAxes 3 2 30)).n
          + (mergedCSS (mixedMerge xzAxes 3 2 30)).hx.length
          + (mergedCSS (mixedMerge xzAxes 3 2 30)).hz.length)
        (mergedCSS (mixedMerge xzAxes 3 2 30)).n
        (SurgeryGadget.extractionRound (mixedMerge xzAxes 3 2 30))
      = (mergedCSS (mixedMerge xzAxes 3 2 30)).toStabilizers

theorem mixedXZ3_logical_correct (signs : List Bool)
    (hsig : signs.length = (mixedMerge xzAxes 3 2 30).merged_hx.length) :
    selectedSignedProduct (mixedMerge xzAxes 3 2 30).span_witness
        (mixedMerge xzAxes 3 2 30).merged_hx signs
      = signedXRow (selectedParity (mixedMerge xzAxes 3 2 30).span_witness signs)
          (mixedMerge xzAxes 3 2 30).target_pauli

theorem mixedXZ3_supports_genuine :
    isXLogical 3 (logicalX 3) = true ∧ isZLogical 3 (logicalZ 3) = true

theorem mixedXZ27_verifies :
    SurgeryGadget.verify_surgery_gadget (mixedMerge xzAxes 27 18 60) = true

theorem mixedXZ27_fully_correct : MergeFullyCorrect (mixedMerge xzAxes 27 18 60)

def modexpGate : FormalRV.Framework.Gate

theorem modexp_compiled : GadgetCompiledOK modexpGate

theorem modexp_measCount :
    measCountC (gadgetPhysical modexpGate)
      = physicalStmtCount (gadgetPPM modexpGate)
          * (27 * (Resource.width modexpGate * 728))

theorem modexp_qubits :
    boardPhysQubits (gadgetBoard modexpGate)
      = Resource.width modexpGate * 1457

def modmultGate : FormalRV.Framework.Gate

theorem modmult_compiled : GadgetCompiledOK modmultGate

theorem modmult_measCount :
    measCountC (gadgetPhysical modmultGate)
      = physicalStmtCount (gadgetPPM modmultGate)
          * (27 * (Resource.width modmultGate * 728))

theorem modmult_qubits :
    boardPhysQubits (gadgetBoard modmultGate)
      = Resource.width modmultGate * 1457

def modmultPPM : FormalRV.PPM.Prog.PPMProg

theorem modmultPPM_fully_covered : uncoveredMeasurements modmultPPM = []

theorem modmultPPM_routes_to_verified :
    (∀ k ∈ progGadgets modmultPPM, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements modmultPPM = []

def modexpPPM : FormalRV.PPM.Prog.PPMProg

theorem modexpPPM_fully_covered : uncoveredMeasurements modexpPPM = []

theorem modexpPPM_routes_to_verified :
    (∀ k ∈ progGadgets modexpPPM, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements modexpPPM = []

theorem qParity_singleton (outs : List Bool) (mon : List CVar) :
    qParity outs [mon] = andParity outs mon

theorem qParity_nil (outs : List Bool) : qParity outs [] = false

theorem qParity_append (outs : List Bool) (mons : List (List CVar))
    (mon : List CVar) :
    qParity outs (mons ++ [mon]) = (qParity outs mons ^^ andParity outs mon)

theorem andParity_singleton (outs : List Bool) (c : CVar) :
    andParity outs [c] = outs.getD c false

theorem qParity_singletons_eq_xorParity (outs : List Bool) (slots : List CVar) :
    qParity outs (slots.map (fun c => [c])) = xorParity outs slots

theorem qParity_ccz_residual (outs : List Bool) (i j k : CVar) :
    qParity outs [[i], [j, k]]
      = (outs.getD i false ^^ (outs.getD j false && outs.getD k false))

theorem and_not_xor_affine :
    ¬ ∃ a b c : Bool, ∀ m n : Bool,
        (m && n) = (a ^^ (b && m) ^^ (c && n))

theorem affine_fails_on_and :
    ∀ a b c : Bool, ∃ m n : Bool, (m && n) ≠ (a ^^ (b && m) ^^ (c && n))

def qFrameCorrection (outs : List Bool) (mons : List (List CVar))
    (thn els : PauliProduct) : PauliProduct

theorem correctQ_step_uses_decoder (n : Nat) (outcome : Bool) (st : ExecState)
    (mons : List (List CVar)) (thn els : PauliProduct) :
    (stepStmt n outcome st (.correctQ mons thn els)).frame
      = mulF st.frame (qFrameCorrection st.outs mons thn els)

theorem surface27_patchPhysQubits : patchPhysQubits surface27 = 1457

theorem gadget_qubits (g : Gate) :
    boardPhysQubits (gadgetBoard g) = Resource.width g * 1457

private theorem board_check_sum (g : Gate) :
    ((gadgetBoard g).map (fun b => b.code.hx.length
        + b.code.hz.length)).sum = Resource.width g * 728

theorem gadget_measCount (g : Gate) :
    measCountC (gadgetPhysical g)
      = physicalStmtCount (gadgetPPM g) * (27 * (Resource.width g * 728))

def measPatches (P : PauliProduct) : Nat

def measDataQubits (P : PauliProduct) : Nat

def measSyndrome (P : PauliProduct) : Nat

def progDataQubits (prog : FormalRV.PPM.Prog.PPMProg) : Nat

def progSyndrome (prog : FormalRV.PPM.Prog.PPMProg) : Nat

def progMerges (prog : FormalRV.PPM.Prog.PPMProg) : Nat

def measSplit (P : PauliProduct) : Nat

def progSplit (prog : FormalRV.PPM.Prog.PPMProg) : Nat

def progSyndromeTotal (prog : FormalRV.PPM.Prog.PPMProg) : Nat

theorem cuccaro_qec_correct :
    ScheduleFullyCorrect (compileToQEC (gadgetPPM cuccaroadderGate)).schedule

theorem modmult_qec_correct :
    ScheduleFullyCorrect (compileToQEC (gadgetPPM modmultGate)).schedule

theorem modexp_qec_correct :
    ScheduleFullyCorrect (compileToQEC (gadgetPPM modexpGate)).schedule

theorem windowed_qec_correct :
    ScheduleFullyCorrect (compileToQEC (gadgetPPM windowedGate)).schedule

def verifiedPatchFootprint : Nat

def paperPatchFootprint : Nat

theorem perPatch_gap :
    paperPatchFootprint - verifiedPatchFootprint = 111

theorem verifiedPatchFootprint_val : verifiedPatchFootprint = 1457

theorem paperPatchFootprint_val : paperPatchFootprint = 1568

def rotatedXMerge (d tau bound : Nat) : SurgeryGadget

theorem rotatedXMerge3_verifies :
    SurgeryGadget.verify_surgery_gadget (rotatedXMerge 3 2 12) = true

theorem rotatedXMerge3_fully_correct : MergeFullyCorrect (rotatedXMerge 3 2 12)

theorem rotatedXMerge3_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS (rotatedXMerge 3 2 12)).n
          + (mergedCSS (rotatedXMerge 3 2 12)).hx.length
          + (mergedCSS (rotatedXMerge 3 2 12)).hz.length)
        (mergedCSS (rotatedXMerge 3 2 12)).n
        (SurgeryGadget.extractionRound (rotatedXMerge 3 2 12))
      = (mergedCSS (rotatedXMerge 3 2 12)).toStabilizers

theorem rotatedXMerge3_logical_correct (signs : List Bool)
    (hsig : signs.length = (rotatedXMerge 3 2 12).merged_hx.length) :
    selectedSignedProduct (rotatedXMerge 3 2 12).span_witness
        (rotatedXMerge 3 2 12).merged_hx signs
      = signedXRow (selectedParity (rotatedXMerge 3 2 12).span_witness signs)
          (rotatedXMerge 3 2 12).target_pauli

theorem rotatedXMerge27_verifies :
    SurgeryGadget.verify_surgery_gadget (rotatedXMerge 27 18 40) = true

theorem rotatedXMerge27_fully_correct : MergeFullyCorrect (rotatedXMerge 27 18 40)

theorem rotatedXMerge27_target_is_genuine_logical :
    isXLogical 27 (logicalX 27) = true

theorem rotatedXMerge27_rounds : (rotatedXMerge 27 18 40).tau_s = 18

def rotatedZMerge (d tau bound : Nat) : SurgeryGadget

theorem rotatedZMerge3_verifies :
    SurgeryGadget.verify_surgery_gadget (rotatedZMerge 3 2 12) = true

theorem rotatedZMerge3_fully_correct : MergeFullyCorrect (rotatedZMerge 3 2 12)

theorem rotatedZMerge3_logical_correct (signs : List Bool)
    (hsig : signs.length = (rotatedZMerge 3 2 12).merged_hx.length) :
    selectedSignedProduct (rotatedZMerge 3 2 12).span_witness
        (rotatedZMerge 3 2 12).merged_hx signs
      = signedXRow (selectedParity (rotatedZMerge 3 2 12).span_witness signs)
          (rotatedZMerge 3 2 12).target_pauli

theorem rotatedZMerge27_verifies :
    SurgeryGadget.verify_surgery_gadget (rotatedZMerge 27 18 40) = true

theorem rotatedZMerge27_fully_correct : MergeFullyCorrect (rotatedZMerge 27 18 40)

theorem rotatedZMerge27_target_is_genuine_logical :
    isZLogical 27 (logicalZ 27) = true

structure ScheduleLaS

def ScheduleImplementsSpec (sl : ScheduleLaS) : Bool

def RealizesSpecFlows (sl : ScheduleLaS) : Prop

theorem implements_sound (sl : ScheduleLaS)
    (h : ScheduleImplementsSpec sl = true) : RealizesSpecFlows sl

theorem delPipe_locally_valid : majorityLaS_delPipe.valid = true

theorem delPipe_globally_wrong :
    majorityLaS_delPipe.funcOK majoritySurf 9 = false

theorem local_does_not_imply_global :
    ∃ (L : LaSre) (S : Surf) (n : Nat),
      L.valid = true ∧ L.funcOK S n = false

theorem perMerge_check_vacuous (prog : PPMProg) :
    ScheduleFullyCorrect (fullSchedule prog)

def cczScheduleLaS : ScheduleLaS

theorem ccz_implements_spec : ScheduleImplementsSpec cczScheduleLaS = true

theorem ccz_realizes_flows : RealizesSpecFlows cczScheduleLaS

def cczScheduleLaS_delPipe : ScheduleLaS

def cczScheduleLaS_badPort : ScheduleLaS

theorem delPipe_obligation_fails :
    ScheduleImplementsSpec cczScheduleLaS_delPipe = false

theorem badPort_obligation_fails :
    ScheduleImplementsSpec cczScheduleLaS_badPort = false

theorem obligation_discriminates :
    ScheduleImplementsSpec cczScheduleLaS = true
      ∧ ScheduleImplementsSpec cczScheduleLaS_delPipe = false
      ∧ ScheduleImplementsSpec cczScheduleLaS_badPort = false

def scheduleReport (sl : ScheduleLaS) : List Viol

theorem ccz_report_empty : scheduleReport cczScheduleLaS = []

def ScheduleImplementsPPM (prog : PPMProg) (sl : ScheduleLaS) : Prop

def cczProg : PPMProg

theorem ccz_completely_implemented :
    ScheduleImplementsPPM cczProg cczScheduleLaS

theorem perMerge_alone_insufficient :
    ScheduleFullyCorrect (fullSchedule cczProg)
      ∧ ScheduleImplementsSpec cczScheduleLaS_delPipe = false

def shorCCZ : FormalRV.PPM.Prog.PPMProg

theorem shorCCZ_gadgets :
    progGadgets shorCCZ =
      [.zMerge, .zMerge, .zMerge,
       .mX1, .mxzMerge, .mxzMerge, .mxzz3,
       .mX1, .mxzMerge, .mzxMerge, .mzxz3,
       .mX1, .mzxMerge, .mzxMerge, .mzzx3]

theorem shorCCZ_fully_covered : uncoveredMeasurements shorCCZ = []

theorem shorCCZ_routes_to_verified :
    (∀ k ∈ progGadgets shorCCZ, ScheduleImplementsSpec (gadgetFor k) = true)
      ∧ uncoveredMeasurements shorCCZ = []

def detachCircuit (g : SurgeryGadget) : PhysCircuit

theorem detachCircuit_measCount (g : SurgeryGadget) :
    measCountC (detachCircuit g) = g.ancilla_n

def postSplitCSS (g : SurgeryGadget) : CSSCode

theorem split_restores_patches (g : SurgeryGadget)
    (hws : (postSplitCSS g).well_shaped = true) :
    Round.measuredDataObs
        ((postSplitCSS g).n + (postSplitCSS g).hx.length + (postSplitCSS g).hz.length)
        (postSplitCSS g).n
        (CSSCode.extractionRound (postSplitCSS g))
      = (postSplitCSS g).toStabilizers

def splitCircuit (g : SurgeryGadget) (rounds : Nat) : PhysCircuit

theorem splitCircuit_measCount (g : SurgeryGadget) (rounds : Nat) :
    measCountC (splitCircuit g rounds)
      = g.ancilla_n
        + rounds * ((postSplitCSS g).hx.length + (postSplitCSS g).hz.length)

def SplitFullyCorrect (g : SurgeryGadget) : Prop

theorem splitFullyCorrect_of (g : SurgeryGadget) : SplitFullyCorrect g

theorem rotatedXMerge27_detach_count :
    measCountC (detachCircuit (rotatedXMerge 27 18 40)) = 1

theorem rotatedXMerge27_split_correct : SplitFullyCorrect (rotatedXMerge 27 18 40)

theorem rotatedXMerge27_split_restores :
    Round.measuredDataObs
        ((postSplitCSS (rotatedXMerge 27 18 40)).n
          + (postSplitCSS (rotatedXMerge 27 18 40)).hx.length
          + (postSplitCSS (rotatedXMerge 27 18 40)).hz.length)
        (postSplitCSS (rotatedXMerge 27 18 40)).n
        (CSSCode.extractionRound (postSplitCSS (rotatedXMerge 27 18 40)))
      = (postSplitCSS (rotatedXMerge 27 18 40)).toStabilizers

def detachObservables (g : SurgeryGadget) : List PauliString

theorem split_preserves_commuting_logical (g : SurgeryGadget) (L : PauliString)
    (s : StabilizerState) (hmem : L ∈ s)
    (hcomm : ∀ P ∈ detachObservables g, L.commutes P = true) :
    L ∈ measureChecks (detachObservables g) s

theorem detachObservables_zRow (g : SurgeryGadget) :
    ∀ P ∈ detachObservables g, ∃ v : BoolVec, P = zRow v

theorem split_preserves_zRow_logical (g : SurgeryGadget) (a : BoolVec)
    (s : StabilizerState) (hmem : zRow a ∈ s) :
    zRow a ∈ measureChecks (detachObservables g) s

theorem commutes_of_all_pos (L obs : PauliString)
    (h : ∀ p ∈ L.ops.zip obs.ops, Pauli.commutes p.1 p.2 = true) :
    L.commutes obs = true

theorem detachObs_commutes_of_I (L : PauliString) (q n : Nat)
    (hlen : L.ops.length = n) (hq : q < n)
    (hI : L.ops[q]'(by omega) = Pauli.I) :
    L.commutes (zRow ((List.range n).map (fun j => decide (j = q)))) = true

theorem split_preserves_data_logical (g : SurgeryGadget) (L : PauliString)
    (s : StabilizerState) (hmem : L ∈ s)
    (hlen : L.ops.length = g.merged_n)
    (hI : ∀ (q : Nat) (hq : q < g.merged_n), g.data_code.n ≤ q →
            L.ops[q]'(by rw [hlen]; exact hq) = Pauli.I) :
    L ∈ measureChecks (detachObservables g) s

def mergedCSS (g : SurgeryGadget) : CSSCode

theorem gadget_extractionRound_eq (g : SurgeryGadget) :
    SurgeryGadget.extractionRound g = CSSCode.extractionRound (mergedCSS g)

theorem merge_syndrome_correct (g : SurgeryGadget)
    (hws : (mergedCSS g).well_shaped = true) :
    Round.measuredDataObs
        ((mergedCSS g).n + (mergedCSS g).hx.length + (mergedCSS g).hz.length)
        (mergedCSS g).n
        (SurgeryGadget.extractionRound g)
      = (mergedCSS g).toStabilizers

def MergeFullyCorrect (g : SurgeryGadget) : Prop

theorem mergeFullyCorrect_of (g : SurgeryGadget) : MergeFullyCorrect g

theorem surface3_xx_merge_fully_correct : MergeFullyCorrect surface3_xx_merge

theorem surface3_xx_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS surface3_xx_merge).n
          + (mergedCSS surface3_xx_merge).hx.length
          + (mergedCSS surface3_xx_merge).hz.length)
        (mergedCSS surface3_xx_merge).n
        (SurgeryGadget.extractionRound surface3_xx_merge)
      = (mergedCSS surface3_xx_merge).toStabilizers

theorem surface3_xx_logical_correct (signs : List Bool)
    (hsig : signs.length = surface3_xx_merge.merged_hx.length) :
    selectedSignedProduct surface3_xx_merge.span_witness
        surface3_xx_merge.merged_hx signs
      = signedXRow (selectedParity surface3_xx_merge.span_witness signs)
          surface3_xx_merge.target_pauli

theorem surface3_xxx_merge_fully_correct : MergeFullyCorrect surface3_xxx_merge

theorem surface3_xx_resource_on_verified :
    surgeryPhysQubits surface3_xx_merge
      = surface3_xx_merge.merged_n + surface3_xx_merge.merged_hx.length
          + surface3_xx_merge.merged_hz.length
    ∧ surgeryMeasPerRound surface3_xx_merge
      = surface3_xx_merge.merged_hx.length + surface3_xx_merge.merged_hz.length

def windowedGate : FormalRV.Framework.Gate

theorem windowed_compiled : GadgetCompiledOK windowedGate

theorem windowed_measCount :
    measCountC (gadgetPhysical windowedGate)
      = physicalStmtCount (gadgetPPM windowedGate)
          * (27 * (Resource.width windowedGate * 728))

theorem windowed_qubits :
    boardPhysQubits (gadgetBoard windowedGate)
      = Resource.width windowedGate * 1457

def hConj : Pauli → Pauli
  | Pauli.I => Pauli.I
  | Pauli.X => Pauli.Z
  | Pauli.Y => Pauli.Y
  | Pauli.Z => Pauli.X

def sConj : Pauli → Pauli
  | Pauli.I => Pauli.I
  | Pauli.X => Pauli.Y
  | Pauli.Y => Pauli.X
  | Pauli.Z => Pauli.Z

def edgeConj (p : Pauli) : Pauli

theorem edgeConj_Z_eq_Y : edgeConj Pauli.Z = Pauli.Y

theorem edgeConj_perm :
    edgeConj Pauli.I = Pauli.I ∧ edgeConj Pauli.X = Pauli.Z
      ∧ edgeConj Pauli.Y = Pauli.X ∧ edgeConj Pauli.Z = Pauli.Y

theorem edgeConj_preserves_commutation (a b : Pauli) :
    Pauli.commutes (edgeConj a) (edgeConj b) = Pauli.commutes a b

def yByEdgeReadout (d tau bound : Nat) : SurgeryGadget

theorem yByEdgeReadout_fully_correct :
    MergeFullyCorrect (yByEdgeReadout 27 18 40)

theorem yByEdgeReadout_is_Zmerge (d tau bound : Nat) :
    yByEdgeReadout d tau bound = rotatedZMerge d tau bound

theorem yMeasurementMerge_is_Zmerge (d tau bound : Nat) :
    yMeasurementMerge d tau bound = mixedMerge yGadgetAxes d tau bound

theorem yGadgetAxes_all_Z : yGadgetAxes = [MergeAxis.zAxis, MergeAxis.zAxis]

theorem y_uses_only_T_resource :
    yMeasurementMerge 27 18 60 = mixedMerge [MergeAxis.zAxis, MergeAxis.zAxis] 27 18 60

theorem yFromT_fully_correct : MergeFullyCorrect (yMeasurementMerge 27 18 60)

def yGadgetAxes : List MergeAxis

def yMeasurementMerge (d tau bound : Nat) : SurgeryGadget

theorem yMerge3_verifies :
    SurgeryGadget.verify_surgery_gadget (yMeasurementMerge 3 2 30) = true

theorem yMerge3_fully_correct : MergeFullyCorrect (yMeasurementMerge 3 2 30)

theorem yMerge3_syndrome_correct :
    Round.measuredDataObs
        ((mergedCSS (yMeasurementMerge 3 2 30)).n
          + (mergedCSS (yMeasurementMerge 3 2 30)).hx.length
          + (mergedCSS (yMeasurementMerge 3 2 30)).hz.length)
        (mergedCSS (yMeasurementMerge 3 2 30)).n
        (SurgeryGadget.extractionRound (yMeasurementMerge 3 2 30))
      = (mergedCSS (yMeasurementMerge 3 2 30)).toStabilizers

theorem yMerge3_logical_correct (signs : List Bool)
    (hsig : signs.length = (yMeasurementMerge 3 2 30).merged_hx.length) :
    selectedSignedProduct (yMeasurementMerge 3 2 30).span_witness
        (yMeasurementMerge 3 2 30).merged_hx signs
      = signedXRow (selectedParity (yMeasurementMerge 3 2 30).span_witness signs)
          (yMeasurementMerge 3 2 30).target_pauli

theorem yMerge27_verifies :
    SurgeryGadget.verify_surgery_gadget (yMeasurementMerge 27 18 60) = true

theorem yMerge27_fully_correct : MergeFullyCorrect (yMeasurementMerge 27 18 60)

def code422 : CSSCode

example : code422.well_shaped = true

example : code422.css_condition = true

def code422Logical : LogicalBasis code422 2

example : code422Logical.valid = true

example : StabilizerState.valid (code422.toStabilizers) 4 = true

def surface3 : CSSCode

def surface5 : CSSCode

example : surface3.n = 13

example : surface3.well_shaped = true

example : surface3.css_condition = true

example : surface5.n = 41

example : surface5.well_shaped = true

example : surface5.css_condition = true

def bb18 : CSSCode

example : bb18.n = 248

example : bb18.css_condition = true

def A_lp16 : List (List Circ)

def A_lp20 : List (List Circ)

def A_lp24 : List (List Circ)

def lp16 : CSSCode

def lp20 : CSSCode

def lp24 : CSSCode

example : lp16.n = (3 * 3 + 7 * 7) * 45

example : lp20.n = (3 * 3 + 7 * 7) * 75

example : lp24.n = (3 * 3 + 7 * 7) * 91

def A_lpproc : List (List Circ)

def lpproc : CSSCode

example : lpproc.n = (3 * 3 + 5 * 5) * 33

abbrev BoolVec

abbrev BoolMat

def vec_xor : BoolVec → BoolVec → BoolVec
  | [],          _           => []
  | _,           []          => []
  | h1 :: t1,    h2 :: t2    => (h1 != h2) :: vec_xor t1 t2

def zero_vec (n : Nat) : BoolVec

def row_combination (sel : BoolVec) (mat : BoolMat) : BoolVec

def hcat (left right : BoolMat) : BoolMat

def vcat (top bot : BoolMat) : BoolMat

def matrix_has_n_cols (mat : BoolMat) (n : Nat) : Bool

def matrix_well_shaped (mat : BoolMat) : Bool

def max_column_weight (mat : BoolMat) (n_cols : Nat) : Nat

def max_row_weight (mat : BoolMat) : Nat

def is_qldpc (mat : BoolMat) (n_cols Δ : Nat) : Bool

example : vec_xor [true, false, true] [false, true, true] = [true, true, false]

example :
    row_combination [true, false, true]
      [ [true,  false, false]
      , [false, true,  false]
      , [false, false, true] ]
      = [true, false, true]

example :
    row_combination [true, true]
      [ [true,  false, false]
      , [false, true,  false] ]
      = [true, true, false]

example :
    hcat [[true, false]] [[true]] = [[true, false, true]]

example :
    vcat [[true, false]] [[false, true]]
      = [[true, false], [false, true]]

example :
    matrix_has_n_cols [[true, false], [false, true]] 2 = true

example :
    matrix_has_n_cols [[true, false], [false]] 2 = false

example :
    max_row_weight [[true, false, true], [false, false, false]] = 2

example :
    max_column_weight [[true, false, true], [true, false, true]] 3 = 2

example :
    is_qldpc [[true, false, true], [true, true, false]] 3 2 = true

example :
    is_qldpc [[true, true, true]] 3 2 = false

theorem subMod (a b ℓ : Nat) (hb : b < ℓ) (ha : a < ℓ) :
    (a + ℓ - b) % ℓ = if b ≤ a then a - b else a + ℓ - b

theorem negMod (e ℓ : Nat) (he : e < ℓ) : (ℓ - e) % ℓ = if e = 0 then 0 else ℓ - e

theorem dagger_contains (ℓ : Nat) (p : Circ) (hp : ∀ e ∈ p, e < ℓ)
    (i j : Nat) (hi : i < ℓ) (hj : j < ℓ) :
    (circDagger ℓ p).contains ((j + ℓ - i % ℓ) % ℓ) = p.contains ((i + ℓ - j % ℓ) % ℓ)

private theorem map_range_getD {α : Type _} (n i : Nat) (f : Nat → α) (d : α) (hi : i < n) :
    ((List.range n).map f).getD i d = f i

theorem circulant_circDagger_eq_transpose (ℓ : Nat) (p : Circ) (hp : ∀ e ∈ p, e < ℓ) :
    circulant ℓ (circDagger ℓ p) = transpose (circulant ℓ p) ℓ

private theorem sum_map_add (l : List Nat) (A B : Nat → Nat) :
    (l.map (fun x => A x + B x)).sum = (l.map A).sum + (l.map B).sum

private theorem countP_eq_sum_ite (q : List Nat) (P : Nat → Bool) :
    q.countP P = (q.map (fun j => if P j then 1 else 0)).sum

private theorem sum_countP_swap (p q : List Nat) (g : Nat → Nat → Bool) :
    (p.map (fun i => q.countP (fun j => g i j))).sum
      = (q.map (fun j => p.countP (fun i => g i j))).sum

theorem circMul_comm (ℓ : Nat) (p q : Circ) : circMul ℓ p q = circMul ℓ q p

private theorem sum_replicate (n a : Nat) : (List.replicate n a).sum = n * a

theorem circulant_row_length (ℓ : Nat) (e : Circ) (r : Nat) (hr : r < ℓ) :
    ((circulant ℓ e).getD r []).length = ℓ

theorem liftRow_length (ℓ : Nat) (pr : List Circ) (r : Nat) (hr : r < ℓ) :
    ((pr.map (fun e => circulant ℓ e)).flatMap (fun blk => blk.getD r [])).length
      = pr.length * ℓ

theorem liftMat_row_length (ℓ : Nat) (A : List (List Circ)) (C : Nat)
    (hrect : ∀ pr ∈ A, pr.length = C) :
    ∀ row ∈ liftMat ℓ A, row.length = C * ℓ

theorem getElem?_flatMap_uniform {α β : Type} (f : α → List β) (ℓ : Nat) :
    ∀ (l : List α), (∀ a ∈ l, (f a).length = ℓ) →
      ∀ (b s : Nat) (a : α), s < ℓ → l[b]? = some a →
        (l.flatMap f)[b * ℓ + s]? = (f a)[s]?

theorem liftMat_entry (ℓ : Nat) (A : List (List Circ)) (C : Nat)
    (hrect : ∀ pr ∈ A, pr.length = C)
    (a r b s : Nat) (ha : a < A.length) (hr : r < ℓ) (hb : b < C) (hs : s < ℓ) :
    ((liftMat ℓ A)[a * ℓ + r]?.getD []).getD (b * ℓ + s) false
      = ((circulant ℓ ((A[a]?.getD []).getD b [])).getD r []).getD s false

theorem pKron_row_length (ℓ : Nat) (A B : List (List Circ)) (cA cB : Nat)
    (hA : ∀ arow ∈ A, arow.length = cA) (hB : ∀ brow ∈ B, brow.length = cB) :
    ∀ row ∈ pKron ℓ A B, row.length = cA * cB

theorem pHcat_row_length (L R : List (List Circ)) (cL cR : Nat)
    (hL : ∀ row ∈ L, row.length = cL) (hR : ∀ row ∈ R, row.length = cR) :
    ∀ row ∈ pHcat L R, row.length = cL + cR

theorem pIdent_row_length (n : Nat) : ∀ row ∈ pIdent n, row.length = n

theorem pDagger_row_length (ℓ : Nat) (A : List (List Circ)) :
    ∀ row ∈ pDagger ℓ A, row.length = A.length

theorem matrix_has_n_cols_of (M : BoolMat) (n : Nat) (h : ∀ row ∈ M, row.length = n) :
    matrix_has_n_cols M n = true

theorem liftedProduct_well_shaped (ℓ : Nat) (A : List (List Circ)) (rA nA : Nat)
    (hA_rows : A.length = rA) (hA_cols : ∀ row ∈ A, row.length = nA) :
    (liftedProduct ℓ A rA nA).well_shaped = true

theorem circulant_getD_row (ℓ : Nat) (p : Circ) (r : Nat) (hr : r < ℓ) :
    (circulant ℓ p).getD r [] = (List.range ℓ).map (fun s => p.contains ((s + ℓ - r % ℓ) % ℓ))

theorem circulant_rows_zip (ℓ : Nat) (p q : Circ) (r r' : Nat) (hr : r < ℓ) (hr' : r' < ℓ) :
    (((circulant ℓ p).getD r []).zip ((circulant ℓ q).getD r' [])).countP (fun x => x.1 && x.2)
      = ((List.range ℓ).filter
          (fun s => p.contains ((s + ℓ - r) % ℓ) && q.contains ((s + ℓ - r') % ℓ))).length

theorem lp16_well_shaped : lp16.well_shaped = true

theorem lp20_well_shaped : lp20.well_shaped = true

theorem lp24_well_shaped : lp24.well_shaped = true

theorem lp_codes_well_shaped :
    lp16.well_shaped = true ∧ lp20.well_shaped = true ∧ lp24.well_shaped = true

def cH_L : LaSre

def cH_S : Surf

def cH_ports : List Port

def cH_paulis : Nat → Nat → Pauli

theorem cH_valid : cH_L.valid = true

theorem cH_maxK : cH_L.maxK = 6

theorem cH_correct : LaSCorrectFull cH_L cH_S cH_ports cH_paulis 1 = true

theorem cH_report_empty : LaSReport cH_L cH_S cH_ports cH_paulis 1 = []

theorem cH_wrong_generator_rejected :
    LaSCorrectFull cH_L (weldSurfP 3 hSurf mergeZSurf (fun _ => [1]) (fun _ => [0]))
      cH_ports cH_paulis 1 = false

def cI_L : LaSre

def cI_S : Surf

theorem cI_valid : cI_L.valid = true

theorem cI_also_passes_X : LaSCorrectFull cI_L cI_S cH_ports cH_paulis 1 = true

theorem cI_passes_Z_input :
    LaSCorrectFull cI_L cI_S
      [⟨0, 0, 0, 4, 5⟩, ⟨1, 0, 3, 4, 5⟩, ⟨0, 0, 5, 4, 5⟩, ⟨1, 0, 5, 4, 5⟩]
      (fun _ p => match p with | 0 => Pauli.Z | _ => Pauli.Z) 1 = true

theorem h_and_idle_same_planes_on_readout_worldline :
    (List.range 2).all (fun s =>
      [0, 2].all (fun k =>
        (hSurf.KI s 0 0 k == idle2Surf.KI s 0 0 k)
          && (hSurf.KJ s 0 0 k == idle2Surf.KJ s 0 0 k)))
      = true

def runA (B : LaSre) (BS : Surf) (top : LaSre) (topS : Surf)
    (bsel rsel : Nat) (inP rdP : Pauli) : Bool

def configsA : List ((LaSre × Surf) × (Nat × Nat) × Pauli × Pauli)

theorem cH_cI_same_verdict_sweep :
    configsA.all (fun cfg =>
      let t

theorem cH_has_rotation_sig : rotationColorSig hLaS = true

theorem cI_lacks_rotation_sig : rotationColorSig idle2 = false

def cH_S_straight : Surf

theorem cH_funcOK_forces_rotation :
    cH_L.funcOK cH_S 1 = true ∧ cH_L.funcOK cH_S_straight 1 = false

theorem cH_straight_surface_localized_violation :
    cH_L.funcViols cH_S_straight 1 = [Viol.orthogonal 0 0 0 1]

theorem cH_has_corner_pipe_idle_lacks :
    cH_L.ExistI 0 0 1 = true ∧ cI_L.ExistI 0 0 1 = false

theorem basisChangeCompA_complete_picture :
    -- (a) C_H is verified and measures the rotated operator
    LaSCorrectFull cH_L cH_S cH_ports cH_paulis 1 = true
    -- (b) the idle control CANNOT fail the same rotated spec (honest negative)
      ∧ LaSCorrectFull cI_L cI_S cH_ports cH_paulis 1 = true
    -- (c1) genuine teeth: the geometric color signature
      ∧ rotationColorSig hLaS = true
      ∧ rotationColorSig idle2 = false
    -- (c2) NEW genuine teeth: the welded composition's interior functionality
    --      forces the rotation (idle's straight surface fails funcOK)
      ∧ cH_L.funcOK cH_S 1 = true
      ∧ cH_L.funcOK cH_S_straight 1 = false

def cnI  : List (Nat × Nat × Nat)

def cnJ  : List (Nat × Nat × Nat)

def cnK  : List (Nat × Nat × Nat)

def cnCI : List (Nat × Nat × Nat)

def cnCJ : List (Nat × Nat × Nat)

def cnY  : List (Nat × Nat × Nat)

def cnotSynthLaS : LaSre

theorem cnotSynth_valid : cnotSynthLaS.valid = true

def ccIJ : List (Nat × Nat × Nat × Nat)

def ccIK : List (Nat × Nat × Nat × Nat)

def ccJK : List (Nat × Nat × Nat × Nat)

def ccJI : List (Nat × Nat × Nat × Nat)

def ccKI : List (Nat × Nat × Nat × Nat)

def ccKJ : List (Nat × Nat × Nat × Nat)

def cnotSynthSurf : Surf

def cnotPorts : List Port

def cnotFlows : List (List Pauli)

def cnotPaulis (s p : Nat) : Pauli

theorem cnotSynth_fully_correct :
    LaSCorrectFull cnotSynthLaS cnotSynthSurf cnotPorts cnotPaulis 4 = true

theorem cnotSynth_report_empty :
    LaSReport cnotSynthLaS cnotSynthSurf cnotPorts cnotPaulis 4 = []

def identityFlows : List (List Pauli)

def identityPaulis (s p : Nat) : Pauli

theorem cnot_not_identity :
    LaSCorrectFull cnotSynthLaS cnotSynthSurf cnotPorts identityPaulis 4 = false

def cnotSynthSurf_flip : Surf

theorem cnot_flip_rejected :
    LaSCorrectFull cnotSynthLaS cnotSynthSurf_flip cnotPorts cnotPaulis 4 = false

def czI  : List (Nat × Nat × Nat)

def czJ  : List (Nat × Nat × Nat)

def czK  : List (Nat × Nat × Nat)

def czCI : List (Nat × Nat × Nat)

def czCJ : List (Nat × Nat × Nat)

def czY  : List (Nat × Nat × Nat)

def czLaS : LaSre

theorem czLaS_valid : czLaS.valid = true

def czIJ : List (Nat × Nat × Nat × Nat)

def czIK : List (Nat × Nat × Nat × Nat)

def czJK : List (Nat × Nat × Nat × Nat)

def czJI : List (Nat × Nat × Nat × Nat)

def czKI : List (Nat × Nat × Nat × Nat)

def czKJ : List (Nat × Nat × Nat × Nat)

def czSurf : Surf

def czPorts : List Port

def czFlows : List (List Pauli)

def czPaulis (s p : Nat) : Pauli

theorem czLaS_fully_correct :
    LaSCorrectFull czLaS czSurf czPorts czPaulis 4 = true

theorem czLaS_report_empty :
    LaSReport czLaS czSurf czPorts czPaulis 4 = []

def chainOK (h n : Nat) (conn : List (Nat × Nat)) (w wj : Nat) :
    List LaSre → List Surf → Bool
  | [g], [s] =>
      g.maxI == w && g.maxJ == wj && g.maxK == h && g.valid && g.funcOK s n
  | (g :: g2 :: rest), (s :: srest) =>
      g.maxI == w && g.maxJ == wj && g.maxK == h && g.valid && g.funcOK s n
        && weldInterfaceValidOK2 h g (weldChain h conn (g2 :: rest)) conn w wj
        && weldInterfaceOK2 h g (weldChain h conn (g2 :: rest)) s (weldChainSurf h srest) conn n w wj
        && chainOK h n conn w wj (g2 :: rest) srest
  | _, _ => false

theorem chainOK_sound (h n : Nat) (conn : List (Nat × Nat)) (w wj : Nat) :
    ∀ (gs : List LaSre) (ss : List Surf), chainOK h n conn w wj gs ss = true →
      (weldChain h conn gs).valid = true
        ∧ (weldChain h conn gs).funcOK (weldChainSurf h ss) n = true
        ∧ (weldChain h conn gs).maxI = w ∧ (weldChain h conn gs).maxJ = wj

theorem weldChain_LaSCorrectFull (h n : Nat) (conn : List (Nat × Nat)) (w wj : Nat)
    (gs : List LaSre) (ss : List Surf) (ports : List Port) (paulis : Nat → Nat → Pauli)
    (hc : chainOK h n conn w wj gs ss = true)
    (hPorts : portsOK (weldChainSurf h ss) ports paulis n = true) :
    LaSCorrectFull (weldChain h conn gs) (weldChainSurf h ss) ports paulis n = true

def shorBlockGadgets : List LaSre

def shorBlockSurfs : List Surf

theorem shorBlock_chainOK :
    chainOK 3 3 measConn 2 1 shorBlockGadgets shorBlockSurfs = true

theorem shorBlock_ports :
    portsOK (weldChainSurf 3 shorBlockSurfs) measProgramPorts measProgramPaulis 3 = true

theorem shorBlock_correct :
    LaSCorrectFull (weldChain 3 measConn shorBlockGadgets) (weldChainSurf 3 shorBlockSurfs)
      measProgramPorts measProgramPaulis 3 = true

def mixChainConn : List (Nat × Nat)

def mixChain : List LaSre

def mixChainSurf : List Surf

def mixChainPorts : List Port

def mixChainPaulis : Nat → Nat → Pauli

theorem mixChain_chainOK :
    chainOK 9 3 mixChainConn 3 2 mixChain mixChainSurf = true

theorem mixChain_ports :
    portsOK (weldChainSurf 9 mixChainSurf) mixChainPorts mixChainPaulis 3 = true

theorem mixChain_correct :
    LaSCorrectFull (weldChain 9 mixChainConn mixChain) (weldChainSurf 9 mixChainSurf)
      mixChainPorts mixChainPaulis 3 = true

theorem cliffordFrame_sound :
    LaSCorrectFull mixLaS mixSurf mixPorts mixPaulis 3 = true
      ∧ LaSCorrectFull mixLaS mixSurf mixPorts mixPaulis_wrongZ 3 = false

def pureZShifted : LaSre

def pureZShiftedSurf : Surf

def fullLayerLaS : LaSre

def fullLayerSurf : Surf

def fullLayerPorts : List Port

def pureP : Nat → Nat → Pauli

def fullLayerPaulis : Nat → Nat → Pauli

theorem fullLayer_correct :
    LaSCorrectFull fullLayerLaS fullLayerSurf fullLayerPorts fullLayerPaulis 6 = true

def fullConn : List (Nat × Nat)

def fullChain : List LaSre

def fullChainSurf : List Surf

def fullChainPorts : List Port

def fullChainPaulis : Nat → Nat → Pauli

theorem fullChain_chainOK :
    chainOK 9 6 fullConn 5 2 fullChain fullChainSurf = true

theorem fullChain_ports :
    portsOK (weldChainSurf 9 fullChainSurf) fullChainPorts fullChainPaulis 6 = true

theorem fullChain_correct :
    LaSCorrectFull (weldChain 9 fullConn fullChain) (weldChainSurf 9 fullChainSurf)
      fullChainPorts fullChainPaulis 6 = true

def weld2 (kG : Nat) (G M : LaSre) (conn : List (Nat × Nat)) : LaSre

def weld2Surf (kG : Nat) (SG SM : Surf) (fmG fmM : Nat → List Nat) : Surf

def weld3 (kA kB : Nat) (A M C : LaSre) (conn : List (Nat × Nat)) : LaSre

def weld3Surf (kA kB : Nat) (SA SM SC : Surf) (fmA fmM fmC : Nat → List Nat) : Surf

theorem mixLaS_is_weld3 :
    mixLaS = weld3 3 6 layerA FormalRV.QEC.Gidney21.mergeZLaS layerA mixConn

theorem mixSurf_is_weld3Surf :
    mixSurf = weld3Surf 3 6 layerASurf FormalRV.QEC.Gidney21.mergeZSurf layerASurf
                fmLayer fmMerge fmLayer

theorem weld3_mixedMerge_correct :
    LaSCorrectFull
      (weld3 3 6 layerA FormalRV.QEC.Gidney21.mergeZLaS layerA mixConn)
      (weld3Surf 3 6 layerASurf FormalRV.QEC.Gidney21.mergeZSurf layerASurf
        fmLayer fmMerge fmLayer)
      mixPorts mixPaulis 3 = true

def memJSurf : Surf

def yReadLaS : LaSre

def yReadSurf : Surf

def yReadPorts : List Port

def yReadPaulis : Nat → Nat → Pauli

theorem yRead_report : LaSReport yReadLaS yReadSurf yReadPorts yReadPaulis 1 = []

theorem yReadWeld_correct :
    LaSCorrectFull yReadLaS yReadSurf yReadPorts yReadPaulis 1 = true

def yReadPaulis_wrongX : Nat → Nat → Pauli

theorem yReadWeld_not_X :
    LaSCorrectFull yReadLaS yReadSurf yReadPorts yReadPaulis_wrongX 1 = false

def hcL1 : LaSre

def hcS1 : Surf

def hcL2 : LaSre

def hcS2 : Surf

def hcConn : List (Nat × Nat)

def hcGadgets : List LaSre

def hcSurfs : List Surf

def hcPorts : List Port

def hcPaulis : Nat → Nat → Pauli

theorem hetCross_chainOK :
    chainOK 3 4 hcConn 3 1 hcGadgets hcSurfs = true

theorem hetCross_ports :
    portsOK (weldChainSurf 3 hcSurfs) hcPorts hcPaulis 4 = true

theorem hetCross_correct :
    LaSCorrectFull (weldChain 3 hcConn hcGadgets) (weldChainSurf 3 hcSurfs)
      hcPorts hcPaulis 4 = true

def hcPaulisAllZ : Nat → Nat → Pauli

theorem hetCross_allZ_rejected :
    LaSCorrectFull (weldChain 3 hcConn hcGadgets) (weldChainSurf 3 hcSurfs)
      hcPorts hcPaulisAllZ 4 = false

theorem hetCross_two_layers :
    (weldChain 3 hcConn hcGadgets).maxK = 6
      ∧ (weldChain 3 hcConn hcGadgets).ExistI 0 0 1 = true
      ∧ (weldChain 3 hcConn hcGadgets).ExistI 0 0 4 = false

theorem hetCross_Y_threads_seam :
    (weldChainSurf 3 hcSurfs).KI 3 2 0 0 = true ∧ (weldChainSurf 3 hcSurfs).KJ 3 2 0 0 = true
      ∧ (weldChainSurf 3 hcSurfs).KI 3 2 0 3 = true ∧ (weldChainSurf 3 hcSurfs).KJ 3 2 0 3 = true

def routeClass (paulis : List Pauli) : Nat

theorem class_pureZ : routeClass [Pauli.Z, Pauli.Z, Pauli.Z] = 0

theorem class_mixed : routeClass [Pauli.X, Pauli.Z] = 1

theorem class_Y : routeClass [Pauli.Y] = 2

def xColOf (cols : List Nat) (paulis : List Pauli) : Nat

def zColOf (cols : List Nat) (paulis : List Pauli) : Nat

def dispatchLaS (cols : List Nat) (paulis : List Pauli) (h : Nat) : LaSre

def dispatchSurf (cols : List Nat) (paulis : List Pauli) : Surf

theorem dispatch_pureZ_verified :
    LaSCorrectFull (dispatchLaS [0, 1] [Pauli.Z, Pauli.Z] 9) (dispatchSurf [0, 1] [Pauli.Z, Pauli.Z])
      (lrMergeMultiPortsH [0, 1] 9) (lrMergeMultiPaulis [0, 1]) 3 = true

theorem dispatch_pureZ3_verified :
    LaSCorrectFull (dispatchLaS [0, 1, 2] [Pauli.Z, Pauli.Z, Pauli.Z] 9)
      (dispatchSurf [0, 1, 2] [Pauli.Z, Pauli.Z, Pauli.Z])
      (lrMergeMultiPortsH [0, 1, 2] 9) (lrMergeMultiPaulis [0, 1, 2]) 4 = true

theorem dispatch_mixed_verified :
    LaSCorrectFull (dispatchLaS [1, 0] [Pauli.X, Pauli.Z] 9) (dispatchSurf [1, 0] [Pauli.X, Pauli.Z])
      (mixGenPorts 1 0) mixGenPaulis 3 = true

theorem dispatch_mixed_nonadjacent :
    LaSCorrectFull (dispatchLaS [2, 0] [Pauli.X, Pauli.Z] 9) (dispatchSurf [2, 0] [Pauli.X, Pauli.Z])
      (mixGenPorts 2 0) mixGenPaulis 3 = true

theorem dispatch_total :
    (LaSCorrectFull (dispatchLaS [0, 1] [Pauli.Z, Pauli.Z] 9) (dispatchSurf [0, 1] [Pauli.Z, Pauli.Z])
        (lrMergeMultiPortsH [0, 1] 9) (lrMergeMultiPaulis [0, 1]) 3 = true)
    ∧ (LaSCorrectFull (dispatchLaS [2, 0] [Pauli.X, Pauli.Z] 9) (dispatchSurf [2, 0] [Pauli.X, Pauli.Z])
        (mixGenPorts 2 0) mixGenPaulis 3 = true)

theorem geometric_per_round (k : GadgetKind) :
    ScheduleImplementsSpec (gadgetFor k) = true

theorem commuting_chain_scales (N : Nat) (hN : 0 < N) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N))
      (weldChainSurf 3 (foldSurfList (zMeasProg N)))
      (heteroStackPorts 2 (List.replicate N true)) (zMergePaulis 2) 3 = true

theorem Z_Z_commute (n q q' : Nat) : symp n (Zq q) (Zq q') = 0

theorem classical_frame_scales (n : Nat) (fs : List P2) (meas : P2) :
    symp n (frameOf fs) meas = (fs.map (fun f => symp n f meas)).foldr (· + ·) 0

theorem endToEnd_ZthenX (raw : ZMod 2) :
    ScheduleImplementsSpec (gadgetFor GadgetKind.zMerge) = true
      ∧ ScheduleImplementsSpec (gadgetFor GadgetKind.mX1) = true
      ∧ corrected 2 (Zq 0) (Xq 0) raw = raw + 1

theorem endToEnd_scalable (N : Nat) (hN : 0 < N) (raw : ZMod 2) :
    LaSCorrectFull
      (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N))
      (weldChainSurf 3 (foldSurfList (zMeasProg N)))
      (heteroStackPorts 2 (List.replicate N true)) (zMergePaulis 2) 3 = true
    ∧ corrected 2 (frameOf (List.replicate N (Zq 0))) (Zq 1) raw = raw

theorem program_seams (N : Nat) (hN : 0 < N) :
    physSeams (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)) = N

theorem program_depth (N : Nat) (hN : 0 < N) :
    (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)).maxK = 3 * N

theorem program_volume (N : Nat) (hN : 0 < N) :
    (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)).volume = 6 * N

theorem endToEnd_correct_and_costed (N : Nat) (hN : 0 < N) (raw : ZMod 2) :
    LaSCorrectFull
        (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N))
        (weldChainSurf 3 (foldSurfList (zMeasProg N)))
        (heteroStackPorts 2 (List.replicate N true)) (zMergePaulis 2) 3 = true
      ∧ corrected 2 (frameOf (List.replicate N (Zq 0))) (Zq 1) raw = raw
      ∧ physSeams (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)) = N
      ∧ (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)).maxK = 3 * N
      ∧ (foldPPMProgLaS 3 (zChainConn 2) (zMeasProg N)).volume = 6 * N

def shiftI (di : Nat) (L : LaSre) : LaSre

def shiftISurf (di : Nat) (S : Surf) : Surf

def q2idle : LaSre

def q2idleSurf : Surf

def layerA : LaSre

def layerASurf : Surf

def layerAPorts : List Port

def layerAPaulis : Nat → Nat → Pauli

theorem layerA_fully_correct :
    LaSCorrectFull layerA layerASurf layerAPorts layerAPaulis 4 = true

theorem layerA_report :
    LaSReport layerA layerASurf layerAPorts layerAPaulis 4 = []

def mixConn : List (Nat × Nat)

def fmLayer : Nat → List Nat

def fmMerge : Nat → List Nat

def mixLaS : LaSre

def mixSurf : Surf

def mixPorts : List Port

def mixPaulis : Nat → Nat → Pauli

theorem mix_report :
    LaSReport mixLaS mixSurf mixPorts mixPaulis 3 = []

theorem faithfulMixedMerge_fully_correct :
    LaSCorrectFull mixLaS mixSurf mixPorts mixPaulis 3 = true

def mixPaulis_wrongZ : Nat → Nat → Pauli

theorem faithfulMixedMerge_not_ZZ :
    LaSCorrectFull mixLaS mixSurf mixPorts mixPaulis_wrongZ 3 = false

theorem mixLaS_maxK : mixLaS.maxK = 9

def faithfulMxzSchedule : FormalRV.QEC.Gidney21.ScheduleLaS

theorem faithfulMxz_implements_spec :
    FormalRV.QEC.Gidney21.ScheduleImplementsSpec faithfulMxzSchedule = true

def hasYCube (L : LaSre) : Bool