noncomputable def cczKet : StateVec 3

noncomputable def CCZdata (ψ : StateVec 3) : StateVec 3

def cnotChainPerm (n : Nat) : Nat

noncomputable def cnotChain : Matrix (Fin 64) (Fin 64) ℂ

noncomputable def projAnc000 : Matrix (Fin 64) (Fin 64) ℂ

noncomputable def plus3 : StateVec 3

noncomputable def cczMatData (ψ : StateVec 3) : StateVec 3

theorem cnotChainPerm_lt (n : Nat) (h : n < 64) : cnotChainPerm n < 64

theorem cnotChainPerm_invol (n : Nat) (h : n < 64) :
    cnotChainPerm (cnotChainPerm n) = n

theorem cnotChain_mul_apply (v : Matrix (Fin 64) (Fin 1) ℂ) (i : Fin 64) (j : Fin 1) :
    (cnotChain * v) i j = v ⟨cnotChainPerm i.val, cnotChainPerm_lt i.val i.isLt⟩ j

theorem cczKet_eq_cczMat_plus3 : cczMat * plus3 = cczKet

theorem CCZdata_eq_cczMat_mul (ψ : StateVec 3) : CCZdata ψ = cczMat * ψ

theorem ccz_teleport_outcome_000 (ψ : StateVec 3) :
    projAnc000 * (cnotChain * (ψ ⊗ᵥ cczKet))
      = (1 / (2 * Real.sqrt 2) : ℂ) • (CCZdata ψ ⊗ᵥ (basisState 0 : StateVec 3))

theorem ccz_gadget_outcome_000_is_cczMat (ψ : StateVec 3) :
    projAnc000 * (cnotChain * (ψ ⊗ᵥ cczKet))
      = (1 / (2 * Real.sqrt 2) : ℂ) • (cczMatData ψ ⊗ᵥ (basisState 0 : StateVec 3))

theorem ccz_gadget_data_is_CCZ (ψ : StateVec 3) :
    ∃ c : ℂ, projAnc000 * (cnotChain * (ψ ⊗ᵥ cczKet))
      = c • (cczMatData ψ ⊗ᵥ (basisState 0 : StateVec 3))

def AllCertifiedT (F : TFactoryContract) (pool : List MagicToken) : Prop

theorem AllCertifiedT_nil (F : TFactoryContract) : AllCertifiedT F []

theorem AllCertifiedT_drop (F : TFactoryContract) :
    ∀ (n : Nat) (pool : List MagicToken),
      AllCertifiedT F pool → AllCertifiedT F (pool.drop n)

def encodeWithPool (input : Nat → Bool) (pool : List MagicToken) :
    MagicBasisPPMState

theorem encodeWithPool_observes (F : TFactoryContract)
    (input : Nat → Bool) (pool : List MagicToken) :
    (magicBasisRefinesApplyNat F).observesBits (encodeWithPool input pool) input

theorem magicBasisPPMGateRel_ICX_total :
    ∀ (g : Gate), isICXGate g = true →
      ∀ (s : MagicBasisPPMState),
        ∃ t, magicBasisPPMGateRel g s t
          ∧ t.magicPool = s.magicPool ∧ t.failed = s.failed

theorem compileMagic_ICX_eq_base_map :
    ∀ (g : Gate), isICXGate g = true →
      compileArithmeticGateToMagicPPM g
        = (compileArithmeticGateToPPM g).map MagicPPMCommand.base

theorem magicCompile_executable_ICX (F : TFactoryContract) :
    ∀ (g : Gate), isICXGate g = true →
      ∀ (s : MagicBasisPPMState),
        ∃ σ', MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g) s σ'
            ∧ σ'.magicPool = s.magicPool

theorem magicCompile_executable (F : TFactoryContract) :
    ∀ (g : Gate) (s : MagicBasisPPMState),
      AllCertifiedT F s.magicPool →
      magicPPMRequestCount (compileArithmeticGateToMagicPPM g) ≤ s.magicPool.length →
      ∃ σ',
        MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g) s σ'
        ∧ σ'.magicPool
            = s.magicPool.drop
                (magicPPMRequestCount (compileArithmeticGateToMagicPPM g))

theorem compileToMagicPPM_run_observe (F : TFactoryContract)
    (g : Gate) (input : Nat → Bool) (pool : List MagicToken)
    (hcert : AllCertifiedT F pool)
    (hlen : magicPPMRequestCount (compileArithmeticGateToMagicPPM g) ≤ pool.length) :
    ∃ σ',
      MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g)
        (encodeWithPool input pool) σ'
      ∧ (magicBasisRefinesApplyNat F).observesBits σ' (Gate.applyNat g input)

def shorMagicDemand (g : Gate) : Nat

def certifiedTToken (F : TFactoryContract) : MagicToken

theorem certifiedTToken_isCertified (F : TFactoryContract) :
    MagicToken.IsCertifiedTFrom F (certifiedTToken F)

def factoryProvision (F : TFactoryContract) (K : Nat) : List MagicToken

theorem factoryProvision_length (F : TFactoryContract) (K : Nat) :
    (factoryProvision F K).length = K

theorem factoryProvision_allCertified (F : TFactoryContract) (K : Nat) :
    AllCertifiedT F (factoryProvision F K)

def factoryRequestSchedule (factoryZone period_us K : Nat) : List SysCall

theorem factoryRequestSchedule_length (factoryZone period_us K : Nat) :
    (factoryRequestSchedule factoryZone period_us K).length = K

theorem factoryRequestSchedule_all_requestMagic (factoryZone period_us K : Nat) :
    ∀ sc ∈ factoryRequestSchedule factoryZone period_us K,
      sc.kind = SysCallKind.RequestMagicState factoryZone

def factoryProvisionLatency (spec : AtomicFactorySpec) (K : Nat) : Nat

theorem factory_schedule_meets_demand (F : TFactoryContract)
    (factoryZone period_us : Nat) (g : Gate) :
    (factoryRequestSchedule factoryZone period_us (shorMagicDemand g)).length
        = shorMagicDemand g
    ∧ (factoryProvision F (shorMagicDemand g)).length = shorMagicDemand g

def TFactoryContract.ofAtomic (spec : AtomicFactorySpec) (fid : Nat) :
    TFactoryContract

theorem TFactoryContract.ofAtomic_wellFormed (spec : AtomicFactorySpec) (fid : Nat)
    (hkind : spec.kind = MagicStateKind.T)
    (hsucc : spec.success_probability_ppm ≤ 1_000_000) :
    (TFactoryContract.ofAtomic spec fid).WellFormed

theorem compileToMagicPPM_provisioned_run_observe (F : TFactoryContract)
    (g : Gate) (input : Nat → Bool) :
    ∃ σ',
      MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g)
        (encodeWithPool input (factoryProvision F (shorMagicDemand g))) σ'
      ∧ (magicBasisRefinesApplyNat F).observesBits σ' (Gate.applyNat g input)

theorem compileToMagicPPM_provisioned_decoder_transfer (F : TFactoryContract)
    (g : Gate) (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (hGateCorrect : decode (Gate.applyNat g input) = expected) :
    ∃ σ' output,
      MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g)
        (encodeWithPool input (factoryProvision F (shorMagicDemand g))) σ'
      ∧ (magicBasisRefinesApplyNat F).observesBits σ' output
      ∧ decode output = expected

def gateCCXCount : Gate → Nat
  | .I          => 0
  | .X _        => 0
  | .CX _ _     => 0
  | .CCX _ _ _  => 1
  | .seq g₁ g₂  => gateCCXCount g₁ + gateCCXCount g₂

theorem shorMagicDemand_eq_ccxCount (g : Gate) :
    shorMagicDemand g = gateCCXCount g

theorem toySurgeryQECTraceLoweringEvidence :
    SurgeryQECTraceLoweringEvidence
      toyQECGadgetSpec
      toySchedulableSurgeryGadget
      toySurgeryVerifiedBackendBlock.schedule

inductive CircuitFragmentKind

def classifyGateForPPMLowering : Gate → CircuitFragmentKind
  | .I        => .arithmetic
  | .X _      => .arithmetic
  | .CX _ _   => .arithmetic
  | .CCX _ _ _ => .arithmetic
  | .seq _ _  => .arithmetic

def isArithmeticGate (g : Gate) : Bool

theorem isArithmeticGate_eq_true (g : Gate) : isArithmeticGate g = true

def classifyBaseUnitary1ForPPMLowering : BaseUnitary 1 → CircuitFragmentKind
  | .R _ _ _ => .qpePhaseRotation   -- conservative: rotated unless decomposed

def classifyBaseUnitary2ForPPMLowering : BaseUnitary 2 → CircuitFragmentKind
  | .CNOT => .cliffordT

def classifyBaseUComForPPMLowering {dim : Nat} : BaseUCom dim → CircuitFragmentKind
  | .seq c₁ c₂ =>
      match classifyBaseUComForPPMLowering c₁, classifyBaseUComForPPMLowering c₂ with
      | .unsupportedOpaque, _ | _, .unsupportedOpaque => .unsupportedOpaque
      | .qpePhaseRotation, _ | _, .qpePhaseRotation   => .qpePhaseRotation
      | _, _                                          => .cliffordT
  | .app1 u _       => classifyBaseUnitary1ForPPMLowering u
  | .app2 u _ _     => classifyBaseUnitary2ForPPMLowering u
  | .app3 _ _ _ _   => .unsupportedOpaque

inductive PPMCommand

abbrev PPMProgram

def compileArithmeticGateToPPM : Gate → PPMProgram
  | .I         => []
  | .X q       => [.applyFrameUpdate [q]]
  | .CX c t    =>
      [ .measurePauliKind PauliKind.Z [c, t]
      , .applyFrameUpdate [t] ]
  | .CCX a b t =>
      [ .useMagicT t
      , .measurePauliKind PauliKind.Z [a, b, t]
      , .applyFrameUpdate [t] ]
  | .seq g₁ g₂ =>
      compileArithmeticGateToPPM g₁ ++ compileArithmeticGateToPPM g₂

theorem compileArithmeticGateToPPM_I :
    compileArithmeticGateToPPM .I = []

theorem compileArithmeticGateToPPM_seq (g₁ g₂ : Gate) :
    compileArithmeticGateToPPM (.seq g₁ g₂)
      = compileArithmeticGateToPPM g₁
          ++ compileArithmeticGateToPPM g₂

theorem isArithmeticGate_of_Gate (g : Gate) : isArithmeticGate g = true

structure GateToPPMSemanticsModel

inductive PPMProgramRel (sem : GateToPPMSemanticsModel) :
    PPMProgram → sem.State → sem.State → Prop
  | nil  (s : sem.State) : PPMProgramRel sem [] s s
  | cons {cmd : PPMCommand} {rest : PPMProgram}
         {s t u : sem.State}
         (h1 : sem.ppmCommandRel cmd s t)
         (h2 : PPMProgramRel sem rest t u) :
         PPMProgramRel sem (cmd :: rest) s u

def ImplementsGateAsPPM
    (sem : GateToPPMSemanticsModel)
    (g : Gate) (ppm : PPMProgram) : Prop

theorem PPMProgramRel_append
    (sem : GateToPPMSemanticsModel) (p₁ p₂ : PPMProgram)
    (s u : sem.State) :
    PPMProgramRel sem (p₁ ++ p₂) s u ↔
      ∃ t, PPMProgramRel sem p₁ s t ∧ PPMProgramRel sem p₂ t u

structure ArithmeticPrimitivePPMObligations
    (sem : GateToPPMSemanticsModel)

theorem compileArithmeticGateToPPM_sound_from_primitives
    (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem) :
    ∀ g, ImplementsGateAsPPM sem g (compileArithmeticGateToPPM g)

structure VerifiedPPMMacro (sem : GateToPPMSemanticsModel)

def macroForX (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem)
    (q : LogicalQubitId) (rounds distance : Nat) :
    VerifiedPPMMacro sem

def macroForCNOT (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem)
    (c t : LogicalQubitId) (rounds distance : Nat) :
    VerifiedPPMMacro sem

def macroForToffoli (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem)
    (a b t : LogicalQubitId) (rounds distance : Nat) :
    VerifiedPPMMacro sem

structure VerifiedArithmeticPPMBlock
    (sem : GateToPPMSemanticsModel)

def VerifiedArithmeticPPMBlock.ofGate
    (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem)
    (g : Gate) :
    VerifiedArithmeticPPMBlock sem

def pauliOfPauliKind : PauliKind → PauliSem.Pauli
  | .I => PauliSem.Pauli.I
  | .X => PauliSem.Pauli.X
  | .Y => PauliSem.Pauli.Y
  | .Z => PauliSem.Pauli.Z

def pauliOpListOfKindOnQubits
    (n : Nat) (pk : PauliKind) (qs : List LogicalQubitId) :
    List PauliSem.Pauli

def pauliStringOfKindOnQubits
    (n : Nat) (pk : PauliKind) (qs : List LogicalQubitId) :
    Option PauliSem.PauliString

theorem pauliStringOfKindOnQubits_length
    (n : Nat) (pk : PauliKind) (qs : List LogicalQubitId)
    (P : PauliSem.PauliString)
    (h : pauliStringOfKindOnQubits n pk qs = some P) :
    P.ops.length = n

def stabilizerPPMCommandRel (n : Nat) :
    PPMCommand → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop
  | .measurePauliKind pk qs, s, t =>
      ∃ P : PauliSem.PauliString,
        pauliStringOfKindOnQubits n pk qs = some P
        ∧ (t = PPMOp.apply_PPM_pos s P ∨ t = PPMOp.apply_PPM_neg s P)
  | .applyFrameUpdate _,    s, t => t = s
  | .useMagicT _,           s, t => t = s

def stabilizerPPMSemanticsModel
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop) :
    GateToPPMSemanticsModel

def mkStabilizerPrimitiveObligations
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop)
    (hI  : ∀ s t, gateRel Gate.I s t → s = t)
    (hX  : ∀ q,
        ImplementsGateAsPPM (stabilizerPPMSemanticsModel n gateRel)
          (Gate.X q) (compileArithmeticGateToPPM (Gate.X q)))
    (hCX : ∀ c t,
        ImplementsGateAsPPM (stabilizerPPMSemanticsModel n gateRel)
          (Gate.CX c t) (compileArithmeticGateToPPM (Gate.CX c t)))
    (hCCX : ∀ a b t,
        ImplementsGateAsPPM (stabilizerPPMSemanticsModel n gateRel)

theorem PPMProgramRel_measure_single_step_pos
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop)
    (pk : PauliKind) (qs : List LogicalQubitId) (s : PPMOp.StabilizerState)
    (P : PauliSem.PauliString)
    (h : pauliStringOfKindOnQubits n pk qs = some P) :
    PPMProgramRel (stabilizerPPMSemanticsModel n gateRel)
      [PPMCommand.measurePauliKind pk qs]
      s
      (PPMOp.apply_PPM_pos s P)

theorem PPMProgramRel_measure_single_step_neg
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop)
    (pk : PauliKind) (qs : List LogicalQubitId) (s : PPMOp.StabilizerState)
    (P : PauliSem.PauliString)
    (h : pauliStringOfKindOnQubits n pk qs = some P) :
    PPMProgramRel (stabilizerPPMSemanticsModel n gateRel)
      [PPMCommand.measurePauliKind pk qs]
      s
      (PPMOp.apply_PPM_neg s P)

theorem PPMProgramRel_applyFrameUpdate_single_step
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop)
    (qs : List LogicalQubitId) (s : PPMOp.StabilizerState) :
    PPMProgramRel (stabilizerPPMSemanticsModel n gateRel)
      [PPMCommand.applyFrameUpdate qs] s s

theorem PPMProgramRel_useMagicT_single_step
    (n : Nat)
    (gateRel : Gate → PPMOp.StabilizerState → PPMOp.StabilizerState → Prop)
    (q : LogicalQubitId) (s : PPMOp.StabilizerState) :
    PPMProgramRel (stabilizerPPMSemanticsModel n gateRel)
      [PPMCommand.useMagicT q] s s

structure LogicalPauliFrame

def LogicalPauliFrame.empty : LogicalPauliFrame

def LogicalPauliFrame.toggleX (frame : LogicalPauliFrame)
    (q : LogicalQubitId) : LogicalPauliFrame

def LogicalPauliFrame.toggleZ (frame : LogicalPauliFrame)
    (q : LogicalQubitId) : LogicalPauliFrame

def LogicalPauliFrame.toggleXList (frame : LogicalPauliFrame)
    (qs : List LogicalQubitId) : LogicalPauliFrame

def LogicalPauliFrame.toggleZList (frame : LogicalPauliFrame)
    (qs : List LogicalQubitId) : LogicalPauliFrame

structure LogicalPPMState

def LogicalPPMState.empty (n : Nat) : LogicalPPMState

def logicalPPMCommandRel (n : Nat) :
    PPMCommand → LogicalPPMState → LogicalPPMState → Prop
  | .measurePauliKind pk qs, s, t =>
      ∃ P : PauliSem.PauliString,
        pauliStringOfKindOnQubits n pk qs = some P
        ∧ ( (t.stabilizer = PPMOp.apply_PPM_pos s.stabilizer P ∨
             t.stabilizer = PPMOp.apply_PPM_neg s.stabilizer P)
            ∧ t.frame = s.frame
            ∧ t.magicUsed = s.magicUsed )
  | .applyFrameUpdate qs,   s, t =>
      t.stabilizer = s.stabilizer
      ∧ t.frame = s.frame.toggleXList qs

def logicalPPMSemanticsModel
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop) :
    GateToPPMSemanticsModel

theorem PPMProgramRel_logical_measure_single_step_pos
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop)
    (pk : PauliKind) (qs : List LogicalQubitId)
    (s : LogicalPPMState) (P : PauliSem.PauliString)
    (h : pauliStringOfKindOnQubits n pk qs = some P) :
    PPMProgramRel (logicalPPMSemanticsModel n gateRel)
      [PPMCommand.measurePauliKind pk qs]
      s
      { stabilizer

theorem PPMProgramRel_logical_measure_single_step_neg
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop)
    (pk : PauliKind) (qs : List LogicalQubitId)
    (s : LogicalPPMState) (P : PauliSem.PauliString)
    (h : pauliStringOfKindOnQubits n pk qs = some P) :
    PPMProgramRel (logicalPPMSemanticsModel n gateRel)
      [PPMCommand.measurePauliKind pk qs]
      s
      { stabilizer

theorem PPMProgramRel_logical_applyFrameUpdate_single_step
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop)
    (qs : List LogicalQubitId) (s : LogicalPPMState) :
    PPMProgramRel (logicalPPMSemanticsModel n gateRel)
      [PPMCommand.applyFrameUpdate qs]
      s
      { stabilizer

theorem PPMProgramRel_logical_useMagicT_single_step
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop)
    (q : LogicalQubitId) (s : LogicalPPMState) :
    PPMProgramRel (logicalPPMSemanticsModel n gateRel)
      [PPMCommand.useMagicT q]
      s
      { stabilizer

def mkLogicalPPMPrimitiveObligations
    (n : Nat)
    (gateRel : Gate → LogicalPPMState → LogicalPPMState → Prop)
    (hI  : ∀ s t, gateRel Gate.I s t → s = t)
    (hX  : ∀ q,
        ImplementsGateAsPPM (logicalPPMSemanticsModel n gateRel)
          (Gate.X q) (compileArithmeticGateToPPM (Gate.X q)))
    (hCX : ∀ c t,
        ImplementsGateAsPPM (logicalPPMSemanticsModel n gateRel)
          (Gate.CX c t) (compileArithmeticGateToPPM (Gate.CX c t)))
    (hCCX : ∀ a b t,
        ImplementsGateAsPPM (logicalPPMSemanticsModel n gateRel)

def frameLevelGateRel : Gate → LogicalPPMState → LogicalPPMState → Prop
  | .I,        s, t => t = s
  | .X q,      s, t =>
      t.stabilizer = s.stabilizer
      ∧ t.frame = s.frame.toggleX q
      ∧ t.magicUsed = s.magicUsed
  | .CX _ _,   _, _ => False
  | .CCX _ _ _, _, _ => False
  | .seq g₁ g₂, s, u =>
      ∃ mid, frameLevelGateRel g₁ s mid ∧ frameLevelGateRel g₂ mid u

def frameLevelPPMSemanticsModel (n : Nat) : GateToPPMSemanticsModel

theorem frameLevelGateRel_I (s t : LogicalPPMState) :
    frameLevelGateRel Gate.I s t ↔ t = s

theorem frameLevelGateRel_X (q : LogicalQubitId) (s t : LogicalPPMState) :
    frameLevelGateRel (Gate.X q) s t ↔
      ( t.stabilizer = s.stabilizer
        ∧ t.frame = s.frame.toggleX q
        ∧ t.magicUsed = s.magicUsed )

theorem frameLevelGateRel_seq_decomp (g₁ g₂ : Gate) (s u : LogicalPPMState) :
    frameLevelGateRel (Gate.seq g₁ g₂) s u ↔
      ∃ mid, frameLevelGateRel g₁ s mid ∧ frameLevelGateRel g₂ mid u

theorem frameLevel_I_is_id (s t : LogicalPPMState)
    (h : frameLevelGateRel Gate.I s t) : s = t

theorem frameLevel_X_ok (n : Nat) (q : LogicalQubitId) :
    ImplementsGateAsPPM (frameLevelPPMSemanticsModel n) (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

structure ArithmeticIXPrimitivePPMObligations
    (sem : GateToPPMSemanticsModel)

def frameLevelIXObligations (n : Nat) :
    ArithmeticIXPrimitivePPMObligations (frameLevelPPMSemanticsModel n)

def cxMacroGateRel (n : Nat) :
    Gate → LogicalPPMState → LogicalPPMState → Prop
  | .I,        s, t => t = s
  | .X q,      s, t =>
      t.stabilizer = s.stabilizer
      ∧ t.frame = s.frame.toggleX q
      ∧ t.magicUsed = s.magicUsed
  | .CX c tgt, s, u =>
      ∃ (P : PauliSem.PauliString) (mid : LogicalPPMState),
        pauliStringOfKindOnQubits n PauliKind.Z [c, tgt] = some P
        ∧ ( mid.stabilizer = PPMOp.apply_PPM_pos s.stabilizer P
            ∨ mid.stabilizer = PPMOp.apply_PPM_neg s.stabilizer P )

def cxMacroPPMSemanticsModel (n : Nat) : GateToPPMSemanticsModel

theorem cxMacroGateRel_I (n : Nat) (s t : LogicalPPMState) :
    cxMacroGateRel n Gate.I s t ↔ t = s

theorem cxMacroGateRel_X (n : Nat) (q : LogicalQubitId) (s t : LogicalPPMState) :
    cxMacroGateRel n (Gate.X q) s t ↔
      ( t.stabilizer = s.stabilizer
        ∧ t.frame = s.frame.toggleX q
        ∧ t.magicUsed = s.magicUsed )

theorem cxMacroGateRel_seq_decomp (n : Nat) (g₁ g₂ : Gate)
    (s u : LogicalPPMState) :
    cxMacroGateRel n (Gate.seq g₁ g₂) s u ↔
      ∃ mid, cxMacroGateRel n g₁ s mid ∧ cxMacroGateRel n g₂ mid u

theorem cxMacro_I_is_id (n : Nat) (s t : LogicalPPMState)
    (h : cxMacroGateRel n Gate.I s t) : s = t

theorem cxMacro_X_ok (n : Nat) (q : LogicalQubitId) :
    ImplementsGateAsPPM (cxMacroPPMSemanticsModel n) (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

theorem cxMacro_CX_ok (n : Nat) (c tgt : LogicalQubitId) :
    ImplementsGateAsPPM (cxMacroPPMSemanticsModel n) (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

structure ArithmeticICXPrimitivePPMObligations
    (sem : GateToPPMSemanticsModel)

def cxMacroICXObligations (n : Nat) :
    ArithmeticICXPrimitivePPMObligations (cxMacroPPMSemanticsModel n)

def isICXGate : Gate → Bool
  | .I         => true
  | .X _       => true
  | .CX _ _    => true
  | .CCX _ _ _ => false
  | .seq g₁ g₂ => isICXGate g₁ && isICXGate g₂

theorem compileICXGateToPPM_sound_from_cxMacro (n : Nat) :
    ∀ g, isICXGate g = true →
      ImplementsGateAsPPM (cxMacroPPMSemanticsModel n) g
        (compileArithmeticGateToPPM g)

structure MagicAwarePPMState

def MagicAwarePPMState.empty (n : Nat) : MagicAwarePPMState

def magicAwarePPMCommandRel (n : Nat) :
    PPMCommand → MagicAwarePPMState → MagicAwarePPMState → Prop
  | .measurePauliKind pk qs, s, t =>
      logicalPPMCommandRel n (PPMCommand.measurePauliKind pk qs)
        s.logicalState t.logicalState
      ∧ t.magicLog = s.magicLog
  | .applyFrameUpdate qs,    s, t =>
      logicalPPMCommandRel n (PPMCommand.applyFrameUpdate qs)
        s.logicalState t.logicalState
      ∧ t.magicLog = s.magicLog
  | .useMagicT q,            s, t =>
      logicalPPMCommandRel n (PPMCommand.useMagicT q)

def magicAwarePPMSemanticsModel
    (n : Nat)
    (gateRel : Gate → MagicAwarePPMState → MagicAwarePPMState → Prop) :
    GateToPPMSemanticsModel

structure MagicInjectionObligations
    (sem : GateToPPMSemanticsModel)

def mkArithmeticPrimitiveObligationsWithMagic
    (sem : GateToPPMSemanticsModel)
    (icx : ArithmeticICXPrimitivePPMObligations sem)
    (mag : MagicInjectionObligations sem)
    (hseq : ∀ g₁ g₂ s u,
      sem.gateRel (Gate.seq g₁ g₂) s u ↔
        ∃ t, sem.gateRel g₁ s t ∧ sem.gateRel g₂ t u) :
    ArithmeticPrimitivePPMObligations sem

theorem compileArithmeticGateToPPM_sound_from_magic_interface
    (sem : GateToPPMSemanticsModel)
    (icx : ArithmeticICXPrimitivePPMObligations sem)
    (mag : MagicInjectionObligations sem)
    (hseq : ∀ g₁ g₂ s u,
      sem.gateRel (Gate.seq g₁ g₂) s u ↔
        ∃ t, sem.gateRel g₁ s t ∧ sem.gateRel g₂ t u) :
    ∀ g, ImplementsGateAsPPM sem g (compileArithmeticGateToPPM g)

structure VerifiedArithmeticToPPMBlock
    (sem : GateToPPMSemanticsModel)

def VerifiedArithmeticToPPMBlock.ofPrimitiveObligations
    (sem : GateToPPMSemanticsModel)
    (obs : ArithmeticPrimitivePPMObligations sem)
    (g : Gate) :
    VerifiedArithmeticToPPMBlock sem

def VerifiedArithmeticToPPMBlock.ofICX
    (n : Nat) (g : Gate) (hg : isICXGate g = true) :
    VerifiedArithmeticToPPMBlock (cxMacroPPMSemanticsModel n)

def VerifiedArithmeticToPPMBlock.ofMagicInterface
    (sem : GateToPPMSemanticsModel)
    (icx : ArithmeticICXPrimitivePPMObligations sem)
    (mag : MagicInjectionObligations sem)
    (hseq : ∀ g₁ g₂ s u,
      sem.gateRel (Gate.seq g₁ g₂) s u ↔
        ∃ t, sem.gateRel g₁ s t ∧ sem.gateRel g₂ t u)
    (g : Gate) :
    VerifiedArithmeticToPPMBlock sem

structure ArithmeticPPMSpec

structure VerifiedArithmeticPPMProgramBlock
    (sem : GateToPPMSemanticsModel)

structure VerifiedArithmeticPPMToSystemBlock
    (models : SystemModels) (sem : GateToPPMSemanticsModel)

theorem VerifiedArithmeticPPMToSystemBlock.system_invariants_ok
    (models : SystemModels) (sem : GateToPPMSemanticsModel)
    (b : VerifiedArithmeticPPMToSystemBlock models sem) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        b.backend.schedule.expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

structure PPMToBackendLoweringModel
    (models : SystemModels) (sem : GateToPPMSemanticsModel)

structure PPMProgramToBackendLoweringObligation
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)

structure VerifiedArithmeticPPMToSystemBlockV2
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)

theorem VerifiedArithmeticPPMToSystemBlockV2.system_invariants_ok
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)
    (b : VerifiedArithmeticPPMToSystemBlockV2 models sem lowering) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        b.backend.schedule.expand
        models.t_react_us

theorem VerifiedArithmeticPPMToSystemBlockV2.ppm_semantic
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)
    (b : VerifiedArithmeticPPMToSystemBlockV2 models sem lowering) :
    lowering.ppmProgramImplementsSpecs
      b.arithmeticPPM.arithmetic.ppmProgram
      b.arithmeticPPM.ppmSpecs

theorem VerifiedArithmeticPPMToSystemBlockV2.qec_backend
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)
    (b : VerifiedArithmeticPPMToSystemBlockV2 models sem lowering) :
    lowering.qecSpecsLowerToSchedule
      b.arithmeticPPM.qecSpecs
      b.backend.schedule

theorem VerifiedArithmeticPPMToSystemBlockV2.resource_alignment
    (models : SystemModels)
    (sem : GateToPPMSemanticsModel)
    (lowering : PPMToBackendLoweringModel models sem)
    (b : VerifiedArithmeticPPMToSystemBlockV2 models sem lowering) :
    lowering.resourceAlignment
      b.arithmeticPPM.arithmetic.ppmProgram
      b.backend.schedule

def ppmSpecsOfICXGate : Gate → List PPMSpec
  | .I         => []
  | .X q       =>
      [{ measuredPauliKind

theorem ppmSpecsOfICXGate_I : ppmSpecsOfICXGate Gate.I = []

theorem ppmSpecsOfICXGate_seq (g₁ g₂ : Gate) :
    ppmSpecsOfICXGate (Gate.seq g₁ g₂)
      = ppmSpecsOfICXGate g₁ ++ ppmSpecsOfICXGate g₂

structure ICXPPMProgramSpecWitness
    (n : Nat) (program : PPMProgram) (specs : List PPMSpec)

def ICXPPMProgramImplementsSpecs
    (n : Nat) (program : PPMProgram) (specs : List PPMSpec) : Prop

theorem compileICXGateToPPM_implements_specs
    (n : Nat) (g : Gate) (hg : isICXGate g = true) :
    ICXPPMProgramImplementsSpecs n
      (compileArithmeticGateToPPM g) (ppmSpecsOfICXGate g)

def ICXPartialLoweringModel
    (models : SystemModels) (n : Nat)
    (qecRel : List QECGadgetSpec → CompressedSchedule → Prop)
    (resRel : PPMProgram → CompressedSchedule → Prop) :
    PPMToBackendLoweringModel models (cxMacroPPMSemanticsModel n)

def VerifiedArithmeticPPMProgramBlock.ofICX
    (n : Nat) (g : Gate) (hg : isICXGate g = true)
    (qecSpecs : List QECGadgetSpec) :
    VerifiedArithmeticPPMProgramBlock (cxMacroPPMSemanticsModel n)

theorem VerifiedArithmeticPPMProgramBlock.ofICX_implements_specs
    (n : Nat) (g : Gate) (hg : isICXGate g = true)
    (qecSpecs : List QECGadgetSpec) :
    ICXPPMProgramImplementsSpecs n
      (VerifiedArithmeticPPMProgramBlock.ofICX n g hg qecSpecs).arithmetic.ppmProgram
      (VerifiedArithmeticPPMProgramBlock.ofICX n g hg qecSpecs).ppmSpecs

structure PPMProgramResourceSummary

def zero : PPMProgramResourceSummary

def add (a b : PPMProgramResourceSummary) : PPMProgramResourceSummary

def ppmCommandMeasureCount : PPMCommand → Nat
  | .measurePauliKind _ _ => 1
  | _                     => 0

def ppmCommandFrameUpdateCount : PPMCommand → Nat
  | .applyFrameUpdate _ => 1
  | _                   => 0

def ppmCommandMagicTCount : PPMCommand → Nat
  | .useMagicT _ => 1
  | _            => 0

def listSumOver {α : Type} (f : α → Nat) : List α → Nat
  | []      => 0
  | x :: xs => f x + listSumOver f xs

theorem listSumOver_append {α : Type} (f : α → Nat) (xs ys : List α) :
    listSumOver f (xs ++ ys) = listSumOver f xs + listSumOver f ys

def ppmProgramResourceSummary (p : PPMProgram) : PPMProgramResourceSummary

theorem ppmProgramResourceSummary_append (p₁ p₂ : PPMProgram) :
    ppmProgramResourceSummary (p₁ ++ p₂)
      = PPMProgramResourceSummary.add
          (ppmProgramResourceSummary p₁) (ppmProgramResourceSummary p₂)

theorem ppmProgramResourceSummary_compile_I :
    ppmProgramResourceSummary (compileArithmeticGateToPPM Gate.I)
      = PPMProgramResourceSummary.zero

theorem ppmProgramResourceSummary_compile_X (q : LogicalQubitId) :
    ppmProgramResourceSummary (compileArithmeticGateToPPM (Gate.X q))
      = PPMProgramResourceSummary.mk 1 0 1 0

theorem ppmProgramResourceSummary_compile_CX (c t : LogicalQubitId) :
    ppmProgramResourceSummary (compileArithmeticGateToPPM (Gate.CX c t))
      = PPMProgramResourceSummary.mk 2 1 1 0

theorem ppmProgramResourceSummary_compile_CCX (a b t : LogicalQubitId) :
    ppmProgramResourceSummary (compileArithmeticGateToPPM (Gate.CCX a b t))
      = PPMProgramResourceSummary.mk 3 1 1 1

theorem ppmProgramResourceSummary_compile_seq (g₁ g₂ : Gate) :
    ppmProgramResourceSummary (compileArithmeticGateToPPM (Gate.seq g₁ g₂))
      = PPMProgramResourceSummary.add
          (ppmProgramResourceSummary (compileArithmeticGateToPPM g₁))
          (ppmProgramResourceSummary (compileArithmeticGateToPPM g₂))

def ICXResourceAlignment
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (program : PPMProgram) (schedule : CompressedSchedule) : Prop

def ICXResourceLoweringModel
    (models : SystemModels) (n : Nat)
    (qecRel : List QECGadgetSpec → CompressedSchedule → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary) :
    PPMToBackendLoweringModel models (cxMacroPPMSemanticsModel n)

theorem VerifiedArithmeticPPMProgramBlock.ofICX_resourceAlignment
    (models : SystemModels) (n : Nat)
    (g : Gate) (hg : isICXGate g = true)
    (qecSpecs : List QECGadgetSpec)
    (qecRel : List QECGadgetSpec → CompressedSchedule → Prop)
    (backend : VerifiedBackendBlock models)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM g)) :
    (ICXResourceLoweringModel models n qecRel backendSummary).resourceAlignment
      (VerifiedArithmeticPPMProgramBlock.ofICX n g hg qecSpecs).arithmetic.ppmProgram

def specMatchListwise
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop) :
    List QECGadgetSpec → List SchedulableSurgeryGadget → Prop
  | [],      []      => True
  | _ :: _,  []      => False
  | [],      _ :: _  => False
  | q :: qs, g :: gs => specMatch q g ∧ specMatchListwise specMatch qs gs

structure SurgeryGadgetBackendLoweringWitness
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpec : QECGadgetSpec) (schedule : CompressedSchedule)

def SurgeryQECSpecLowerToScheduleOne
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpec : QECGadgetSpec) (schedule : CompressedSchedule) : Prop

def composedSurgerySchedule
    (gadgets : List SchedulableSurgeryGadget) : CompressedSchedule

def SurgeryQECSpecsLowerToSchedule
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpecs : List QECGadgetSpec) (schedule : CompressedSchedule) : Prop

theorem SurgeryQECSpecLowerToScheduleOne.construct
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpec : QECGadgetSpec) (gadget : SchedulableSurgeryGadget)
    (hmatch : specMatch qecSpec gadget) :
    SurgeryQECSpecLowerToScheduleOne specMatch qecSpec
      (CompressedSchedule.atom (compileSurgeryGadgetToSysCalls gadget))

theorem SurgeryQECSpecsLowerToSchedule.construct
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpecs : List QECGadgetSpec) (gadgets : List SchedulableSurgeryGadget)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets) :
    SurgeryQECSpecsLowerToSchedule specMatch qecSpecs
      (composedSurgerySchedule gadgets)

theorem SurgeryQECSpecsLowerToSchedule.nil
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop) :
    SurgeryQECSpecsLowerToSchedule specMatch []
      (composedSurgerySchedule [])

def ICXSurgeryLoweringModel
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary) :
    PPMToBackendLoweringModel models (cxMacroPPMSemanticsModel n)

def VerifiedArithmeticPPMToSystemBlockV2.ofICXSurgery
    (models : SystemModels) (n : Nat)
    (g : Gate) (hg : isICXGate g = true) (qecSpecs : List QECGadgetSpec)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (backend : VerifiedBackendBlock models)
    (hqec :
      SurgeryQECSpecsLowerToSchedule specMatch qecSpecs backend.schedule)
    (hres :
      ICXResourceAlignment backendSummary
        ((VerifiedArithmeticPPMProgramBlock.ofICX n g hg qecSpecs).arithmetic.ppmProgram)
        backend.schedule) :

def toyICXGate : Gate

theorem toyICXGate_isICX : isICXGate toyICXGate = true

def toyArithmeticPPMBlock (n : Nat) (qecSpecs : List QECGadgetSpec) :
    VerifiedArithmeticPPMProgramBlock (cxMacroPPMSemanticsModel n)

theorem toyArithmeticPPMBlock_implements_specs
    (n : Nat) (qecSpecs : List QECGadgetSpec) :
    ICXPPMProgramImplementsSpecs n
      (toyArithmeticPPMBlock n qecSpecs).arithmetic.ppmProgram
      (toyArithmeticPPMBlock n qecSpecs).ppmSpecs

theorem toy_qec_backend_ok
    (models : SystemModels)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (backend : VerifiedBackendBlock models)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets) :
    SurgeryQECSpecsLowerToSchedule specMatch qecSpecs backend.schedule

theorem toy_resource_alignment_ok
    (models : SystemModels) (n : Nat)
    (qecSpecs : List QECGadgetSpec)
    (backend : VerifiedBackendBlock models)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :
    ICXResourceAlignment backendSummary
      ((toyArithmeticPPMBlock n qecSpecs).arithmetic.ppmProgram)
      backend.schedule

def toyV2Block
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

theorem toyICXBlock_system_invariants_ok
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

theorem toyICXBlock_ppm_semantic
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

theorem toyICXBlock_qec_backend
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

theorem toyICXBlock_resource_alignment
    (models : SystemModels) (n : Nat)
    (specMatch : QECGadgetSpec → SchedulableSurgeryGadget → Prop)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch : specMatchListwise specMatch qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

def QECSpecMatchesSurgeryGadget
    (spec : QECGadgetSpec) (sg : SchedulableSurgeryGadget) : Prop

theorem QECSpecMatchesSurgeryGadget.tau_s_eq
    {spec : QECGadgetSpec} {sg : SchedulableSurgeryGadget}
    (h : QECSpecMatchesSurgeryGadget spec sg) :
    spec.gadget.tau_s = sg.gadget.tau_s

theorem QECSpecMatchesSurgeryGadget.code_eq
    {spec : QECGadgetSpec} {sg : SchedulableSurgeryGadget}
    (h : QECSpecMatchesSurgeryGadget spec sg) :
    spec.code = sg.gadget.data_code

theorem QECSpecMatchesSurgeryGadget.target_eq
    {spec : QECGadgetSpec} {sg : SchedulableSurgeryGadget}
    (h : QECSpecMatchesSurgeryGadget spec sg) :
    spec.gadget.target = sg.gadget.data_code

theorem QECSpecMatchesSurgeryGadget.syndromeRounds_eq
    {spec : QECGadgetSpec} {sg : SchedulableSurgeryGadget}
    (h : QECSpecMatchesSurgeryGadget spec sg) :
    spec.syndromeRounds = sg.gadget.tau_s

theorem QECSpecMatchesSurgeryGadget.decoder_eq
    {spec : QECGadgetSpec} {sg : SchedulableSurgeryGadget}
    (h : QECSpecMatchesSurgeryGadget spec sg) :
    spec.decoder = sg.decoder_id_base

def ICXConcreteSurgeryLoweringModel
    (models : SystemModels) (n : Nat)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary) :
    PPMToBackendLoweringModel models (cxMacroPPMSemanticsModel n)

theorem toy_qec_backend_ok_concrete
    (models : SystemModels)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (hmatch :
      specMatchListwise QECSpecMatchesSurgeryGadget qecSpecs gadgets)
    (backend : VerifiedBackendBlock models)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets) :
    SurgeryQECSpecsLowerToSchedule QECSpecMatchesSurgeryGadget qecSpecs
      backend.schedule

def toyV2BlockConcreteSpecMatch
    (models : SystemModels) (n : Nat)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch :
      specMatchListwise QECSpecMatchesSurgeryGadget qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

theorem toyICXBlockConcreteSpecMatch_system_invariants_ok
    (models : SystemModels) (n : Nat)
    (backendSummary : CompressedSchedule → PPMProgramResourceSummary)
    (qecSpecs : List QECGadgetSpec)
    (gadgets : List SchedulableSurgeryGadget)
    (backend : VerifiedBackendBlock models)
    (hmatch :
      specMatchListwise QECSpecMatchesSurgeryGadget qecSpecs gadgets)
    (hbackend : backend.schedule = composedSurgerySchedule gadgets)
    (hAlign :
      backendSummary backend.schedule
        = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)) :

def toyQECCode : QECCode

def toyPPMGadget : PPMGadget

def toyPPMSpec : PPMSpec

def toyQECGadgetSpec : QECGadgetSpec

def toyLDPCSurgeryGadget : LDPC.SurgeryGadget

def toySchedulableSurgeryGadget : SchedulableSurgeryGadget

theorem toy_QECSpecMatchesSurgeryGadget :
    QECSpecMatchesSurgeryGadget
      toyQECGadgetSpec
      toySchedulableSurgeryGadget

theorem toy_specMatchListwise_singleton :
    specMatchListwise
      QECSpecMatchesSurgeryGadget
      [toyQECGadgetSpec]
      [toySchedulableSurgeryGadget]

theorem toy_singleton_qec_backend_lowering :
    SurgeryQECSpecsLowerToSchedule
      QECSpecMatchesSurgeryGadget
      [toyQECGadgetSpec]
      (composedSurgerySchedule [toySchedulableSurgeryGadget])

def toySurgerySysCalls : List SysCall

def toySurgeryAtomSchedule : CompressedSchedule

theorem toySurgerySysCalls_length : toySurgerySysCalls.length = 6

def toySurgeryAncillaModel : AncillaModel

def toySurgerySystemModels : SystemModels

def toySurgeryComposedSchedule : CompressedSchedule

theorem toySurgeryBackendCert :
    compressed_schedule_strict_certificate_ok
      toySurgerySystemModels
      toySurgeryComposedSchedule = true

def toySurgeryVerifiedBackendBlock :
    VerifiedBackendBlock toySurgerySystemModels

theorem toySurgeryBackendBlock_strict_invariants_ok :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        toySurgerySystemModels.arch
        toySurgerySystemModels.opCap
        toySurgerySystemModels.slotCap
        toySurgerySystemModels.ancillaModel
        toySurgeryVerifiedBackendBlock.schedule.expand
        toySurgerySystemModels.t_react_us
        toySurgerySystemModels.window_us
        toySurgerySystemModels.max_per_window = true

theorem toySurgeryVerifiedBackendBlock_schedule_eq_composed :
    toySurgeryVerifiedBackendBlock.schedule
      = composedSurgerySchedule [toySchedulableSurgeryGadget]

def toyConstantBackendSummary :
    CompressedSchedule → PPMProgramResourceSummary

theorem toyConstantBackendSummary_alignment :
    toyConstantBackendSummary toySurgeryVerifiedBackendBlock.schedule
      = ppmProgramResourceSummary (compileArithmeticGateToPPM toyICXGate)

def toyConcreteEndToEndV2Block (n : Nat) :
    VerifiedArithmeticPPMToSystemBlockV2 toySurgerySystemModels
      (cxMacroPPMSemanticsModel n)
      (ICXConcreteSurgeryLoweringModel toySurgerySystemModels n
        toyConstantBackendSummary)

theorem toyConcreteEndToEnd_system_invariants_ok (n : Nat) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        toySurgerySystemModels.arch
        toySurgerySystemModels.opCap
        toySurgerySystemModels.slotCap
        toySurgerySystemModels.ancillaModel
        toySurgeryVerifiedBackendBlock.schedule.expand
        toySurgerySystemModels.t_react_us
        toySurgerySystemModels.window_us
        toySurgerySystemModels.max_per_window = true

inductive SurgeryObs

def syscallToSurgeryObs? : SysCall → Option SurgeryObs
  | { kind

def surgeryTraceOfSysCalls (xs : List SysCall) : List SurgeryObs

def surgeryTraceOfCompressedSchedule (cs : CompressedSchedule) : List SurgeryObs

def expectedSingleRoundTrace (g : SchedulableSurgeryGadget) :
    List SurgeryObs

def SurgeryTraceMatchesGadget
    (g : SchedulableSurgeryGadget) (tr : List SurgeryObs) : Prop

instance (g : SchedulableSurgeryGadget) (tr : List SurgeryObs) :
    Decidable (SurgeryTraceMatchesGadget g tr)

theorem toySurgeryTraceMatchesGadget :
    SurgeryTraceMatchesGadget toySchedulableSurgeryGadget
      (surgeryTraceOfSysCalls toySurgerySysCalls)

theorem toySurgeryComposedSchedule_trace_matches :
    SurgeryTraceMatchesGadget toySchedulableSurgeryGadget
      (surgeryTraceOfCompressedSchedule
        toySurgeryVerifiedBackendBlock.schedule)

structure SurgeryQECTraceLoweringEvidence
    (spec : QECGadgetSpec) (g : SchedulableSurgeryGadget)
    (sched : CompressedSchedule) : Prop

structure TFactoryContract

def TFactoryContract.WellFormed (F : TFactoryContract) : Prop

structure MagicToken

inductive FactoryOutcome

def MagicToken.IsCertifiedTFrom
    (F : TFactoryContract) (tok : MagicToken) : Prop

structure MagicBasisPPMState : Type

instance : Inhabited MagicBasisPPMState

def MagicBasisPPMState.toBasis (s : MagicBasisPPMState) : BasisPPMState

def BasisPPMState.withEmptyMagic (s : BasisPPMState) : MagicBasisPPMState

def hasCertifiedT (F : TFactoryContract) (s : MagicBasisPPMState) : Prop

def consumeCertifiedT
    (F : TFactoryContract) (s t : MagicBasisPPMState) : Prop

def requestTSuccess
    (F : TFactoryContract)
    (s t : MagicBasisPPMState) (tok : MagicToken) : Prop

def magicRequestCount (p : PPMProgram) : Nat

theorem magicRequestCount_nil : magicRequestCount [] = 0

theorem magicRequestCount_append (p q : PPMProgram) :
    magicRequestCount (p ++ q)
      = magicRequestCount p + magicRequestCount q

theorem magicRequestCount_compile_I :
    magicRequestCount (compileArithmeticGateToPPM Gate.I) = 0

theorem magicRequestCount_compile_X (q : Nat) :
    magicRequestCount (compileArithmeticGateToPPM (Gate.X q)) = 0

theorem magicRequestCount_compile_CX (c t : Nat) :
    magicRequestCount (compileArithmeticGateToPPM (Gate.CX c t)) = 0

theorem magicRequestCount_compile_CCX (a b c : Nat) :
    magicRequestCount (compileArithmeticGateToPPM (Gate.CCX a b c)) = 1

theorem magicRequestCount_compile_ICX :
    ∀ g, isICXGate g = true →
      magicRequestCount (compileArithmeticGateToPPM g) = 0

def allMagicRequestsSuccessProbLB
    (F : TFactoryContract) (k : Nat) : Nat

theorem allMagicRequestsSuccessProbLB_zero (F : TFactoryContract) :
    allMagicRequestsSuccessProbLB F 0 = 1

theorem allMagicRequestsSuccessProbLB_succ (F : TFactoryContract) (k : Nat) :
    allMagicRequestsSuccessProbLB F (k + 1)
      = allMagicRequestsSuccessProbLB F k * F.successProbLB_ppm

def magicBasisPPMCommandRel
    (F : TFactoryContract) :
    PPMCommand → MagicBasisPPMState → MagicBasisPPMState → Prop
  | .applyFrameUpdate qs, s, t =>
      t.bits = qs.foldl (fun bs q => update bs q (!bs q)) s.bits
      ∧ t.magicUsed = s.magicUsed
      ∧ t.magicPool = s.magicPool
      ∧ t.failed    = s.failed
  | .measurePauliKind PauliKind.Z [c, tgt], s, t =>
      t.bits = update s.bits tgt (xor (s.bits tgt) (!s.bits c))
      ∧ t.magicUsed = s.magicUsed
      ∧ t.magicPool = s.magicPool

def magicBasisPPMGateRel : Gate → MagicBasisPPMState → MagicBasisPPMState → Prop
  | .I,         s, t => t = s
  | .X q,       s, t =>
      t.bits = update s.bits q (!s.bits q)
      ∧ t.magicUsed = s.magicUsed
      ∧ t.magicPool = s.magicPool
      ∧ t.failed    = s.failed
  | .CX c tgt,  s, t =>
      t.bits = update s.bits tgt (xor (s.bits tgt) (s.bits c))
      ∧ t.magicUsed = s.magicUsed
      ∧ t.magicPool = s.magicPool
      ∧ t.failed    = s.failed

def magicBasisPPMSemanticsModel (F : TFactoryContract) : GateToPPMSemanticsModel

theorem magicBasisPPM_I_sound (F : TFactoryContract) :
    ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) Gate.I
      (compileArithmeticGateToPPM Gate.I)

theorem magicBasisPPM_X_sound (F : TFactoryContract) (q : Nat) :
    ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

theorem magicBasisPPM_CX_sound (F : TFactoryContract) (c tgt : Nat) :
    ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

theorem magicBasisPPM_seq_sound (F : TFactoryContract) (g₁ g₂ : Gate)
    (h₁ : ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) g₁
            (compileArithmeticGateToPPM g₁))
    (h₂ : ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) g₂
            (compileArithmeticGateToPPM g₂)) :
    ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) (Gate.seq g₁ g₂)
      (compileArithmeticGateToPPM (Gate.seq g₁ g₂))

theorem magicBasisPPMSound_ICX (F : TFactoryContract) :
    ∀ g, isICXGate g = true →
      ImplementsGateAsPPM (magicBasisPPMSemanticsModel F) g
        (compileArithmeticGateToPPM g)

theorem magicBasisPPM_I_reflects (F : TFactoryContract) :
    PPMReflectsGateRel (magicBasisPPMSemanticsModel F) Gate.I
      (compileArithmeticGateToPPM Gate.I)

theorem magicBasisPPM_X_reflects (F : TFactoryContract) (q : Nat) :
    PPMReflectsGateRel (magicBasisPPMSemanticsModel F) (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

theorem magicBasisPPM_CX_reflects (F : TFactoryContract) (c tgt : Nat) :
    PPMReflectsGateRel (magicBasisPPMSemanticsModel F) (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

theorem magicBasisPPM_seq_reflects (F : TFactoryContract) (g₁ g₂ : Gate)
    (h₁ : PPMReflectsGateRel (magicBasisPPMSemanticsModel F) g₁
            (compileArithmeticGateToPPM g₁))
    (h₂ : PPMReflectsGateRel (magicBasisPPMSemanticsModel F) g₂
            (compileArithmeticGateToPPM g₂)) :
    PPMReflectsGateRel (magicBasisPPMSemanticsModel F) (Gate.seq g₁ g₂)
      (compileArithmeticGateToPPM (Gate.seq g₁ g₂))

theorem magicBasisPPMReflects_ICX (F : TFactoryContract) :
    ∀ g, isICXGate g = true →
      PPMReflectsGateRel (magicBasisPPMSemanticsModel F) g
        (compileArithmeticGateToPPM g)

def magicBasisEncodeBits (F : TFactoryContract) (f : Nat → Bool) :
    (magicBasisPPMSemanticsModel F).State

def magicBasisObservesBits (F : TFactoryContract)
    (s : (magicBasisPPMSemanticsModel F).State)
    (f : Nat → Bool) : Prop

theorem magicBasisEncode_observes (F : TFactoryContract) (f : Nat → Bool) :
    magicBasisObservesBits F (magicBasisEncodeBits F f) f

theorem magicBasisPPMGateRel_imp_applyNat
    (g : Gate) :
    ∀ (s σ' : MagicBasisPPMState),
      magicBasisPPMGateRel g s σ' → σ'.bits = Gate.applyNat g s.bits

theorem magicBasisPPMGateRel_preserves_failed
    (g : Gate) :
    ∀ (s σ' : MagicBasisPPMState),
      magicBasisPPMGateRel g s σ' → σ'.failed = s.failed

theorem magicBasisGateRel_applyNat_obs (F : TFactoryContract)
    (g : Gate) (f : Nat → Bool)
    (σ' : (magicBasisPPMSemanticsModel F).State)
    (h : (magicBasisPPMSemanticsModel F).gateRel g
            (magicBasisEncodeBits F f) σ') :
    magicBasisObservesBits F σ' (Gate.applyNat g f)

def magicBasisRefinesApplyNat (F : TFactoryContract) :
    PPMRefinesApplyNat (magicBasisPPMSemanticsModel F)

theorem compileICXGateToPPM_applyNat_bridge_magicBasisPPM
    (F : TFactoryContract) (g : Gate) (hICX : isICXGate g = true) :
    LogicalGateAsPPMApplyNat (magicBasisPPMSemanticsModel F)
      (magicBasisRefinesApplyNat F) g

theorem shor_arithmetic_ICX_correctness_transfers_to_magicBasisPPM
    (F : TFactoryContract)
    (g : Gate) (hICX : isICXGate g = true)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (σ' : (magicBasisPPMSemanticsModel F).State)
    (hrun :
      PPMProgramRel (magicBasisPPMSemanticsModel F)
        (compileArithmeticGateToPPM g)
        ((magicBasisRefinesApplyNat F).encodeBits input)
        σ')
    (hGateCorrect : decode (Gate.applyNat g input) = expected) :

structure TFactoryToffoliObligation
    (F : TFactoryContract)

def ObservesCCXApplyNat
    (F : TFactoryContract) (a b c : Nat)
    (input : Nat → Bool)
    (σ' : (magicBasisPPMSemanticsModel F).State) : Prop

structure TFactoryToffoliObligationV2 (F : TFactoryContract)

theorem toffoli_obligationV2_decoder_transfer
    (F : TFactoryContract)
    (obl : TFactoryToffoliObligationV2 F)
    (a b c : Nat)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (σ' : (magicBasisPPMSemanticsModel F).State)
    (hrun :
      PPMProgramRel (magicBasisPPMSemanticsModel F)
        (obl.ccx_program a b c)
        ((magicBasisRefinesApplyNat F).encodeBits input) σ')
    (hGateCorrect :

def compileArithmeticGateToPPMWithToffoli
    (F : TFactoryContract)
    (obl : TFactoryToffoliObligationV2 F) :
    Gate → PPMProgram
  | Gate.I         => compileArithmeticGateToPPM Gate.I
  | Gate.X q       => compileArithmeticGateToPPM (Gate.X q)
  | Gate.CX c t    => compileArithmeticGateToPPM (Gate.CX c t)
  | Gate.CCX a b c => obl.ccx_program a b c
  | Gate.seq g₁ g₂ =>
      compileArithmeticGateToPPMWithToffoli F obl g₁
        ++ compileArithmeticGateToPPMWithToffoli F obl g₂

theorem compileArithmeticGateToPPMWithToffoli_applyNat_sound_from_observed
    (F : TFactoryContract)
    (obl : TFactoryToffoliObligationV2 F) :
    ∀ (g : Gate) (input : Nat → Bool)
      (s σ' : (magicBasisPPMSemanticsModel F).State),
      (magicBasisRefinesApplyNat F).observesBits s input →
      PPMProgramRel (magicBasisPPMSemanticsModel F)
        (compileArithmeticGateToPPMWithToffoli F obl g) s σ' →
      (magicBasisRefinesApplyNat F).observesBits σ'
        (Gate.applyNat g input)

theorem compileArithmeticGateToPPMWithToffoli_applyNat_sound
    (F : TFactoryContract)
    (obl : TFactoryToffoliObligationV2 F)
    (g : Gate) (input : Nat → Bool)
    (σ' : (magicBasisPPMSemanticsModel F).State)
    (hrun :
      PPMProgramRel (magicBasisPPMSemanticsModel F)
        (compileArithmeticGateToPPMWithToffoli F obl g)
        ((magicBasisRefinesApplyNat F).encodeBits input) σ') :
    (magicBasisRefinesApplyNat F).observesBits σ'
      (Gate.applyNat g input)

theorem shor_arithmetic_full_correctness_transfers_to_magicPPM_from_ToffoliObligation
    (F : TFactoryContract)
    (obl : TFactoryToffoliObligationV2 F)
    (g : Gate)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (σ' : (magicBasisPPMSemanticsModel F).State)
    (hrun :
      PPMProgramRel (magicBasisPPMSemanticsModel F)
        (compileArithmeticGateToPPMWithToffoli F obl g)
        ((magicBasisRefinesApplyNat F).encodeBits input) σ')
    (hGateCorrect : decode (Gate.applyNat g input) = expected) :

theorem magicRequestCount_compileWithToffoli_I
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) :
    magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl Gate.I) = 0

theorem magicRequestCount_compileWithToffoli_X
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) (q : Nat) :
    magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl (Gate.X q)) = 0

theorem magicRequestCount_compileWithToffoli_CX
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) (c t : Nat) :
    magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl (Gate.CX c t)) = 0

theorem magicRequestCount_compileWithToffoli_CCX
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) (a b c : Nat) :
    magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl (Gate.CCX a b c))
      = magicRequestCount (obl.ccx_program a b c)

theorem magicRequestCount_compileWithToffoli_seq
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) (g₁ g₂ : Gate) :
    magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl (Gate.seq g₁ g₂))
      = magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl g₁)
        + magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl g₂)

theorem magicRequestCount_compileWithToffoli_ICX
    (F : TFactoryContract) (obl : TFactoryToffoliObligationV2 F) :
    ∀ g, isICXGate g = true →
      magicRequestCount (compileArithmeticGateToPPMWithToffoli F obl g) = 0

structure BasisPPMState

instance : Inhabited BasisPPMState

def basisPPMGateRel : Gate → BasisPPMState → BasisPPMState → Prop
  | .I,         s, t => t = s
  | .X q,       s, t =>
      t.bits = update s.bits q (!s.bits q)
      ∧ t.magicUsed = s.magicUsed
  | .CX c tgt,  s, t =>
      t.bits = update s.bits tgt (xor (s.bits tgt) (s.bits c))
      ∧ t.magicUsed = s.magicUsed
  | .CCX a b c, s, t =>
      t.bits = update s.bits c (xor (s.bits c) (s.bits a && s.bits b))
      ∧ t.magicUsed = s.magicUsed + 1
  | .seq g₁ g₂, s, u =>

def basisPPMCommandRel :
    PPMCommand → BasisPPMState → BasisPPMState → Prop
  | .applyFrameUpdate qs, s, t =>
      t.bits = qs.foldl (fun bs q => update bs q (!bs q)) s.bits
      ∧ t.magicUsed = s.magicUsed
  | .measurePauliKind PauliKind.Z [c, tgt], s, t =>
      t.bits = update s.bits tgt (xor (s.bits tgt) (!s.bits c))
      ∧ t.magicUsed = s.magicUsed
  | .measurePauliKind _ _, s, t =>
      t = s
  | .useMagicT _, s, t =>
      t.bits = s.bits

def basisPPMSemanticsModel : GateToPPMSemanticsModel

def basisEncodeBits (f : Nat → Bool) : basisPPMSemanticsModel.State

def basisObservesBits
    (s : basisPPMSemanticsModel.State) (f : Nat → Bool) : Prop

theorem basisEncode_observes (f : Nat → Bool) :
    basisObservesBits (basisEncodeBits f) f

theorem basisPPMGateRel_imp_applyNat
    (g : Gate) :
    ∀ (s σ' : BasisPPMState),
      basisPPMGateRel g s σ' → σ'.bits = Gate.applyNat g s.bits

theorem basisGateRel_applyNat_obs
    (g : Gate) (f : Nat → Bool) (σ' : basisPPMSemanticsModel.State)
    (h : basisPPMSemanticsModel.gateRel g (basisEncodeBits f) σ') :
    basisObservesBits σ' (Gate.applyNat g f)

def basisRefinesApplyNat : PPMRefinesApplyNat basisPPMSemanticsModel

theorem basisPPM_I_sound :
    ImplementsGateAsPPM basisPPMSemanticsModel Gate.I
      (compileArithmeticGateToPPM Gate.I)

theorem basisPPM_X_sound (q : Nat) :
    ImplementsGateAsPPM basisPPMSemanticsModel (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

theorem basisPPM_CX_sound (c tgt : Nat) :
    ImplementsGateAsPPM basisPPMSemanticsModel (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

theorem basisPPM_seq_sound (g₁ g₂ : Gate)
    (h₁ : ImplementsGateAsPPM basisPPMSemanticsModel g₁
            (compileArithmeticGateToPPM g₁))
    (h₂ : ImplementsGateAsPPM basisPPMSemanticsModel g₂
            (compileArithmeticGateToPPM g₂)) :
    ImplementsGateAsPPM basisPPMSemanticsModel (Gate.seq g₁ g₂)
      (compileArithmeticGateToPPM (Gate.seq g₁ g₂))

theorem basisPPMSound_ICX :
    ∀ g, isICXGate g = true →
      ImplementsGateAsPPM basisPPMSemanticsModel g
        (compileArithmeticGateToPPM g)

theorem basisPPM_I_reflects :
    PPMReflectsGateRel basisPPMSemanticsModel Gate.I
      (compileArithmeticGateToPPM Gate.I)

theorem basisPPM_X_reflects (q : Nat) :
    PPMReflectsGateRel basisPPMSemanticsModel (Gate.X q)
      (compileArithmeticGateToPPM (Gate.X q))

theorem basisPPM_CX_reflects (c tgt : Nat) :
    PPMReflectsGateRel basisPPMSemanticsModel (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

theorem basisPPM_seq_reflects (g₁ g₂ : Gate)
    (h₁ : PPMReflectsGateRel basisPPMSemanticsModel g₁
            (compileArithmeticGateToPPM g₁))
    (h₂ : PPMReflectsGateRel basisPPMSemanticsModel g₂
            (compileArithmeticGateToPPM g₂)) :
    PPMReflectsGateRel basisPPMSemanticsModel (Gate.seq g₁ g₂)
      (compileArithmeticGateToPPM (Gate.seq g₁ g₂))

theorem basisPPMReflects_ICX :
    ∀ g, isICXGate g = true →
      PPMReflectsGateRel basisPPMSemanticsModel g
        (compileArithmeticGateToPPM g)

theorem compileICXGateToPPM_applyNat_bridge_basisPPM
    (g : Gate) (hICX : isICXGate g = true) :
    LogicalGateAsPPMApplyNat basisPPMSemanticsModel
      basisRefinesApplyNat g

theorem shor_arithmetic_ICX_correctness_transfers_to_basisPPM
    (g : Gate) (hICX : isICXGate g = true)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (σ' : basisPPMSemanticsModel.State)
    (hrun :
      PPMProgramRel basisPPMSemanticsModel
        (compileArithmeticGateToPPM g)
        (basisRefinesApplyNat.encodeBits input)
        σ')
    (hGateCorrect :
      decode (Gate.applyNat g input) = expected) :

inductive HLGate

def gateToPPM (na : Nat) : HLGate → List QasmOp
  | .H q       => [.opH q]
  | .S q       => [.opS q]
  | .X q       => [.opX q]
  | .Z q       => [.opZ q]
  | .CNOT c t  => [.opCX c t]
  | .T q       => [.opH na, .opT na, .opCX q na, .opMeas na 0, .opIf 0 (.opS q)]
  | .CCZ a b c =>
      [ .opH na, .opH (na+1), .opH (na+2), .opCCZ na (na+1) (na+2),
        .opCX a na, .opCX b (na+1), .opCX c (na+2),
        .opMeas na 0, .opMeas (na+1) 1, .opMeas (na+2) 2,
        .opIf 0 (.opCZ b c), .opIf 1 (.opCZ a c), .opIf 2 (.opCZ a b),

def circuitToPPM (na : Nat) (gs : List HLGate) : List QasmOp

def gateTMagic : HLGate → Nat | .T _ => 1 | _ => 0

def gateCCZMagic : HLGate → Nat | .CCZ _ _ _ => 1 | _ => 0

def gateMeas : HLGate → Nat | .T _ => 1 | .CCZ _ _ _ => 3 | _ => 0

def gateClifford : HLGate → Nat
  | .H _ => 1 | .S _ => 1 | .X _ => 1 | .Z _ => 1 | .CNOT _ _ => 1
  | .T _ => 2 | .CCZ _ _ _ => 6

def gateFeedforward : HLGate → Nat | .T _ => 1 | .CCZ _ _ _ => 6 | _ => 0

theorem numTMagic_gateToPPM (na : Nat) (g : HLGate) :
    numTMagic (gateToPPM na g) = gateTMagic g

theorem numCCZMagic_gateToPPM (na : Nat) (g : HLGate) :
    numCCZMagic (gateToPPM na g) = gateCCZMagic g

theorem numMeas_gateToPPM (na : Nat) (g : HLGate) :
    numMeas (gateToPPM na g) = gateMeas g

theorem numClifford_gateToPPM (na : Nat) (g : HLGate) :
    numClifford (gateToPPM na g) = gateClifford g

theorem numFeedforward_gateToPPM (na : Nat) (g : HLGate) :
    numFeedforward (gateToPPM na g) = gateFeedforward g

theorem numTMagic_circuitToPPM (na : Nat) (gs : List HLGate) :
    numTMagic (circuitToPPM na gs) = (gs.map gateTMagic).sum

theorem numCCZMagic_circuitToPPM (na : Nat) (gs : List HLGate) :
    numCCZMagic (circuitToPPM na gs) = (gs.map gateCCZMagic).sum

theorem numMeas_circuitToPPM (na : Nat) (gs : List HLGate) :
    numMeas (circuitToPPM na gs) = (gs.map gateMeas).sum

theorem numClifford_circuitToPPM (na : Nat) (gs : List HLGate) :
    numClifford (circuitToPPM na gs) = (gs.map gateClifford).sum

theorem numFeedforward_circuitToPPM (na : Nat) (gs : List HLGate) :
    numFeedforward (circuitToPPM na gs) = (gs.map gateFeedforward).sum

def demoCircuit : List HLGate

theorem demo_TMagic   : numTMagic   (circuitToPPM 3 demoCircuit) = 2

theorem demo_CCZMagic : numCCZMagic (circuitToPPM 3 demoCircuit) = 1

theorem demo_Meas     : numMeas     (circuitToPPM 3 demoCircuit) = 5

theorem demo_Clifford : numClifford (circuitToPPM 3 demoCircuit) = 12

theorem demo_Feedforward : numFeedforward (circuitToPPM 3 demoCircuit) = 8

def toffoli (a b c : Nat) : List HLGate

def shor15Modmult : List HLGate

theorem shor15_TMagic      : numTMagic      (circuitToPPM 8 shor15Modmult) = 0

theorem shor15_CCZMagic    : numCCZMagic    (circuitToPPM 8 shor15Modmult) = 27

theorem shor15_Meas        : numMeas        (circuitToPPM 8 shor15Modmult) = 81

theorem shor15_Clifford    : numClifford    (circuitToPPM 8 shor15Modmult) = 228

theorem shor15_Feedforward : numFeedforward (circuitToPPM 8 shor15Modmult) = 162

theorem sum_map_flatten_replicate (n : Nat) (L : List HLGate) (f : HLGate → Nat) :
    (((List.replicate n L).flatten).map f).sum = n * (L.map f).sum

def modmultBlock (nToff nCnot : Nat) : List HLGate

theorem modmult_CCZMagic (nToff nCnot : Nat) :
    numCCZMagic (circuitToPPM 8 (modmultBlock nToff nCnot)) = nToff

theorem modmult_Meas (nToff nCnot : Nat) :
    numMeas (circuitToPPM 8 (modmultBlock nToff nCnot)) = 3 * nToff

example : numCCZMagic (circuitToPPM 8 (modmultBlock 27 12)) = 27

example : numMeas (circuitToPPM 8 (modmultBlock 27 12)) = 81

structure PPMRefinesApplyNat (sem : GateToPPMSemanticsModel)

def PPMReflectsGateRel
    (sem : GateToPPMSemanticsModel)
    (g : Gate) (ppm : PPMProgram) : Prop

structure LogicalGateAsPPMApplyNat
    (sem : GateToPPMSemanticsModel)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate) : Prop

theorem LogicalGateAsPPMApplyNat.from_refinement
    (sem : GateToPPMSemanticsModel)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (hppm :
      ImplementsGateAsPPM sem g (compileArithmeticGateToPPM g))
    (hreflect :
      PPMReflectsGateRel sem g (compileArithmeticGateToPPM g)) :
    LogicalGateAsPPMApplyNat sem bridge g

theorem compileICXGateToPPM_applyNat_bridge
    (n : Nat)
    (bridge : PPMRefinesApplyNat (cxMacroPPMSemanticsModel n))
    (g : Gate)
    (hICX : isICXGate g = true)
    (hreflect :
      PPMReflectsGateRel (cxMacroPPMSemanticsModel n) g
        (compileArithmeticGateToPPM g)) :
    LogicalGateAsPPMApplyNat (cxMacroPPMSemanticsModel n) bridge g

theorem PPMProgramRel_nil_iff
    (sem : GateToPPMSemanticsModel) (s t : sem.State) :
    PPMProgramRel sem [] s t ↔ s = t

theorem PPMProgramRel_cons_inv
    (sem : GateToPPMSemanticsModel)
    (cmd : PPMCommand) (rest : PPMProgram)
    (s u : sem.State)
    (h : PPMProgramRel sem (cmd :: rest) s u) :
    ∃ mid, sem.ppmCommandRel cmd s mid
        ∧ PPMProgramRel sem rest mid u

theorem PPMProgramRel_append_inv
    (sem : GateToPPMSemanticsModel)
    (p q : PPMProgram) (s u : sem.State)
    (h : PPMProgramRel sem (p ++ q) s u) :
    ∃ mid, PPMProgramRel sem p s mid
        ∧ PPMProgramRel sem q mid u

theorem cxMacro_I_reflects_gateRel (n : Nat) :
    PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
      Gate.I (compileArithmeticGateToPPM Gate.I)

theorem cxMacro_X_reflects_gateRel (n : Nat) (q : Nat) :
    PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
      (Gate.X q) (compileArithmeticGateToPPM (Gate.X q))

theorem cxMacro_CX_reflects_gateRel
    (n : Nat) (c tgt : Nat) :
    PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
      (Gate.CX c tgt)
      (compileArithmeticGateToPPM (Gate.CX c tgt))

theorem cxMacro_seq_reflects_gateRel
    (n : Nat) (g₁ g₂ : Gate)
    (h₁ :
      PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
        g₁ (compileArithmeticGateToPPM g₁))
    (h₂ :
      PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
        g₂ (compileArithmeticGateToPPM g₂)) :
    PPMReflectsGateRel (cxMacroPPMSemanticsModel n)
      (Gate.seq g₁ g₂)
      (compileArithmeticGateToPPM (Gate.seq g₁ g₂))

theorem compileICXGateToPPM_reflects_gateRel_from_cxMacro
    (n : Nat) :
    ∀ g, isICXGate g = true →
      PPMReflectsGateRel (cxMacroPPMSemanticsModel n) g
        (compileArithmeticGateToPPM g)

theorem compileICXGateToPPM_applyNat_bridge_no_reflect_hyp
    (n : Nat)
    (bridge : PPMRefinesApplyNat (cxMacroPPMSemanticsModel n))
    (g : Gate)
    (hICX : isICXGate g = true) :
    LogicalGateAsPPMApplyNat (cxMacroPPMSemanticsModel n) bridge g

theorem applyNat_postcondition_transfers_to_PPM
    (sem : GateToPPMSemanticsModel)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (P : (Nat → Bool) → Prop)
    (hbridge : LogicalGateAsPPMApplyNat sem bridge g)
    (input : Nat → Bool)
    (σ' : sem.State)
    (hrun :
      PPMProgramRel sem
        (compileArithmeticGateToPPM g)
        (bridge.encodeBits input)

theorem decoder_postcondition_transfers_to_PPM
    (sem : GateToPPMSemanticsModel)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (decode : (Nat → Bool) → Nat)
    (expected : Nat)
    (hbridge : LogicalGateAsPPMApplyNat sem bridge g)
    (input : Nat → Bool)
    (σ' : sem.State)
    (hrun :
      PPMProgramRel sem
        (compileArithmeticGateToPPM g)

theorem shor_arithmetic_applyNat_correctness_transfers_to_PPM
    (sem : GateToPPMSemanticsModel)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool)
    (expected : Nat)
    (hbridge : LogicalGateAsPPMApplyNat sem bridge g)
    (σ' : sem.State)
    (hrun :
      PPMProgramRel sem
        (compileArithmeticGateToPPM g)

theorem shor_arithmetic_ICX_correctness_transfers_to_PPM_no_reflect_hyp
    (n : Nat)
    (bridge : PPMRefinesApplyNat (cxMacroPPMSemanticsModel n))
    (g : Gate)
    (hICX : isICXGate g = true)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool)
    (expected : Nat)
    (σ' : (cxMacroPPMSemanticsModel n).State)
    (hrun :
      PPMProgramRel (cxMacroPPMSemanticsModel n)
        (compileArithmeticGateToPPM g)

theorem compileArithmeticGateToPPM_applyNat_bridge_from_magic
    (sem : GateToPPMSemanticsModel)
    (icx : ArithmeticICXPrimitivePPMObligations sem)
    (mag : MagicInjectionObligations sem)
    (hseq :
      ∀ g₁ g₂ s u,
        sem.gateRel (Gate.seq g₁ g₂) s u ↔
          ∃ t, sem.gateRel g₁ s t ∧ sem.gateRel g₂ t u)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (hreflect :
      PPMReflectsGateRel sem g (compileArithmeticGateToPPM g)) :

theorem shor_arithmetic_full_correctness_transfers_to_PPM_modulo_magic
    (sem : GateToPPMSemanticsModel)
    (icx : ArithmeticICXPrimitivePPMObligations sem)
    (mag : MagicInjectionObligations sem)
    (hseq :
      ∀ g₁ g₂ s u,
        sem.gateRel (Gate.seq g₁ g₂) s u ↔
          ∃ t, sem.gateRel g₁ s t ∧ sem.gateRel g₂ t u)
    (bridge : PPMRefinesApplyNat sem)
    (g : Gate)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool)

inductive MagicPPMCommand : Type
  | base        : PPMCommand → MagicPPMCommand
  | teleportCCX : Nat → Nat → Nat → MagicPPMCommand
  deriving Inhabited

abbrev MagicPPMProgram

def magicPPMCommandMagicTCount : MagicPPMCommand → Nat
  | .base cmd          => ppmCommandMagicTCount cmd
  | .teleportCCX _ _ _ => 1

def magicPPMRequestCount (p : MagicPPMProgram) : Nat

theorem magicPPMRequestCount_nil :
    magicPPMRequestCount [] = 0

theorem magicPPMRequestCount_append (p q : MagicPPMProgram) :
    magicPPMRequestCount (p ++ q)
      = magicPPMRequestCount p + magicPPMRequestCount q

theorem magicPPMRequestCount_teleportCCX (a b c : Nat) :
    magicPPMRequestCount [MagicPPMCommand.teleportCCX a b c] = 1

def teleportCCXRel
    (F : TFactoryContract) (a b c : Nat)
    (s t : MagicBasisPPMState) : Prop

def magicPPMCommandRel
    (F : TFactoryContract) :
    MagicPPMCommand → MagicBasisPPMState → MagicBasisPPMState → Prop
  | .base cmd,          s, t => magicBasisPPMCommandRel F cmd s t
  | .teleportCCX a b c, s, t => teleportCCXRel F a b c s t

inductive MagicPPMProgramRel (F : TFactoryContract) :
    MagicPPMProgram → MagicBasisPPMState → MagicBasisPPMState → Prop
  | nil  (s : MagicBasisPPMState) : MagicPPMProgramRel F [] s s
  | cons {cmd : MagicPPMCommand} {rest : MagicPPMProgram}
         {s t u : MagicBasisPPMState}
         (h1 : magicPPMCommandRel F cmd s t)
         (h2 : MagicPPMProgramRel F rest t u) :
         MagicPPMProgramRel F (cmd :: rest) s u

theorem MagicPPMProgramRel_nil_iff
    (F : TFactoryContract) (s t : MagicBasisPPMState) :
    MagicPPMProgramRel F [] s t ↔ s = t

theorem MagicPPMProgramRel_cons_inv
    (F : TFactoryContract)
    (cmd : MagicPPMCommand) (rest : MagicPPMProgram)
    (s u : MagicBasisPPMState)
    (h : MagicPPMProgramRel F (cmd :: rest) s u) :
    ∃ mid, magicPPMCommandRel F cmd s mid
        ∧ MagicPPMProgramRel F rest mid u

theorem MagicPPMProgramRel_append
    (F : TFactoryContract) (p q : MagicPPMProgram)
    (s u : MagicBasisPPMState) :
    MagicPPMProgramRel F (p ++ q) s u ↔
      ∃ t, MagicPPMProgramRel F p s t ∧ MagicPPMProgramRel F q t u

theorem MagicPPMProgramRel_append_inv
    (F : TFactoryContract) (p q : MagicPPMProgram)
    (s u : MagicBasisPPMState)
    (h : MagicPPMProgramRel F (p ++ q) s u) :
    ∃ mid, MagicPPMProgramRel F p s mid
        ∧ MagicPPMProgramRel F q mid u

theorem MagicPPMProgramRel_base_map_iff
    (F : TFactoryContract) (l : PPMProgram) :
    ∀ (s σ' : MagicBasisPPMState),
      MagicPPMProgramRel F (l.map MagicPPMCommand.base) s σ' ↔
        PPMProgramRel (magicBasisPPMSemanticsModel F) l s σ'

def teleportCCXProgram (a b c : Nat) : MagicPPMProgram

theorem teleportCCXProgram_uses_magic
    (F : TFactoryContract) (a b c : Nat) :
    magicPPMRequestCount (teleportCCXProgram a b c) > 0

theorem teleportCCXProgram_correct_on_success
    (F : TFactoryContract) (a b c : Nat)
    (input : Nat → Bool)
    (s σ' : MagicBasisPPMState)
    (hobs : (magicBasisRefinesApplyNat F).observesBits s input)
    (hrun : MagicPPMProgramRel F (teleportCCXProgram a b c) s σ') :
    (magicBasisRefinesApplyNat F).observesBits σ'
      (Gate.applyNat (Gate.CCX a b c) input)

def compileArithmeticGateToMagicPPM : Gate → MagicPPMProgram
  | Gate.I         =>
      (compileArithmeticGateToPPM Gate.I).map MagicPPMCommand.base
  | Gate.X q       =>
      (compileArithmeticGateToPPM (Gate.X q)).map MagicPPMCommand.base
  | Gate.CX c t    =>
      (compileArithmeticGateToPPM (Gate.CX c t)).map MagicPPMCommand.base
  | Gate.CCX a b c => teleportCCXProgram a b c
  | Gate.seq g₁ g₂ =>
      compileArithmeticGateToMagicPPM g₁
        ++ compileArithmeticGateToMagicPPM g₂

theorem magicBasisPPM_applyNat_sound_ICX_from_observed
    (F : TFactoryContract)
    (g : Gate) (hICX : isICXGate g = true)
    (input : Nat → Bool)
    (s σ' : MagicBasisPPMState)
    (hobs : (magicBasisRefinesApplyNat F).observesBits s input)
    (hrun : PPMProgramRel (magicBasisPPMSemanticsModel F)
              (compileArithmeticGateToPPM g) s σ') :
    (magicBasisRefinesApplyNat F).observesBits σ'
      (Gate.applyNat g input)

theorem compileArithmeticGateToMagicPPM_applyNat_sound_from_observed
    (F : TFactoryContract) :
    ∀ (g : Gate) (input : Nat → Bool)
      (s σ' : MagicBasisPPMState),
      (magicBasisRefinesApplyNat F).observesBits s input →
      MagicPPMProgramRel F (compileArithmeticGateToMagicPPM g) s σ' →
      (magicBasisRefinesApplyNat F).observesBits σ'
        (Gate.applyNat g input)

theorem compileArithmeticGateToMagicPPM_applyNat_sound
    (F : TFactoryContract)
    (g : Gate) (input : Nat → Bool)
    (σ' : MagicBasisPPMState)
    (hrun : MagicPPMProgramRel F
              (compileArithmeticGateToMagicPPM g)
              ((magicBasisRefinesApplyNat F).encodeBits input) σ') :
    (magicBasisRefinesApplyNat F).observesBits σ'
      (Gate.applyNat g input)

theorem shor_arithmetic_full_correctness_transfers_to_magicTeleportPPM
    (F : TFactoryContract)
    (g : Gate)
    (decode : (Nat → Bool) → Nat)
    (input : Nat → Bool) (expected : Nat)
    (σ' : MagicBasisPPMState)
    (hrun : MagicPPMProgramRel F
              (compileArithmeticGateToMagicPPM g)
              ((magicBasisRefinesApplyNat F).encodeBits input) σ')
    (hGateCorrect : decode (Gate.applyNat g input) = expected) :
    ∃ output,
      (magicBasisRefinesApplyNat F).observesBits σ' output

structure TFactoryToffoliObligationV3 (F : TFactoryContract)

def teleportCCX_ToffoliObligationV3 (F : TFactoryContract) :
    TFactoryToffoliObligationV3 F

theorem magicPPMRequestCount_base_map (l : PPMProgram) :
    magicPPMRequestCount (l.map MagicPPMCommand.base)
      = magicRequestCount l

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_I :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM Gate.I) = 0

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_X (q : Nat) :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM (Gate.X q)) = 0

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_CX (c t : Nat) :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM (Gate.CX c t)) = 0

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_CCX (a b c : Nat) :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM (Gate.CCX a b c)) = 1

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_CCX_pos
    (a b c : Nat) :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM (Gate.CCX a b c)) > 0

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_seq (g₁ g₂ : Gate) :
    magicPPMRequestCount (compileArithmeticGateToMagicPPM (Gate.seq g₁ g₂))
      = magicPPMRequestCount (compileArithmeticGateToMagicPPM g₁)
        + magicPPMRequestCount (compileArithmeticGateToMagicPPM g₂)

theorem magicPPMRequestCount_compileArithmeticGateToMagicPPM_ICX :
    ∀ g, isICXGate g = true →
      magicPPMRequestCount (compileArithmeticGateToMagicPPM g) = 0

def toSym : Pauli → Bool × Bool
  | .I => (false, false)
  | .X => (true,  false)
  | .Z => (false, true)
  | .Y => (true,  true)

def ofSym : Bool × Bool → Pauli
  | (false, false) => .I
  | (true,  false) => .X
  | (false, true)  => .Z
  | (true,  true)  => .Y

theorem ofSym_toSym (p : Pauli) : ofSym (toSym p) = p

def cnotConj (c t : Nat) (p : PauliString) : PauliString

example : cnotConj 0 1 ⟨Phase.plus, [Pauli.X, Pauli.I]⟩
    = ⟨Phase.plus, [Pauli.X, Pauli.X]⟩

example : cnotConj 0 1 ⟨Phase.plus, [Pauli.I, Pauli.Z]⟩
    = ⟨Phase.plus, [Pauli.Z, Pauli.Z]⟩

example : cnotConj 0 1 ⟨Phase.plus, [Pauli.Z, Pauli.I]⟩
    = ⟨Phase.plus, [Pauli.Z, Pauli.I]⟩

example : cnotConj 0 1 ⟨Phase.plus, [Pauli.I, Pauli.X]⟩
    = ⟨Phase.plus, [Pauli.I, Pauli.X]⟩

def measGadgetConj (supp : List Nat) (a : Nat) (p : PauliString) : PauliString

theorem measGadget_measures_Z0Z1 :
    measGadgetConj [0, 1] 2 ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.Z]⟩
      = ⟨Phase.plus, [Pauli.Z, Pauli.Z, Pauli.Z]⟩

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

theorem cnot_ctrl (p : PauliString) (i a : Nat) (hi : i < p.ops.length)
    (hci : p.ops.getD i .I = Pauli.I) (hca : p.ops.getD a .I = Pauli.Z) :
    (cnotConj i a p).ops.getD i .I = Pauli.Z

theorem cnot_anc (p : PauliString) (i a : Nat) (ha : a < p.ops.length)
    (hci : p.ops.getD i .I = Pauli.I) (hca : p.ops.getD a .I = Pauli.Z) :
    (cnotConj i a p).ops.getD a .I = Pauli.Z

theorem cnot_other (p : PauliString) (c t j : Nat) (hjc : j ≠ c) (hjt : j ≠ t) :
    (cnotConj c t p).ops.getD j .I = p.ops.getD j .I

theorem cnot_len (p : PauliString) (c t : Nat) :
    (cnotConj c t p).ops.length = p.ops.length

theorem cnot_phase (p : PauliString) (c t : Nat) :
    (cnotConj c t p).phase = p.phase

theorem gadget_len (supp : List Nat) (a : Nat) (p : PauliString) :
    (measGadgetConj supp a p).ops.length = p.ops.length

theorem gadget_phase (supp : List Nat) (a : Nat) (p : PauliString) :
    (measGadgetConj supp a p).phase = p.phase

theorem gadget_untouched (supp : List Nat) (a : Nat) (j : Nat) (hja : j ≠ a) :
    ∀ (p : PauliString), j ∉ supp →
      (measGadgetConj supp a p).ops.getD j .I = p.ops.getD j .I

theorem gadget_anc (supp : List Nat) (a : Nat) :
    ∀ (p : PauliString), a < p.ops.length → a ∉ supp → supp.Nodup →
      p.ops.getD a .I = Pauli.Z → (∀ i ∈ supp, p.ops.getD i .I = Pauli.I) →
      (measGadgetConj supp a p).ops.getD a .I = Pauli.Z

theorem gadget_ctrl (supp : List Nat) (a : Nat) :
    ∀ (p : PauliString), a < p.ops.length → a ∉ supp → supp.Nodup →
      p.ops.getD a .I = Pauli.Z → (∀ i ∈ supp, i < p.ops.length) →
      (∀ i ∈ supp, p.ops.getD i .I = Pauli.I) →
      ∀ k ∈ supp, (measGadgetConj supp a p).ops.getD k .I = Pauli.Z

theorem measGadget_characterization
    (supp : List Nat) (a : Nat) (p : PauliString)
    (ha : a < p.ops.length) (hanc : a ∉ supp) (hnd : supp.Nodup)
    (hca : p.ops.getD a .I = Pauli.Z)
    (hrange : ∀ i ∈ supp, i < p.ops.length)
    (hctrl : ∀ i ∈ supp, p.ops.getD i .I = Pauli.I) :
    (∀ k ∈ supp, (measGadgetConj supp a p).ops.getD k .I = Pauli.Z)
    ∧ (measGadgetConj supp a p).ops.getD a .I = Pauli.Z
    ∧ (∀ j, j ≠ a → j ∉ supp →
        (measGadgetConj supp a p).ops.getD j .I = p.ops.getD j .I)

def xMeasGadgetConj (supp : List Nat) (a : Nat) (p : PauliString) : PauliString

theorem xMeasGadget_measures_X0X1 :
    xMeasGadgetConj [0, 1] 2 ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.X]⟩
      = ⟨Phase.plus, [Pauli.X, Pauli.X, Pauli.X]⟩

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

theorem cnot_x_tgt (p : PauliString) (i a : Nat) (hi : i < p.ops.length)
    (hti : p.ops.getD i .I = Pauli.I) (hca : p.ops.getD a .I = Pauli.X) :
    (cnotConj a i p).ops.getD i .I = Pauli.X

theorem cnot_x_anc (p : PauliString) (i a : Nat) (ha : a < p.ops.length)
    (hti : p.ops.getD i .I = Pauli.I) (hca : p.ops.getD a .I = Pauli.X) :
    (cnotConj a i p).ops.getD a .I = Pauli.X

theorem xgadget_len (supp : List Nat) (a : Nat) (p : PauliString) :
    (xMeasGadgetConj supp a p).ops.length = p.ops.length

theorem xgadget_phase (supp : List Nat) (a : Nat) (p : PauliString) :
    (xMeasGadgetConj supp a p).phase = p.phase

theorem xgadget_untouched (supp : List Nat) (a : Nat) (j : Nat) (hja : j ≠ a) :
    ∀ (p : PauliString), j ∉ supp →
      (xMeasGadgetConj supp a p).ops.getD j .I = p.ops.getD j .I

theorem xgadget_anc (supp : List Nat) (a : Nat) :
    ∀ (p : PauliString), a < p.ops.length → a ∉ supp → supp.Nodup →
      p.ops.getD a .I = Pauli.X → (∀ i ∈ supp, p.ops.getD i .I = Pauli.I) →
      (xMeasGadgetConj supp a p).ops.getD a .I = Pauli.X

theorem xgadget_ctrl (supp : List Nat) (a : Nat) :
    ∀ (p : PauliString), a < p.ops.length → a ∉ supp → supp.Nodup →
      p.ops.getD a .I = Pauli.X → (∀ i ∈ supp, i < p.ops.length) →
      (∀ i ∈ supp, p.ops.getD i .I = Pauli.I) →
      ∀ k ∈ supp, (xMeasGadgetConj supp a p).ops.getD k .I = Pauli.X

theorem xMeasGadget_characterization
    (supp : List Nat) (a : Nat) (p : PauliString)
    (ha : a < p.ops.length) (hanc : a ∉ supp) (hnd : supp.Nodup)
    (hca : p.ops.getD a .I = Pauli.X)
    (hrange : ∀ i ∈ supp, i < p.ops.length)
    (hctrl : ∀ i ∈ supp, p.ops.getD i .I = Pauli.I) :
    (∀ k ∈ supp, (xMeasGadgetConj supp a p).ops.getD k .I = Pauli.X)
    ∧ (xMeasGadgetConj supp a p).ops.getD a .I = Pauli.X
    ∧ (∀ j, j ≠ a → j ∉ supp →
        (xMeasGadgetConj supp a p).ops.getD j .I = p.ops.getD j .I)

def hRes_XZ : PauliString

def hRes_ZX : PauliString

def measXX : PauliString

def measZZ : PauliString

def hGadget (s : StabilizerState) : StabilizerState

def input0     : StabilizerState

def input1     : StabilizerState

def inputPlus  : StabilizerState

def inputMinus : StabilizerState

def outputB (s : StabilizerState) : Option (Phase × Pauli)

theorem hRule_0_gives_plus :
    outputB (hGadget input0) = some (.plus, .X)

theorem hRule_1_gives_minus :
    outputB (hGadget input1) = some (.minus, .X)

theorem hRule_plus_gives_0 :
    outputB (hGadget inputPlus) = some (.plus, .Z)

theorem hRule_minus_gives_1 :
    outputB (hGadget inputMinus) = some (.minus, .Z)

theorem hRule_truth_table :
    outputB (hGadget input0)     = some (.plus,  .X)
  ∧ outputB (hGadget input1)     = some (.minus, .X)
  ∧ outputB (hGadget inputPlus)  = some (.plus,  .Z)
  ∧ outputB (hGadget inputMinus) = some (.minus, .Z)

theorem hGadget_valid_0 :
    StabilizerState.valid (hGadget input0) 3 = true

theorem hGadget_valid_1 :
    StabilizerState.valid (hGadget input1) 3 = true

theorem hGadget_valid_plus :
    StabilizerState.valid (hGadget inputPlus) 3 = true

theorem hGadget_valid_minus :
    StabilizerState.valid (hGadget inputMinus) 3 = true

theorem hGadget_measZZ_mem_input0 :
    measZZ ∈ hGadget input0

def cnotMeasZZ   : PauliString

def cnotMeasXX   : PauliString

def cnotMeasZanc : PauliString

def cnotGadget (s : StabilizerState) : StabilizerState

def cnot_in00 : StabilizerState

def cnot_in01 : StabilizerState

def cnot_in10 : StabilizerState

def cnot_in11 : StabilizerState

theorem cnotRule_00 :
    cnotGadget cnot_in00
      = [⟨.plus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus, [.Z,.Z,.Z]⟩]

theorem cnotRule_01 :
    cnotGadget cnot_in01
      = [⟨.plus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]

theorem cnotRule_10 :
    cnotGadget cnot_in10
      = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus, [.Z,.Z,.Z]⟩]

theorem cnotRule_11 :
    cnotGadget cnot_in11
      = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]

theorem cnotRule_truth_table :
    cnotGadget cnot_in00 = [⟨.plus,  [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus,  [.Z,.Z,.Z]⟩]
  ∧ cnotGadget cnot_in01 = [⟨.plus,  [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]
  ∧ cnotGadget cnot_in10 = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus,  [.Z,.Z,.Z]⟩]
  ∧ cnotGadget cnot_in11 = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]

theorem cnotGadget_valid_00 :
    StabilizerState.valid (cnotGadget cnot_in00) 3 = true

theorem cnotGadget_valid_11 :
    StabilizerState.valid (cnotGadget cnot_in11) 3 = true

def sRes_XY : PauliString

def sRes_ZZ : PauliString

def sGadget (s : StabilizerState) : StabilizerState

def sInput0     : StabilizerState

def sInput1     : StabilizerState

def sInputPlus  : StabilizerState

def sInputMinus : StabilizerState

theorem sRule_0_gives_0 :
    outputB (sGadget sInput0) = some (.plus, .Z)

theorem sRule_1_gives_1 :
    outputB (sGadget sInput1) = some (.minus, .Z)

theorem sRule_plus_gives_plusI :
    outputB (sGadget sInputPlus) = some (.plus, .Y)

theorem sRule_minus_gives_minusI :
    outputB (sGadget sInputMinus) = some (.minus, .Y)

theorem sRule_truth_table :
    outputB (sGadget sInput0)     = some (.plus,  .Z)
  ∧ outputB (sGadget sInput1)     = some (.minus, .Z)
  ∧ outputB (sGadget sInputPlus)  = some (.plus,  .Y)
  ∧ outputB (sGadget sInputMinus) = some (.minus, .Y)

theorem sGadget_valid_0 :
    StabilizerState.valid (sGadget sInput0) 3 = true

theorem sGadget_valid_plus :
    StabilizerState.valid (sGadget sInputPlus) 3 = true

noncomputable def ω : ℂ

theorem ω_pow_four : ω ^ 4 = -1

theorem ω_pow_eight : ω ^ 8 = 1

theorem ω_pow_mod_eight (n : Nat) : ω ^ n = ω ^ (n % 8)

def bitN (x : Bool) : Nat

def tExp (a b c : Bool) : Nat

theorem tExp_mod_eight (a b c : Bool) :
    tExp a b c % 8 = 4 * bitN (a && b && c)

def cczPhase (a b c : Bool) : ℂ

theorem eightT_ccz_phase (a b c : Bool) :
    ω ^ (tExp a b c) = cczPhase a b c

noncomputable def cczMat : Matrix (Fin 8) (Fin 8) ℂ

def aOf (i : Fin 8) : Bool

def bOf (i : Fin 8) : Bool

def cOf (i : Fin 8) : Bool

noncomputable def tDecompMat : Matrix (Fin 8) (Fin 8) ℂ

theorem tDecompMat_eq_cczMat : tDecompMat = cczMat

inductive MagicStateKind
  | T
  | CCZ
  deriving DecidableEq, Repr

instance : Inhabited MagicStateKind

structure AtomicFactorySpec

def max_outputs_in_window (f : AtomicFactorySpec) (window_us : Nat) : Nat

def expected_outputs_in_window
    (f : AtomicFactorySpec) (window_us : Nat) : Nat

def throughput_per_ms_x1000 (f : AtomicFactorySpec) : Nat

def total_latency_for_n_outputs (f : AtomicFactorySpec) (n : Nat) : Nat

structure EightTToCCZSpec

def t_requests_in_window (spec : EightTToCCZSpec) (sched : List SysCall) : Nat

def has_eight_t_requests (spec : EightTToCCZSpec) (sched : List SysCall) : Bool

def window_well_formed (spec : EightTToCCZSpec) : Bool

def downstream_ccz_request
    (spec : EightTToCCZSpec) (sched : List SysCall) : Bool

def verifies (spec : EightTToCCZSpec) (sched : List SysCall) : Bool

inductive MagicFactory
  | atomic   (spec : AtomicFactorySpec)
  | composite (spec : EightTToCCZSpec)
  deriving Repr, Inhabited

def output_zone : MagicFactory → Nat
  | .atomic    s => s.zone_id
  | .composite s => s.ccz_output_zone

def verifies (f : MagicFactory) (sched : List SysCall) : Bool

def cuccaro_n1_cultivation_factory : MagicFactory

def cuccaro_n1_gate3_eight_t : EightTToCCZSpec

def ge2021_ppm_arch : ZonedArch

theorem ge2021_ppm_arch_zone_count :
    ge2021_ppm_arch.zones.length = 2

theorem ge2021_ppm_arch_total :
    ge2021_ppm_arch.total_sites = 200

def ppm_round (start_us : Nat) (decoder_id : Nat) : List SysCall

theorem ppm_round_count (s d : Nat) : (ppm_round s d).length = 5

def ppm_block_syscalls : List SysCall

theorem ppm_block_syscall_count :
    ppm_block_syscalls.length = 16

def ppm_block_wallclock_us : Nat

def ppm_block_peak_physical_qubits : Nat

def ppm_block_total_distinct_qubits : Nat

theorem ppm_block_wallclock_is_derived :
    ppm_block_wallclock_us =
      ppm_block_syscalls.foldl (fun acc sc => Nat.max acc sc.end_us) 0

theorem ppm_block_wallclock_value :
    ppm_block_wallclock_us = 16

theorem ppm_block_peak_physical_qubits_value :
    ppm_block_peak_physical_qubits = 2

theorem ppm_block_total_distinct_qubits_value :
    ppm_block_total_distinct_qubits = 3

theorem ppm_block_capacity_in_arch_ok :
    capacity_in_arch_ok ge2021_ppm_arch ppm_block_syscalls = true

theorem ppm_block_capacity_per_cycle_ok :
    capacity_per_cycle_ok ge2021_ppm_arch ppm_block_syscalls = true

theorem ppm_block_exclusivity_ok :
    exclusivity_ok ppm_block_syscalls = true

theorem ppm_block_feedback_latency_ok :
    feedback_latency_ok ge2021_ppm_arch.t_cycle_us ppm_block_syscalls = true

theorem ppm_block_speed_limit_ok :
    speed_limit_ok ge2021_ppm_arch.v_max_um_per_us (fun _ => 0)
      ppm_block_syscalls = true

theorem ppm_block_window_throughput_ok :
    window_throughput_ok ppm_block_syscalls 1000 1000 = true

theorem ppm_block_decoder_react_ok :
    decoder_react_ok 10 ppm_block_syscalls = true

theorem ppm_block_all_invariants_ok :
    all_invariants_ok ge2021_ppm_arch ppm_block_syscalls 1000 1000 (fun _ => 0) = true

def count_request_fresh_ancilla (sched : List SysCall) : Nat

def count_gate2q (sched : List SysCall) : Nat

def count_measure (sched : List SysCall) : Nat

def count_decode_syndrome (sched : List SysCall) : Nat

def count_pauli_frame_update (sched : List SysCall) : Nat

theorem ppm_block_count_request_fresh_ancilla :
    count_request_fresh_ancilla ppm_block_syscalls = 3

theorem ppm_block_count_gate2q :
    count_gate2q ppm_block_syscalls = 6

theorem ppm_block_count_measure :
    count_measure ppm_block_syscalls = 3

theorem ppm_block_count_decode_syndrome :
    count_decode_syndrome ppm_block_syscalls = 3

theorem ppm_block_count_pauli_frame_update :
    count_pauli_frame_update ppm_block_syscalls = 1

noncomputable def tGadgetOp (b : Bool) : Matrix (Fin 4) (Fin 4) ℂ

noncomputable def injectMagic : Matrix (Fin 4) (Fin 2) ℂ

def extractAnc : Bool → Matrix (Fin 2) (Fin 4) ℂ
  | false => !![1, 0, 0, 0;
                0, 0, 1, 0]
  | true  => !![0, 1, 0, 0;
                0, 0, 0, 1]

theorem injectMagic_apply (ψ : StateVec 1) :
    injectMagic * ψ = ψ ⊗ᵥ tKet

theorem extractAnc_kron (ψd : StateVec 1) (b : Bool) :
    extractAnc b * (ψd ⊗ᵥ tAnc b) = ψd

noncomputable def tKraus (b : Bool) : Matrix (Fin 2) (Fin 2) ℂ

theorem tKraus_eq_smul_U (b : Bool) :
    tKraus b = tBorn b • tMat

theorem normSq_ω : Complex.normSq ω = 1

theorem tBorn_normSq_sum :
    Complex.normSq (tBorn false) + Complex.normSq (tBorn true) = 1

noncomputable def tChannel (ρ : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 2) (Fin 2) ℂ

noncomputable def tUnitaryChannel (ρ : Matrix (Fin 2) (Fin 2) ℂ) :
    Matrix (Fin 2) (Fin 2) ℂ

theorem tChannel_eq_unitaryChannel (ρ : Matrix (Fin 2) (Fin 2) ℂ) :
    tChannel ρ = tUnitaryChannel ρ

noncomputable def cczGadgetOp000 : Matrix (Fin 64) (Fin 64) ℂ

noncomputable def injectCCZ : Matrix (Fin 64) (Fin 8) ℂ

noncomputable def extractCCZ000 : Matrix (Fin 8) (Fin 64) ℂ

theorem injectCCZ_apply (ψ : StateVec 3) :
    injectCCZ * ψ = ψ ⊗ᵥ cczKet

theorem extractCCZ000_kron (d : StateVec 3) :
    extractCCZ000 * (d ⊗ᵥ (basisState 0 : StateVec 3)) = d

noncomputable def cczKraus000 : Matrix (Fin 8) (Fin 8) ℂ

noncomputable def cczBorn000 : ℂ

theorem cczKraus000_eq_smul_U :
    cczKraus000 = cczBorn000 • cczMat

noncomputable def unitaryChannel {n : Nat} (U ρ : Matrix (Fin n) (Fin n) ℂ) :
    Matrix (Fin n) (Fin n) ℂ

theorem unitaryChannel_comp {n : Nat} (U₁ U₂ ρ : Matrix (Fin n) (Fin n) ℂ) :
    unitaryChannel U₂ (unitaryChannel U₁ ρ) = unitaryChannel (U₂ * U₁) ρ

theorem tChannel_eq_unitaryChannel' (ρ : Matrix (Fin 2) (Fin 2) ℂ) :
    tChannel ρ = unitaryChannel tMat ρ

def toffCount : Gate → Nat
  | .I => 0
  | .X _ => 0
  | .CX _ _ => 0
  | .CCX _ _ _ => 1
  | .seq g₁ g₂ => toffCount g₁ + toffCount g₂

theorem tcount_eq_seven_mul_toffCount (g : Gate) : tcount g = 7 * toffCount g

def gateToHL : Gate → List HLGate
  | .I => []
  | .X q => [.X q]
  | .CX c t => [.CNOT c t]
  | .CCX a b t => [.H t, .CCZ a b t, .H t]
  | .seq g₁ g₂ => gateToHL g₁ ++ gateToHL g₂

theorem cczMagic_sum_gateToHL (g : Gate) :
    ((gateToHL g).map gateCCZMagic).sum = toffCount g

theorem meas_sum_gateToHL (g : Gate) :
    ((gateToHL g).map gateMeas).sum = 3 * toffCount g

theorem numCCZMagic_circuitToPPM_gateToHL (na : Nat) (g : Gate) :
    numCCZMagic (circuitToPPM na (gateToHL g)) = toffCount g

theorem numMeas_circuitToPPM_gateToHL (na : Nat) (g : Gate) :
    numMeas (circuitToPPM na (gateToHL g)) = 3 * toffCount g

theorem toffCount_gidney_adder (n : Nat) :
    toffCount (gidney_adder_full_faithful_no_measurement (n + 2)) = 2 * (n + 2)

theorem verified_adder_ppm_CCZMagic (na n : Nat) :
    numCCZMagic (circuitToPPM na (gateToHL (gidney_adder_full_faithful_no_measurement (n + 2))))
      = 2 * (n + 2)

theorem verified_adder_ppm_Meas (na n : Nat) :
    numMeas (circuitToPPM na (gateToHL (gidney_adder_full_faithful_no_measurement (n + 2))))
      = 6 * (n + 2)

theorem verified_adder_end_to_end
    (n a b : Nat) (hn : 1 < n + 2) (ha : a < 2 ^ (n + 2)) (hb : b < 2 ^ (n + 2)) :
    (∀ i, i < n + 2 →
        Gate.applyNat (gidney_adder_full_faithful_no_measurement (n + 2))
          (adder_input_F (n + 2) a b) (target_idx i)
        = adder_sum_bit_classical a b i)
    ∧ numCCZMagic (circuitToPPM 0
          (gateToHL (gidney_adder_full_faithful_no_measurement (n + 2)))) = 2 * (n + 2)
    ∧ numMeas (circuitToPPM 0
          (gateToHL (gidney_adder_full_faithful_no_measurement (n + 2)))) = 6 * (n + 2)

def GidneyAND_forward (ctrl tgt anc : Nat) : Gate

theorem tcount_GidneyAND_forward (ctrl tgt anc : Nat) :
    tcount (GidneyAND_forward ctrl tgt anc) = 7

theorem gcount_GidneyAND_forward (ctrl tgt anc : Nat) :
    gcount (GidneyAND_forward ctrl tgt anc) = 1

structure GidneyAND_reverse

def GidneyAND_reverse.ppm (r : GidneyAND_reverse) : PPM

def GidneyAND_reverse_tcount (_r : GidneyAND_reverse) : Nat

theorem GidneyAND_reverse_tcount_eq_zero (r : GidneyAND_reverse) :
    GidneyAND_reverse_tcount r = 0

def GidneyAND_cycle_tcount (ctrl tgt anc : Nat) (r : GidneyAND_reverse) : Nat

theorem GidneyAND_cycle_tcount_eq_seven
    (ctrl tgt anc : Nat) (r : GidneyAND_reverse) :
    GidneyAND_cycle_tcount ctrl tgt anc r = 7

example :
    let r : GidneyAND_reverse

abbrev LogicalQubitId

abbrev LogicalPatchId

abbrev PhysicalSiteId

abbrev DecoderId

abbrev FactoryPortId

structure PPMSpec

structure QECGadgetSpec

def PPMSpec.ofPauliMeasurementClaim
    (claim : PauliMeasurementClaim)
    (rounds distance : Nat) : PPMSpec

def QECGadgetSpec.ofPPMGadget
    (ppm : PPMSpec) (gadget : PPMGadget)
    (syndromeRounds : Nat) (decoder : DecoderId)
    (usesPauliFrame : Bool) : QECGadgetSpec

structure PPMToSystemLoweringCertificate
    (models : SystemModels)

structure VerifiedBackendBlock (models : SystemModels)

theorem VerifiedBackendBlock.strict_invariants_ok
    (models : SystemModels) (b : VerifiedBackendBlock models) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        b.schedule.expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

structure VerifiedPPMBlock (models : SystemModels)

theorem VerifiedPPMBlock.system_invariants_ok
    (models : SystemModels) (b : VerifiedPPMBlock models) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        b.backend.schedule.expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

structure ShorResourceVerificationInterface
    (models : SystemModels)

theorem ShorResourceVerificationInterface.system_invariants_ok
    (models : SystemModels)
    (s : ShorResourceVerificationInterface models) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        s.schedule.expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

def Pauli.toMatrix : Pauli → Matrix (Fin 2) (Fin 2) ℂ
  | .I => !![1, 0; 0, 1]
  | .X => !![0, 1; 1, 0]
  | .Y => !![0, -Complex.I; Complex.I, 0]
  | .Z => !![1, 0; 0, -1]

example : Pauli.toMatrix .I = !![(1:ℂ), 0; 0, 1]

example : (Pauli.toMatrix .X) 0 1 = 1

example : (Pauli.toMatrix .X) 1 0 = 1

example :
    (Pauli.toMatrix .Z) 0 0 = 1
    ∧ (Pauli.toMatrix .Z) 1 1 = -1

example :
    (Pauli.toMatrix .Y) 0 1 = -Complex.I
    ∧ (Pauli.toMatrix .Y) 1 0 = Complex.I

example : (Pauli.toMatrix .X * Pauli.toMatrix .X) 0 0 = 1

example : (Pauli.toMatrix .X * Pauli.toMatrix .X) 1 1 = 1

example : (Pauli.toMatrix .X * Pauli.toMatrix .X) 0 1 = 0

example : (Pauli.toMatrix .Z * Pauli.toMatrix .Z) 0 0 = 1

example : (Pauli.toMatrix .Z * Pauli.toMatrix .Z) 1 1 = 1

example : (Pauli.toMatrix .X * Pauli.toMatrix .Z) 0 1 = -1

example : (Pauli.toMatrix .X * Pauli.toMatrix .Z) 1 0 = 1

example : (Pauli.toMatrix .Z * Pauli.toMatrix .X) 0 1 = 1

example : (Pauli.toMatrix .Y * Pauli.toMatrix .Y) 0 0 = 1

example : (Pauli.toMatrix .Y * Pauli.toMatrix .Y) 1 1 = 1

example : (Pauli.toMatrix .Y * Pauli.toMatrix .Y) 0 1 = 0

example : (Pauli.toMatrix .Y * Pauli.toMatrix .X) 0 0 = -Complex.I

example : (Pauli.toMatrix .X * Pauli.toMatrix .Y) 0 0 = Complex.I

example : (Pauli.toMatrix .Y * Pauli.toMatrix .Z) 0 0 = 0

example : (Pauli.toMatrix .Y * Pauli.toMatrix .Z) 0 1 = Complex.I

noncomputable def PauliString.toMatrix : (P : PauliString) →
    Matrix (Fin (2 ^ P.length)) (Fin (2 ^ P.length)) ℂ
  | [] => 1
  | p :: ps =>
    Matrix.reindex finProdFinEquiv finProdFinEquiv
      (Matrix.kroneckerMap (· * ·) (PauliString.toMatrix ps) p.toMatrix)

theorem PauliString.toMatrix_nil :
    PauliString.toMatrix [] = (1 : Matrix (Fin 1) (Fin 1) ℂ)

theorem PauliString.toMatrix_cons (p : Pauli) (ps : PauliString) :
    PauliString.toMatrix (p :: ps)
      = Matrix.reindex finProdFinEquiv finProdFinEquiv
          (Matrix.kroneckerMap (· * ·) (PauliString.toMatrix ps) p.toMatrix)

theorem Pauli.toMatrix_I_eq_one :
    Pauli.toMatrix Pauli.I = (1 : Matrix (Fin 2) (Fin 2) ℂ)

theorem PauliString.toMatrix_replicate_I (n : Nat) :
    PauliString.toMatrix (List.replicate n Pauli.I) = 1

theorem Pauli.toMatrix_mul_self (p : Pauli) :
    Pauli.toMatrix p * Pauli.toMatrix p = (1 : Matrix (Fin 2) (Fin 2) ℂ)

theorem PauliString.toMatrix_mul_self (P : PauliString) :
    P.toMatrix * P.toMatrix = 1

theorem Pauli.toMatrix_comm_of_commutes (p q : Pauli)
    (h : commutes p q = true) :
    Pauli.toMatrix p * Pauli.toMatrix q
      = Pauli.toMatrix q * Pauli.toMatrix p

theorem PauliString.toMatrix_projector_idem_aux (P : PauliString) :
    (1 + P.toMatrix) * (1 + P.toMatrix) = 2 • (1 + P.toMatrix)

theorem PauliString.toMatrix_projector_idem_aux_minus (P : PauliString) :
    (1 - P.toMatrix) * (1 - P.toMatrix) = 2 • (1 - P.toMatrix)

theorem PauliString.toMatrix_projector_orthogonality (P : PauliString) :
    (1 + P.toMatrix) * (1 - P.toMatrix) = 0

theorem PauliString.toMatrix_projector_resolution (P : PauliString) :
    (1 + P.toMatrix) + (1 - P.toMatrix)
      = (2 • 1 : Matrix (Fin (2^P.length)) (Fin (2^P.length)) ℂ)

inductive PointwisePauliCommutes : PauliString → PauliString → Prop
  | nil : PointwisePauliCommutes [] []
  | cons : ∀ {p q : Pauli} {ps qs : PauliString},
      Pauli.commutes p q = true → PointwisePauliCommutes ps qs →
      PointwisePauliCommutes (p :: ps) (q :: qs)

theorem PointwisePauliCommutes.length_eq :
    ∀ {P Q : PauliString}, PointwisePauliCommutes P Q → P.length = Q.length
  | _, _, .nil => rfl
  | _, _, .cons _ h => congrArg (· + 1) (PointwisePauliCommutes.length_eq h)

theorem Pauli.commutes_comm (p q : Pauli) :
    Pauli.commutes p q = Pauli.commutes q p

theorem PointwisePauliCommutes.self :
    ∀ (P : PauliString), PointwisePauliCommutes P P
  | [] => .nil
  | (p :: ps) =>
      .cons (Pauli.commutes_self p) (PointwisePauliCommutes.self ps)

theorem PointwisePauliCommutes.symm :
    ∀ {P Q : PauliString}, PointwisePauliCommutes P Q →
                            PointwisePauliCommutes Q P
  | _, _, .nil => .nil
  | _, _, .cons hpq h =>
      .cons (by rw [Pauli.commutes_comm]; exact hpq)
            (PointwisePauliCommutes.symm h)

theorem PointwisePauliCommutes.replicate_I_left :
    ∀ (Q : PauliString),
    PointwisePauliCommutes (List.replicate Q.length Pauli.I) Q
  | [] => by exact PointwisePauliCommutes.nil
  | (q :: qs) =>

theorem PointwisePauliCommutes.replicate_I_right :
    ∀ (P : PauliString),
    PointwisePauliCommutes P (List.replicate P.length Pauli.I)
  | [] => by exact PointwisePauliCommutes.nil
  | (p :: ps) =>

theorem PointwisePauliCommutes.append :
    ∀ {P₁ Q₁ P₂ Q₂ : PauliString},
    PointwisePauliCommutes P₁ Q₁ → PointwisePauliCommutes P₂ Q₂ →
    PointwisePauliCommutes (P₁ ++ P₂) (Q₁ ++ Q₂)
  | _, _, _, _, .nil, h₂ => h₂
  | _, _, _, _, .cons hpq h₁, h₂ =>

theorem PointwisePauliCommutes.disjoint_left_right (P Q : PauliString) :
    PointwisePauliCommutes
      (P ++ List.replicate Q.length Pauli.I)
      (List.replicate P.length Pauli.I ++ Q)

theorem PauliString.commutes_of_pointwise :
    ∀ {P Q : PauliString}, PointwisePauliCommutes P Q →
    PauliString.commutes P Q = true
  | _, _, .nil => rfl
  | _, _, .cons hpq h =>

theorem Code4Code4_XXXX_L_pointwise_commutes_ZZZZ_R :
    PointwisePauliCommutes Code4Code4_XXXX_L Code4Code4_ZZZZ_R

theorem Code4Code4_XXXX_L_pointwise_commutes_XXXX_R :
    PointwisePauliCommutes Code4Code4_XXXX_L Code4Code4_XXXX_R

theorem Code4Code4_ZZZZ_L_pointwise_commutes_XXXX_R :
    PointwisePauliCommutes Code4Code4_ZZZZ_L Code4Code4_XXXX_R

theorem Code4Code4_ZZZZ_L_pointwise_commutes_ZZZZ_R :
    PointwisePauliCommutes Code4Code4_ZZZZ_L Code4Code4_ZZZZ_R

private lemma toMatrix_cons_cast {q : Pauli} {qs ps : PauliString}
    (hsym : qs.length = ps.length) :
    (congrArg (· + 1) hsym ▸ PauliString.toMatrix (q :: qs)
      : Matrix (Fin (2^(ps.length + 1))) (Fin (2^(ps.length + 1))) ℂ)
      = Matrix.reindex finProdFinEquiv finProdFinEquiv
          (Matrix.kroneckerMap (· * ·)
            (hsym ▸ PauliString.toMatrix qs
              : Matrix (Fin (2^ps.length)) (Fin (2^ps.length)) ℂ)
            q.toMatrix)

theorem PauliString.toMatrix_comm_of_pointwise :
    ∀ {P Q : PauliString} (h : PointwisePauliCommutes P Q),
      PauliString.toMatrix P *
          (h.length_eq.symm ▸ PauliString.toMatrix Q
            : Matrix (Fin (2^P.length)) _ ℂ)
        = (h.length_eq.symm ▸ PauliString.toMatrix Q
            : Matrix (Fin (2^P.length)) _ ℂ) * PauliString.toMatrix P
  | [], [], _ => by simp [PauliString.toMatrix]
  | (p :: ps), (q :: qs), .cons hpq h_tail =>

abbrev JointStateVector

def in_Code4Code4_codespace (_v : JointStateVector) : Prop

structure LogicalState_4_2_2_pair

example (v : JointStateVector) : in_Code4Code4_codespace v

def LogicalState_4_2_2_pair.mk_trivial (v : JointStateVector) :
    LogicalState_4_2_2_pair

noncomputable def Code4Code4_CNOT_L1L_R1_matrix :
    Matrix (Fin (2^8)) (Fin (2^8)) ℂ

noncomputable def apply_logical_gate (g : Framework.Gate)
    (s : LogicalState_4_2_2_pair) : LogicalState_4_2_2_pair

inductive MeasurementOutcome
  | plus    -- +1 eigenvalue
  | minus   -- -1 eigenvalue
  deriving DecidableEq, Repr

def MeasurementOutcome.toComplex : MeasurementOutcome → ℂ
  | .plus  => 1
  | .minus => -1

def outcome_product : List MeasurementOutcome → ℂ
  | [] => 1
  | x :: xs => x.toComplex * outcome_product xs

example : MeasurementOutcome.plus.toComplex = 1

example : MeasurementOutcome.minus.toComplex = -1

example : outcome_product [] = 1

example :
    outcome_product [.plus, .plus, .plus, .plus, .plus] = 1

example :
    outcome_product [.plus, .minus, .plus, .plus, .plus] = -1

example :
    outcome_product [.minus, .plus, .minus, .plus, .plus] = 1

def apply_PPM (s : LogicalState_4_2_2_pair) (_ppm : PPM) :
    MeasurementOutcome × LogicalState_4_2_2_pair

noncomputable def apply_PPM_projector
    (s : LogicalState_4_2_2_pair)
    (P : Matrix (Fin (2^8)) (Fin (2^8)) ℂ)
    (outcome : MeasurementOutcome) :
    LogicalState_4_2_2_pair

example : (MeasurementOutcome.plus = MeasurementOutcome.minus) = False

example (s : LogicalState_4_2_2_pair) (ppm : PPM) :
    let result

def Code4Code4_CNOT_correction_fn (_outcomes : List MeasurementOutcome) :
    PauliString

def apply_schedule (s : LogicalState_4_2_2_pair) :
    List PPM → List MeasurementOutcome × LogicalState_4_2_2_pair
  | [] => ([], s)
  | ppm :: rest =>
      let (out_head, s_after_head)

def apply_surgery_with_corrections (s : LogicalState_4_2_2_pair)
    (schedule : List PPM)
    (_correction_fn : List MeasurementOutcome → PauliString) :
    LogicalState_4_2_2_pair

example (s : LogicalState_4_2_2_pair) :
    (apply_schedule s Code4Code4_CNOT_surgery_schedule).1.length = 5

example (outs : List MeasurementOutcome) :
    Code4Code4_CNOT_correction_fn outs = PauliString.id 8

def logical_CNOT_L1_R1 (s : LogicalState_4_2_2_pair) : LogicalState_4_2_2_pair

theorem Code4Code4_surgery_implements_logical_CNOT
    (s : LogicalState_4_2_2_pair) :
    apply_surgery_with_corrections s
        Code4Code4_CNOT_surgery_schedule
        Code4Code4_CNOT_correction_fn
      = logical_CNOT_L1_R1 s

def MagicRealizes {dD dA : Nat}
    (G : Square (dD + dA)) (magic : StateVec dA) (U : Square dD) : Prop

noncomputable def tMat : Matrix (Fin 2) (Fin 2) ℂ

theorem tMat_apply (ψ : StateVec 1) : tMat * ψ = Tdata ψ

theorem tGadget_magic_realizes (b : Bool) :
    MagicRealizes (dD

theorem magic_realizes_chain {dD dA1 dA2 : Nat}
    {G1 : Square (dD + dA1)} {m1 : StateVec dA1} {U1 : Square dD}
    {G2 : Square (dD + dA2)} {m2 : StateVec dA2} {U2 : Square dD}
    (h1 : MagicRealizes G1 m1 U1) (h2 : MagicRealizes G2 m2 U2) (ψ : StateVec dD) :
    ∃ (anc1 : StateVec dA1) (anc2 : StateVec dA2) (c1 c2 : ℂ),
      G1 * (ψ ⊗ᵥ m1) = c1 • ((U1 * ψ) ⊗ᵥ anc1)
      ∧ G2 * ((U1 * ψ) ⊗ᵥ m2) = c2 • (((U2 * U1) * ψ) ⊗ᵥ anc2)

noncomputable def tKet : StateVec 1

noncomputable def Tdata (ψ : StateVec 1) : StateVec 1

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

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

noncomputable def Shigh : Matrix (Fin 4) (Fin 4) ℂ

theorem ω_sq : ω ^ 2 = Complex.I

theorem t_teleport_outcome_0 (ψ : StateVec 1) :
    projLow0 * (cnotMatrix * (ψ ⊗ᵥ tKet))
      = (1 / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1))

theorem t_teleport_outcome_1 (ψ : StateVec 1) :
    Shigh * (projLow1 * (cnotMatrix * (ψ ⊗ᵥ tKet)))
      = (ω / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1))

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

theorem toffCount_sqir_modmult_const_gate_le (bits N a : Nat) :
    toffCount (sqir_modmult_const_gate bits N a) ≤ 8 * bits ^ 2

theorem numCCZMagic_sqir_modmult_const_gate_le (na bits N a : Nat) :
    numCCZMagic (circuitToPPM na (gateToHL (sqir_modmult_const_gate bits N a))) ≤ 8 * bits ^ 2

theorem verified_modmult_end_to_end
    (bits N a m : Nat) (hbits : 1 ≤ bits) (hN_pos : 0 < N)
    (hN : N ≤ 2 ^ bits) (hN2 : 2 * N ≤ 2 ^ bits) (hm : m < 2 ^ bits) :
    cuccaro_target_val bits 2
        (Gate.applyNat (sqir_modmult_const_gate bits N a) (sqir_mult_input_F bits m 0))
      = (a * m) % N
    ∧ numCCZMagic (circuitToPPM 0
          (gateToHL (sqir_modmult_const_gate bits N a))) ≤ 8 * bits ^ 2

theorem shor2048_per_modmult_CCZMagic_le (na N a : Nat) :
    numCCZMagic (circuitToPPM na (gateToHL (sqir_modmult_const_gate 2048 N a))) ≤ 33554432

example : 4096 * 33554432 = 137438953472

theorem toffCount_shorModExp (bits N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    toffCount (shorModExp bits N a) = 16 * bits ^ 3

theorem numCCZMagic_shorModExp (na bits N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    numCCZMagic (circuitToPPM na (gateToHL (shorModExp bits N a))) = 16 * bits ^ 3

theorem numMeas_shorModExp (na bits N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    numMeas (circuitToPPM na (gateToHL (shorModExp bits N a))) = 48 * bits ^ 3

theorem shor2048_CCZMagic_outOfPlaceModel (na N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    numCCZMagic (circuitToPPM na (gateToHL (shorModExp 2048 N a))) = 137438953472

theorem shor2048_Meas_outOfPlaceModel (na N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    numMeas (circuitToPPM na (gateToHL (shorModExp 2048 N a))) = 412316860416

theorem toffCount_sqir_modmult_MCP_gate (bits N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    toffCount (sqir_modmult_MCP_gate bits N a ainv) = 16 * bits ^ 2

theorem verified_MCP_oracle_end_to_end
    (bits N a ainv : Nat)
    (hbits : 1 ≤ bits) (hN_pos : 0 < N) (hN : N ≤ 2 ^ bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hodd : Odd N) (h1 : 1 < N) (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (h_inv : a * ainv % N = 1) :
    FormalRV.SQIRPort.MultiplyCircuitProperty a N bits (sqir_modmult_rev_anc bits)
        (Gate.toUCom (sqir_total_dim bits) (sqir_modmult_MCP_gate bits N a ainv))
    ∧ numCCZMagic (circuitToPPM 0 (gateToHL (sqir_modmult_MCP_gate bits N a ainv)))
        = 16 * bits ^ 2

theorem toffCount_shorModExpVerified (bits N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    toffCount (shorModExpVerified bits N a ainv) = 32 * bits ^ 3

theorem numCCZMagic_shorModExpVerified (na bits N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    numCCZMagic (circuitToPPM na (gateToHL (shorModExpVerified bits N a ainv))) = 32 * bits ^ 3

theorem shor2048_CCZMagic_verified (na N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    numCCZMagic (circuitToPPM na (gateToHL (shorModExpVerified 2048 N a ainv))) = 274877906944

inductive Pauli

inductive Phase

def Phase.mul : Phase → Phase → Phase
  | .pos, p => p
  | p, .pos => p
  | .neg, .neg => .pos
  | .neg, .posI => .negI
  | .neg, .negI => .posI
  | .posI, .neg => .negI
  | .posI, .posI => .neg
  | .posI, .negI => .pos
  | .negI, .neg => .posI
  | .negI, .posI => .pos
  | .negI, .negI => .neg

def mul : Pauli → Pauli → Phase × Pauli
  | .I, p => (.pos, p)
  | p, .I => (.pos, p)
  | .X, .X => (.pos, .I)
  | .Y, .Y => (.pos, .I)
  | .Z, .Z => (.pos, .I)
  | .X, .Y => (.posI, .Z)
  | .Y, .X => (.negI, .Z)
  | .Y, .Z => (.posI, .X)
  | .Z, .Y => (.negI, .X)
  | .Z, .X => (.posI, .Y)
  | .X, .Z => (.negI, .Y)

example : mul .X .X = (.pos, .I)

example : mul .X .Y = (.posI, .Z)

example : mul .Y .X = (.negI, .Z)

example : mul .Z .X = (.posI, .Y)

example : (mul .X .Y).2 = (mul .Y .X).2

example : (mul .X .Y).1 = .posI ∧ (mul .Y .X).1 = .negI

def commutes (p q : Pauli) : Bool

def anticommutes (p q : Pauli) : Bool

theorem commutes_self (p : Pauli) : commutes p p = true

theorem commutes_I_left (p : Pauli) : commutes .I p = true

theorem commutes_I_right (p : Pauli) : commutes p .I = true

example : anticommutes .X .Y = true

example : anticommutes .Y .Z = true

example : anticommutes .X .Z = true

example : commutes .X .Y = false

theorem distinct_nonI_anticommute :
    ∀ p q : Pauli, p ≠ q → p ≠ .I → q ≠ .I → anticommutes p q = true

abbrev PauliString

def PauliString.id (n : Nat) : PauliString

def PauliString.singleX (n i : Nat) : PauliString

example : PauliString.id 3 = [.I, .I, .I]

example : PauliString.singleX 3 1 = [.I, .X, .I]

inductive PPM_outcome

example : (PPM_outcome.zero = PPM_outcome.one) = False

structure PPM

def PauliString.mul : PauliString → PauliString → Pauli.Phase × PauliString
  | [], _ => (.pos, [])
  | _, [] => (.pos, [])
  | p :: ps, q :: qs =>
      let (φ_head, r_head)

example : PauliString.mul [.I, .I] [.I, .I] = (.pos, [.I, .I])

example : PauliString.mul [.X, .Y] [.Y, .X] = (.pos, [.Z, .Z])

example : PauliString.mul [.X, .X, .X] [.X, .X, .X] = (.pos, [.I, .I, .I])

example : PauliString.mul [.X, .Z] [.Z, .X] = (.pos, [.Y, .Y])

def PauliString.commutes (A B : PauliString) : Bool

example : PauliString.commutes [.I, .I] [.I, .I] = true

example : PauliString.commutes [.X, .X] [.Z, .Z] = true

example : PauliString.commutes [.X, .X, .X] [.Z, .Z, .Z] = false

example : PauliString.commutes [.X, .Y] [.Y, .X] = true

example : PauliString.commutes [.X, .I] [.Z, .I] = false

example : PauliString.commutes [.X, .X, .X, .X] [.Z, .Z, .Z, .Z] = true

def Code4_S1 : PauliString

def Code4_S2 : PauliString

def Code4_stabilizers : List PauliString

example : Code4_S1.length = 4 ∧ Code4_S2.length = 4

example : PauliString.commutes Code4_S1 Code4_S1 = true

example : PauliString.commutes Code4_S2 Code4_S2 = true

theorem Code4_stabilizers_commute :
    PauliString.commutes Code4_S1 Code4_S2 = true

theorem Code4_stabilizers_commute_symm :
    PauliString.commutes Code4_S2 Code4_S1 = true

def Code4_S3 : PauliString

example :
    PauliString.mul Code4_S1 Code4_S2 = (Pauli.Phase.pos, Code4_S3)

example : PauliString.commutes Code4_S3 Code4_S3 = true

example :
    PauliString.commutes Code4_S3 Code4_S1 = true
    ∧ PauliString.commutes Code4_S3 Code4_S2 = true

def Pauli.toSymplectic : Pauli → Bool × Bool
  | .I => (false, false)
  | .X => (true,  false)
  | .Y => (true,  true)
  | .Z => (false, true)

def PauliString.toSymplectic (P : PauliString) : List Bool

def parity_check_matrix (stabilizers : List PauliString) : List (List Bool)

example :
    PauliString.toSymplectic Code4_S1
      = [true, true, true, true, false, false, false, false]

example :
    PauliString.toSymplectic Code4_S2
      = [false, false, false, false, true, true, true, true]

example :
    parity_check_matrix Code4_stabilizers
      = [[true, true, true, true, false, false, false, false],
         [false, false, false, false, true, true, true, true]]

example :
    ∀ row ∈ parity_check_matrix Code4_stabilizers, row.length = 8

def Code4Code4_merge_CNOT_PPM : PPM

def Code4Code4_split_L_X_PPM : PPM

def Code4Code4_split_R_Z_PPM : PPM

def Code4Code4_check_L_Z_PPM : PPM

def Code4Code4_check_R_X_PPM : PPM

def Code4Code4_CNOT_surgery_schedule : List PPM

theorem Code4Code4_CNOT_surgery_count :
    Code4Code4_CNOT_surgery_schedule.length = 5

theorem PauliString.commutes_self (P : PauliString) :
    PauliString.commutes P P = true

theorem PauliString.commutes_symm (A B : PauliString) :
    PauliString.commutes A B = PauliString.commutes B A

theorem PauliString.mul_id_left_phase_pos (n : Nat) (P : PauliString) :
    (PauliString.mul (PauliString.id n) P).1 = Pauli.Phase.pos

theorem PauliString.commutes_I_left (n : Nat) (P : PauliString) :
    PauliString.commutes (PauliString.id n) P = true

theorem PauliString.commutes_I_right (n : Nat) (P : PauliString) :
    PauliString.commutes P (PauliString.id n) = true

theorem PauliString.id_commutes_with_all (n : Nat) (stabs : List PauliString) :
    ∀ S ∈ stabs, PauliString.commutes (PauliString.id n) S = true

theorem PauliString.mul_id_left_eq : ∀ (P : PauliString),
    PauliString.mul (PauliString.id P.length) P = (Pauli.Phase.pos, P)
  | [] => rfl
  | q :: ps =>

theorem PauliString.mul_id_right_eq : ∀ (P : PauliString),
    PauliString.mul P (PauliString.id P.length) = (Pauli.Phase.pos, P)
  | [] => rfl
  | q :: ps =>

theorem PauliString.length_id (n : Nat) :
    (PauliString.id n).length = n

theorem PauliString.length_singleX (n i : Nat) :
    (PauliString.singleX n i).length = n

theorem PauliString.length_mul (P Q : PauliString) :
    (PauliString.mul P Q).2.length = min P.length Q.length

theorem PauliString.length_mul_of_eq_length (P Q : PauliString)
    (h : P.length = Q.length) :
    (PauliString.mul P Q).2.length = P.length

theorem PauliString.length_mul_singleX (n i : Nat) (P : PauliString)
    (h : P.length = n) :
    (PauliString.mul P (PauliString.singleX n i)).2.length = n

theorem PauliString.toSymplectic_length (P : PauliString) :
    P.toSymplectic.length = 2 * P.length

theorem PauliString.toSymplectic_id (n : Nat) :
    (PauliString.id n).toSymplectic = List.replicate (2 * n) false

theorem parity_check_matrix_length (stabs : List PauliString) :
    (parity_check_matrix stabs).length = stabs.length

example :
    ∀ ppm ∈ Code4Code4_CNOT_surgery_schedule, ppm.measure.length = 8

example : PauliString.commutes (PauliString.id 4) Code4_S1 = true

example : PauliString.commutes (PauliString.id 4) Code4_S2 = true

example : PauliString.commutes (PauliString.id 4) (PauliString.id 4) = true

example : PauliString.commutes (PauliString.id 4) [.Y, .Y, .Y, .Y] = true

example :
    PauliString.commutes (PauliString.id 4) (PauliString.singleX 4 0) = true
    ∧ PauliString.commutes (PauliString.id 4) (PauliString.singleX 4 1) = true
    ∧ PauliString.commutes (PauliString.id 4) (PauliString.singleX 4 2) = true
    ∧ PauliString.commutes (PauliString.id 4) (PauliString.singleX 4 3) = true

def PPM.commutes_with (ppm : PPM) (S : PauliString) : Bool

def Code4Code4_XXXX_L : PauliString

def Code4Code4_ZZZZ_L : PauliString

def Code4Code4_XXXX_R : PauliString

def Code4Code4_ZZZZ_R : PauliString

def Code4Code4_stabilizers : List PauliString

example :
    Code4Code4_merge_CNOT_PPM.commutes_with Code4Code4_XXXX_L = true
    ∧ Code4Code4_merge_CNOT_PPM.commutes_with Code4Code4_ZZZZ_L = true
    ∧ Code4Code4_merge_CNOT_PPM.commutes_with Code4Code4_XXXX_R = true
    ∧ Code4Code4_merge_CNOT_PPM.commutes_with Code4Code4_ZZZZ_R = true

example :
    Code4Code4_split_L_X_PPM.commutes_with Code4Code4_XXXX_L = true
    ∧ Code4Code4_split_L_X_PPM.commutes_with Code4Code4_ZZZZ_L = true  -- 4 anti-comm = even = comm
    ∧ Code4Code4_split_L_X_PPM.commutes_with Code4Code4_XXXX_R = true
    ∧ Code4Code4_split_L_X_PPM.commutes_with Code4Code4_ZZZZ_R = true

example :
    ∀ ppm ∈ Code4Code4_CNOT_surgery_schedule,
    ∀ S ∈ Code4Code4_stabilizers, ppm.commutes_with S = true

def Code4_X_L1 : PauliString

def Code4_X_L2 : PauliString

def Code4_Z_L1 : PauliString

def Code4_Z_L2 : PauliString

example :
    PauliString.commutes Code4_X_L1 Code4_S1 = true
    ∧ PauliString.commutes Code4_X_L1 Code4_S2 = true
    ∧ PauliString.commutes Code4_X_L2 Code4_S1 = true
    ∧ PauliString.commutes Code4_X_L2 Code4_S2 = true
    ∧ PauliString.commutes Code4_Z_L1 Code4_S1 = true
    ∧ PauliString.commutes Code4_Z_L1 Code4_S2 = true
    ∧ PauliString.commutes Code4_Z_L2 Code4_S1 = true
    ∧ PauliString.commutes Code4_Z_L2 Code4_S2 = true

example :
    PauliString.commutes Code4_X_L1 Code4_Z_L1 = false
    ∧ PauliString.commutes Code4_X_L2 Code4_Z_L2 = false

example :
    PauliString.commutes Code4_X_L1 Code4_Z_L2 = true
    ∧ PauliString.commutes Code4_X_L2 Code4_Z_L1 = true
    ∧ PauliString.commutes Code4_X_L1 Code4_X_L2 = true
    ∧ PauliString.commutes Code4_Z_L1 Code4_Z_L2 = true

def Code4Code4_X_L1_left : PauliString

def Code4Code4_X_L2_left : PauliString

def Code4Code4_Z_L1_left : PauliString

def Code4Code4_Z_L2_left : PauliString

def Code4Code4_X_L1_right : PauliString

def Code4Code4_X_L2_right : PauliString

def Code4Code4_Z_L1_right : PauliString

def Code4Code4_Z_L2_right : PauliString

def Code4Code4_logicals : List PauliString

example :
    ∀ ppm ∈ Code4Code4_CNOT_surgery_schedule,
    ∀ L ∈ Code4Code4_logicals, ppm.commutes_with L = true

theorem Code4Code4_surgery_schedule_logical_identity :
    ∀ ppm ∈ Code4Code4_CNOT_surgery_schedule,
    ∀ L ∈ Code4Code4_logicals, ppm.commutes_with L = true

def PauliString.product_of_list (head : PauliString) :
    List PauliString → Pauli.Phase × PauliString
  | [] => (.pos, head)
  | P :: rest =>
      let (φ_acc, R_acc)

def Code4Code4_surgery_joint_action : Pauli.Phase × PauliString

example :
    Code4Code4_surgery_joint_action.2 =
      [.Z, .Z, .Z, .Z, .X, .X, .X, .X]

example :
    Code4Code4_surgery_joint_action.1 = Pauli.Phase.pos

theorem PauliString.product_of_list_nil (head : PauliString) :
    PauliString.product_of_list head [] = (Pauli.Phase.pos, head)

theorem PauliString.product_of_list_singleton (head P : PauliString) :
    PauliString.product_of_list head [P] = PauliString.mul head P

theorem PauliString.product_of_list_cons_string
    (head P : PauliString) (rest : List PauliString) :
    (PauliString.product_of_list head (P :: rest)).2
      = (PauliString.mul (PauliString.product_of_list head rest).2 P).2

theorem PauliString.product_of_list_cons_phase
    (head P : PauliString) (rest : List PauliString) :
    (PauliString.product_of_list head (P :: rest)).1
      = Pauli.Phase.mul (PauliString.product_of_list head rest).1
          (PauliString.mul (PauliString.product_of_list head rest).2 P).1

theorem PauliString.product_of_list_pair (head P Q : PauliString) :
    PauliString.product_of_list head [P, Q]
      = (Pauli.Phase.mul (PauliString.mul head Q).1
            (PauliString.mul (PauliString.mul head Q).2 P).1,
         (PauliString.mul (PauliString.mul head Q).2 P).2)

theorem Pauli.mul_self (p : Pauli) : Pauli.mul p p = (Pauli.Phase.pos, Pauli.I)

theorem PauliString.mul_self_phase_pos : ∀ (P : PauliString),
    (PauliString.mul P P).1 = Pauli.Phase.pos
  | [] => rfl
  | p :: ps =>

theorem PauliString.mul_self_string_eq_id : ∀ (P : PauliString),
    (PauliString.mul P P).2 = PauliString.id P.length
  | [] => rfl
  | p :: ps =>

def Code4Code4_merge_measure : PauliString

example :
    PauliString.mul Code4Code4_X_L1_left Code4Code4_merge_measure
      = PauliString.mul Code4Code4_merge_measure Code4Code4_X_L1_left

example :
    PauliString.mul Code4Code4_X_L1_left Code4Code4_merge_measure
      = (Pauli.Phase.pos,
         [Pauli.I, Pauli.I, Pauli.X, Pauli.X, Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z])

example :
    PauliString.product_of_list Code4Code4_X_L1_left [Code4Code4_merge_measure]
      = PauliString.mul Code4Code4_X_L1_left Code4Code4_merge_measure

example :
    PauliString.mul Code4Code4_X_L1_left Code4Code4_merge_measure
      = PauliString.mul Code4Code4_merge_measure Code4Code4_X_L1_left
    ∧ PauliString.mul Code4Code4_X_L2_left Code4Code4_merge_measure
        = PauliString.mul Code4Code4_merge_measure Code4Code4_X_L2_left
    ∧ PauliString.mul Code4Code4_Z_L1_left Code4Code4_merge_measure
        = PauliString.mul Code4Code4_merge_measure Code4Code4_Z_L1_left
    ∧ PauliString.mul Code4Code4_Z_L2_left Code4Code4_merge_measure
        = PauliString.mul Code4Code4_merge_measure Code4Code4_Z_L2_left

def Code4Code4_CNOT_image_X_L1 : PauliString

def Code4Code4_CNOT_image_X_R1 : PauliString

def Code4Code4_CNOT_image_Z_L1 : PauliString

def Code4Code4_CNOT_image_Z_R1 : PauliString

example :
    Code4Code4_CNOT_image_X_L1 = [.X, .X, .I, .I, .X, .X, .I, .I]

example :
    Code4Code4_CNOT_image_Z_R1 = [.Z, .I, .Z, .I, .Z, .I, .Z, .I]

theorem TODO_emergent_CNOT_image_X_L1 :
    -- Placeholder shape: `apply_surgery (X_L1_left) ≅ X_L1·X_R1`
    -- needs LogicalState + apply_surgery_with_corrections.
    -- For now: the Pauli-algebra shadow holds (decide-checked above).
    Code4Code4_CNOT_image_X_L1
      = (PauliString.mul Code4Code4_X_L1_left Code4Code4_X_L1_right).2

theorem TODO_emergent_CNOT_image_X_R1 :
    Code4Code4_CNOT_image_X_R1 = Code4Code4_X_L1_right

theorem TODO_emergent_CNOT_image_Z_L1 :
    Code4Code4_CNOT_image_Z_L1 = Code4Code4_Z_L1_left

theorem TODO_emergent_CNOT_image_Z_R1 :
    Code4Code4_CNOT_image_Z_R1
      = (PauliString.mul Code4Code4_Z_L1_left Code4Code4_Z_L1_right).2

def RealizesUpToFrame {n : Type*} [Fintype n] [DecidableEq n]
    (op frame U : Matrix n n ℂ) : Prop

theorem realizes_comp {n : Type*} [Fintype n] [DecidableEq n]
    {op1 op2 f1 f2 f1' U1 U2 : Matrix n n ℂ}
    (h1 : RealizesUpToFrame op1 f1 U1)
    (h2 : RealizesUpToFrame op2 f2 U2)
    (hcomm : U2 * f1 = f1' * U2) :
    RealizesUpToFrame (op2 * op1) (f2 * f1') (U2 * U1)

theorem realizes_comp_id_lower {n : Type*} [Fintype n] [DecidableEq n]
    {op1 op2 f2 U1 U2 : Matrix n n ℂ}
    (h1 : RealizesUpToFrame op1 1 U1)
    (h2 : RealizesUpToFrame op2 f2 U2) :
    RealizesUpToFrame (op2 * op1) f2 (U2 * U1)

structure PPMGadgetInterface (dim : Nat)

theorem compileToPPM_correct {dim : Nat} (Iface : PPMGadgetInterface dim)
    {C : BaseUCom dim} (hC : IsCliffordT C) :
    RealizesUpToFrame (Iface.compile C) (Iface.frame C) (uc_eval C)

theorem tGadget_realizes_frame
    (U proj corr : Matrix (Fin 4) (Fin 4) ℂ) :
    RealizesUpToFrame (corr * proj * U) (corr * proj) U

theorem tGadget_denote_eq_frame_apply
    (U proj corr : Matrix (Fin 4) (Fin 4) ℂ)
    (ψ res : StateVec 1) :
    FormalRV.PPM.PPMDenote.gadgetDenote U proj corr ψ res
      = ((corr * proj) * U) * (ψ ⊗ᵥ res)

theorem realizes_trivial_frame {n : Type*} [Fintype n] [DecidableEq n]
    {op U : Matrix n n ℂ}
    (h : RealizesUpToFrame op (1 : Matrix n n ℂ) U) : op = U

theorem success_transfer {dim : Nat}
    (succ : Square dim → ℝ)
    {compiledOp f : Square dim} {C : BaseUCom dim}
    (hreal : RealizesUpToFrame compiledOp f (uc_eval C))
    (hframe : ∀ U : Square dim, succ (f * U) = succ U) :
    succ compiledOp = succ (uc_eval C)

noncomputable def pauliProj (P : Pauli) (b : Bool) : Matrix (Fin 2) (Fin 2) ℂ

abbrev corrOp (Q : Pauli) : Matrix (Fin 2) (Fin 2) ℂ

theorem pauli_conjTranspose (P : Pauli) : P.toMatrix.conjTranspose = P.toMatrix

theorem signedPauli_sq (P : Pauli) (b : Bool) :
    (if b then -P.toMatrix else P.toMatrix) * (if b then -P.toMatrix else P.toMatrix)
      = (1 : Matrix (Fin 2) (Fin 2) ℂ)

theorem pauliProj_idem (P : Pauli) (b : Bool) :
    pauliProj P b * pauliProj P b = pauliProj P b

theorem pauliProj_herm (P : Pauli) (b : Bool) :
    (pauliProj P b).conjTranspose = pauliProj P b

theorem pauliProj_resolution (P : Pauli) :
    pauliProj P false + pauliProj P true = (1 : Matrix (Fin 2) (Fin 2) ℂ)

theorem pauliProj_orthogonal (P : Pauli) :
    pauliProj P false * pauliProj P true = 0

noncomputable def gadgetDenote
    (U proj corr : Matrix (Fin 4) (Fin 4) ℂ) (ψ res : StateVec 1) : StateVec 2

theorem gadgetDenote_eq
    (U proj corr : Matrix (Fin 4) (Fin 4) ℂ) (ψ res : StateVec 1) :
    gadgetDenote U proj corr ψ res = (corr * proj * U) * (ψ ⊗ᵥ res)

theorem tGadget_denote_outcome_0 (ψ : StateVec 1) :
    gadgetDenote cnotMatrix projLow0 (1 : Matrix (Fin 4) (Fin 4) ℂ) ψ tKet
      = (1 / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1))

theorem tGadget_denote_outcome_1 (ψ : StateVec 1) :
    gadgetDenote cnotMatrix projLow1 Shigh ψ tKet
      = (ω / Real.sqrt 2 : ℂ) • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1))

theorem tGadget_data_outcome_independent (ψ : StateVec 1) :
    (∃ c₀ : ℂ, gadgetDenote cnotMatrix projLow0 (1 : Matrix (Fin 4) (Fin 4) ℂ) ψ tKet
        = c₀ • (Tdata ψ ⊗ᵥ (basisState 0 : StateVec 1)))
    ∧ (∃ c₁ : ℂ, gadgetDenote cnotMatrix projLow1 Shigh ψ tKet
        = c₁ • (Tdata ψ ⊗ᵥ (basisState 1 : StateVec 1)))

theorem tGadget_outcome1_correction_bridge (ψ : StateVec 1) :
    Shigh * gadgetDenote cnotMatrix projLow1 (1 : Matrix (Fin 4) (Fin 4) ℂ) ψ tKet
      = gadgetDenote cnotMatrix projLow1 Shigh ψ tKet

theorem clifford_gadget_intertwine :
    corrOp Pauli.X * pauliProj Pauli.Z true
      = pauliProj Pauli.Z false * corrOp Pauli.X

theorem clifford_gadget_outcome_independent (ψ : StateVec 1) :
    corrOp Pauli.X * (pauliProj Pauli.Z true * ψ)
      = pauliProj Pauli.Z false * (corrOp Pauli.X * ψ)

noncomputable def exactFrameInstance (dim : Nat)
    (hinv : ∀ c : BaseUCom dim, Invertible (uc_eval c)) :
    PPMGadgetInterface dim

theorem exactFrame_compiles_correctly (dim : Nat)
    (hinv : ∀ c : BaseUCom dim, Invertible (uc_eval c))
    {C : BaseUCom dim} (hC : IsCliffordT C) :
    (exactFrameInstance dim hinv).compile C = uc_eval C

theorem exactFrame_success_transfer (dim : Nat)
    (hinv : ∀ c : BaseUCom dim, Invertible (uc_eval c))
    (succ : Square dim → ℝ) {C : BaseUCom dim} (hC : IsCliffordT C) :
    succ ((exactFrameInstance dim hinv).compile C) = succ (uc_eval C)

abbrev StabilizerState

def valid_length (s : StabilizerState) (n : Nat) : Bool

def valid_commuting (s : StabilizerState) : Bool

def valid (s : StabilizerState) (n : Nat) : Bool

def find_anticommuting
    (s : StabilizerState) (P : PauliString) : Option Nat

def apply_PPM_pos
    (s : StabilizerState) (P : PauliString) : StabilizerState

def apply_PPM_neg
    (s : StabilizerState) (P : PauliString) : StabilizerState

def plus_state : StabilizerState

def zero_state : StabilizerState

def one_state  : StabilizerState

theorem PPM_Z_on_plus_pos :
    apply_PPM_pos plus_state ⟨.plus, [.Z]⟩
    = [⟨.plus, [.Z]⟩]

theorem PPM_Z_on_plus_neg :
    apply_PPM_neg plus_state ⟨.plus, [.Z]⟩
    = [⟨.minus, [.Z]⟩]

theorem PPM_Z_on_zero_pos :
    apply_PPM_pos zero_state ⟨.plus, [.Z]⟩ = zero_state

def bell_state : StabilizerState

theorem bell_state_valid :
    StabilizerState.valid bell_state 2 = true

theorem PPM_Z1_on_bell_pos :
    apply_PPM_pos bell_state ⟨.plus, [.Z, .I]⟩
    = [⟨.plus, [.Z, .I]⟩, ⟨.plus, [.Z, .Z]⟩]

theorem PPM_Z1_on_bell_pos_valid :
    StabilizerState.valid
      (apply_PPM_pos bell_state ⟨.plus, [.Z, .I]⟩) 2 = true

theorem PPM_preserves_validity_plus_Z :
    StabilizerState.valid
      (apply_PPM_pos plus_state ⟨.plus, [.Z]⟩) 1 = true

theorem PPM_preserves_validity_plus_X :
    StabilizerState.valid
      (apply_PPM_pos plus_state ⟨.plus, [.X]⟩) 1 = true

theorem PPM_preserves_validity_bell_Z1 :
    StabilizerState.valid
      (apply_PPM_pos bell_state ⟨.plus, [.Z, .I]⟩) 2 = true

theorem PPM_preserves_validity_bell_X2 :
    StabilizerState.valid
      (apply_PPM_pos bell_state ⟨.plus, [.I, .X]⟩) 2 = true

def isTMagic : QasmOp → Bool | .opT _ => true | _ => false

def isCCZMagic : QasmOp → Bool | .opCCZ _ _ _ => true | _ => false

def isMeas : QasmOp → Bool | .opMeas _ _ => true | _ => false

def isFeedforward : QasmOp → Bool
  | .opIf _ _ => true | .opIf2 _ _ _ => true | _ => false

def isClifford : QasmOp → Bool
  | .opH _ => true | .opS _ => true | .opX _ => true | .opZ _ => true
  | .opCX _ _ => true | .opCZ _ _ => true | _ => false

def maxQubitOf : QasmOp → Nat
  | .opH q | .opT q | .opS q | .opX q | .opZ q => q
  | .opCX a b | .opCZ a b => max a b
  | .opCCZ a b c => max a (max b c)
  | .opMeas q _ => q
  | .opIf _ op | .opIf2 _ _ op => maxQubitOf op

def numTMagic      (ops : List QasmOp) : Nat

def numCCZMagic    (ops : List QasmOp) : Nat

def numMeas        (ops : List QasmOp) : Nat

def numFeedforward (ops : List QasmOp) : Nat

def numClifford    (ops : List QasmOp) : Nat

def numQubits      (ops : List QasmOp) : Nat

def seqDepth       (ops : List QasmOp) : Nat

theorem numTMagic_append (p q : List QasmOp) :
    numTMagic (p ++ q) = numTMagic p + numTMagic q

theorem numCCZMagic_append (p q : List QasmOp) :
    numCCZMagic (p ++ q) = numCCZMagic p + numCCZMagic q

theorem numMeas_append (p q : List QasmOp) :
    numMeas (p ++ q) = numMeas p + numMeas q

theorem numFeedforward_append (p q : List QasmOp) :
    numFeedforward (p ++ q) = numFeedforward p + numFeedforward q

theorem numClifford_append (p q : List QasmOp) :
    numClifford (p ++ q) = numClifford p + numClifford q

theorem seqDepth_append (p q : List QasmOp) :
    seqDepth (p ++ q) = seqDepth p + seqDepth q

theorem tGadget_qubits      : numQubits tGadgetOps = 2

theorem tGadget_TMagic      : numTMagic tGadgetOps = 1

theorem tGadget_CCZMagic    : numCCZMagic tGadgetOps = 0

theorem tGadget_meas        : numMeas tGadgetOps = 1

theorem tGadget_feedforward : numFeedforward tGadgetOps = 1

theorem tGadget_clifford    : numClifford tGadgetOps = 2

theorem cczGadget_qubits      : numQubits cczGadgetOps = 6

theorem cczGadget_TMagic      : numTMagic cczGadgetOps = 0

theorem cczGadget_CCZMagic    : numCCZMagic cczGadgetOps = 1

theorem cczGadget_meas        : numMeas cczGadgetOps = 3

theorem cczGadget_feedforward : numFeedforward cczGadgetOps = 6

theorem cczGadget_clifford    : numClifford cczGadgetOps = 6

example : numMeas (tGadgetOps ++ cczGadgetOps) = 4

example : numTMagic (tGadgetOps ++ cczGadgetOps) = 1

example : numCCZMagic (tGadgetOps ++ cczGadgetOps) = 1

theorem Pauli.commutes_comm (a b : Pauli) :
    Pauli.commutes a b = Pauli.commutes b a

theorem Pauli.commutes_mul (a b c : Pauli) :
    Pauli.commutes (Pauli.mul a b).2 c
      = (Pauli.commutes a c == Pauli.commutes b c)

theorem apply_PPM_pos_length (s : StabilizerState) (P : PauliString) :
    (apply_PPM_pos s P).length = s.length

theorem apply_PPM_neg_length (s : StabilizerState) (P : PauliString) :
    (apply_PPM_neg s P).length = s.length

theorem apply_PPM_pos_mem (s : StabilizerState) (P : PauliString) (i : Nat)
    (hi : find_anticommuting s P = some i) (hlt : i < s.length) :
    P ∈ apply_PPM_pos s P

theorem apply_PPM_neg_mem (s : StabilizerState) (P : PauliString) (i : Nat)
    (hi : find_anticommuting s P = some i) (hlt : i < s.length) :
    P.neg ∈ apply_PPM_neg s P

theorem apply_PPM_outcome_independent_ops (s : StabilizerState) (P : PauliString) :
    (apply_PPM_pos s P).map (·.ops) = (apply_PPM_neg s P).map (·.ops)

noncomputable def trivAnc : StateVec 0

theorem kron_vec_triv_right {a : Nat} (ψ : StateVec a) :
    (ψ ⊗ᵥ trivAnc : StateVec (a + 0)) = ψ

theorem ccz_magic_realizes_outcome_000 :
    MagicRealizes (dD

theorem clifford_magic_realizes {dD : Nat} (U : Square dD) :
    MagicRealizes (dD

structure Gadget (dD : Nat)

noncomputable def foldGateProduct {dD : Nat} : List (Gadget dD) → Square dD
  | [] => 1
  | g :: gs => foldGateProduct gs * g.U

theorem magic_realizes_list_fold {dD : Nat}
    (gs : List (Gadget dD)) (ψ : StateVec dD) :
    ∃ (final : StateVec dD) (c : ℂ),
      final = c • (foldGateProduct gs * ψ)
      ∧ (∀ (g : Gadget dD) (gtl : List (Gadget dD)), gs = g :: gtl →
          ∃ (anc : StateVec g.dA) (chead : ℂ),
            g.G * (ψ ⊗ᵥ g.magic) = chead • ((g.U * ψ) ⊗ᵥ anc))

def PPMRealizesShorOracle
    (m n anc : Nat) (f_ver f_ppm : Nat → BaseUCom (n + anc)) : Prop

theorem ppm_preserves_success
    (a r N m n anc : Nat)
    (f_ver f_ppm : Nat → BaseUCom (n + anc))
    (hppm : PPMRealizesShorOracle m n anc f_ver f_ppm) :
    probability_of_success a r N m n anc f_ppm
      = probability_of_success a r N m n anc f_ver

theorem ppm_realized_shor_succeeds
    (a r N m bits ainv : Nat)
    (f_ppm : Nat → BaseUCom (bits + ModMul.ancillaWidth bits))
    (h_setting : ShorSetting a r N m bits)
    (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1)
    (hppm : PPMRealizesShorOracle m bits (ModMul.ancillaWidth bits)
              (ModMul.circuitFamily a ainv N bits) f_ppm) :
    probability_of_success a r N m bits (ModMul.ancillaWidth bits) f_ppm
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem ppm_realized_shor_succeeds_with_budget
    (a r N m bits ainv : Nat)
    (f_ppm : Nat → BaseUCom (bits + ModMul.ancillaWidth bits))
    (h_setting : ShorSetting a r N m bits) (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1)
    (hppm : PPMRealizesShorOracle m bits (ModMul.ancillaWidth bits)
              (ModMul.circuitFamily a ainv N bits) f_ppm)
    (cutoff : ℕ) (p_L num_ops : ℝ) (hp_L : 0 ≤ p_L) (hnum : 0 ≤ num_ops) :
    probability_of_success a r N m bits (ModMul.ancillaWidth bits) f_ppm
      ≥ κ / (Nat.log2 N : ℝ) ^ 4 - (2 * Real.pi / 2 ^ cutoff) - num_ops * p_L

theorem ppm_shor_succeeds_from_effective_action
    (a r N m bits ainv : Nat)
    (f_ppm : Nat → BaseUCom (bits + ModMul.ancillaWidth bits))
    (h_setting : ShorSetting a r N m bits) (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1)
    (h_effective_action :
      uc_eval (QPE_var_lsb m (bits + ModMul.ancillaWidth bits) f_ppm)
          (Shor_initial_state m bits (ModMul.ancillaWidth bits))
        = uc_eval (QPE_var_lsb m (bits + ModMul.ancillaWidth bits)
            (ModMul.circuitFamily a ainv N bits))
          (Shor_initial_state m bits (ModMul.ancillaWidth bits))) :
    probability_of_success a r N m bits (ModMul.ancillaWidth bits) f_ppm

theorem ppm_realized_shor_succeeds_representative
    (a r N m bits ainv : Nat)
    (h_setting : ShorSetting a r N m bits) (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1) :
    probability_of_success a r N m bits (ModMul.ancillaWidth bits)
        (ModMul.circuitFamily a ainv N bits)
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

inductive QasmOp

def QasmOp.toLine : QasmOp → String
  | .opH q       => s!"h q[{q}];"
  | .opT q       => s!"t q[{q}];"
  | .opS q       => s!"s q[{q}];"
  | .opX q       => s!"x q[{q}];"
  | .opZ q       => s!"z q[{q}];"
  | .opCX c t    => s!"cx q[{c}], q[{t}];"
  | .opCZ a b    => s!"cz q[{a}], q[{b}];"
  -- CCZ is not in stdgates.inc; emit it as H·CCX·H (ccx, h ARE standard).
  | .opCCZ a b c => s!"h q[{c}]; ccx q[{a}], q[{b}], q[{c}]; h q[{c}];"
  | .opMeas q cr => s!"c[{cr}] = measure q[{q}];"
  | .opIf cr op  => s!"if (c[{cr}] == true) " ++ QasmOp.toLine op

def toQASM (nq ncr : Nat) (ops : List QasmOp) : String

def tGadgetOps : List QasmOp

def tGadgetQASM : String

def cczGadgetOps : List QasmOp

def cczGadgetQASM : String

theorem foldl_mul_snd (l : List (Pauli × Pauli)) (ph0 : Phase) (acc0 : List Pauli) :
    (l.foldl
      (fun (acc : Phase × List Pauli) (ab : Pauli × Pauli) =>
        let (a, b)

theorem mul_ops (p q : PauliString) :
    (p.mul q).ops = (p.ops.zip q.ops).map (fun ab => pmul2 ab.1 ab.2)

theorem mul_length (p q : PauliString) :
    (p.mul q).ops.length = min p.ops.length q.ops.length

theorem mul_length_eq (p q : PauliString) (n : Nat)
    (hp : p.ops.length = n) (hq : q.ops.length = n) :
    (p.mul q).ops.length = n

theorem pauli_commutes_mul (a b c : Pauli) :
    Pauli.commutes (pmul2 a b) c = (Pauli.commutes a c == Pauli.commutes b c)

theorem countP_xor_mod2 {α : Type} (l : List α) (f g : α → Bool) :
    (l.countP (fun x => xor (f x) (g x))) % 2
      = (l.countP f + l.countP g) % 2

theorem commutes_self (p : PauliString) : p.commutes p = true

theorem commutes_symm (p q : PauliString) (h : p.ops.length = q.ops.length) :
    p.commutes q = q.commutes p

def antiP : Pauli × Pauli → Bool

theorem commutes_eq (p q : PauliString) :
    p.commutes q = ((p.ops.zip q.ops).countP antiP % 2 == 0)

theorem add_mod2_eq (x y : Nat) :
    ((x + y) % 2 == 0) = ((x % 2 == 0) == (y % 2 == 0))

theorem antiCount_mul_left :
    ∀ la lb lc : List Pauli, la.length = lb.length → la.length = lc.length →
      ((((la.zip lb).map (fun ab => pmul2 ab.1 ab.2)).zip lc).countP antiP) % 2
      = ((la.zip lc).countP antiP + (lb.zip lc).countP antiP) % 2

theorem commutes_mul_left (a b c : PauliString)
    (hab : a.ops.length = b.ops.length) (hac : a.ops.length = c.ops.length) :
    (a.mul b).commutes c = (a.commutes c == b.commutes c)

theorem neg_ops (p : PauliString) : (p.neg).ops = p.ops

theorem neg_commutes_left (p q : PauliString) : (p.neg).commutes q = p.commutes q

theorem neg_commutes_right (p q : PauliString) : q.commutes (p.neg) = q.commutes p

theorem pair_commutes
    (P V g_anti g1 g2 : PauliString) (n : Nat)
    (hP : P.ops.length = n) (hV : V.ops.length = n)
    (hga : g_anti.ops.length = n)
    (h1 : g1.ops.length = n) (h2 : g2.ops.length = n)
    (c12 : g1.commutes g2 = true)
    (cga1 : g_anti.commutes g1 = true)
    (cga2 : g_anti.commutes g2 = true)
    (hgaP : g_anti.commutes P = false)
    (hVcg2 : V.commutes g2 = P.commutes g2)
    (hVcga : V.commutes g_anti = P.commutes g_anti)
    (hg1V : g1.commutes V = g1.commutes P)

theorem apply_generic_valid
    (s : StabilizerState) (P V : PauliString) (n i_anti : Nat) (g_anti : PauliString)
    (hv : StabilizerState.valid s n = true) (hP : P.ops.length = n) (hV : V.ops.length = n)
    (hf : find_anticommuting s P = some i_anti) (hg : s[i_anti]? = some g_anti)
    (hVcomm : ∀ q : PauliString, V.commutes q = P.commutes q)
    (hVcomm' : ∀ q : PauliString, q.commutes V = q.commutes P)
    (hVV : V.commutes V = true)
    (result : StabilizerState)
    (hres : result = (s.zipIdx).map (fun (g, j) =>
              if decide (j = i_anti) then V
              else if g.commutes P then g else g.mul g_anti)) :
    StabilizerState.valid result n = true

theorem apply_PPM_pos_preserves_valid (s : StabilizerState) (P : PauliString) (n : Nat)
    (hv : StabilizerState.valid s n = true) (hP : P.ops.length = n) :
    StabilizerState.valid (apply_PPM_pos s P) n = true

theorem apply_PPM_neg_preserves_valid (s : StabilizerState) (P : PauliString) (n : Nat)
    (hv : StabilizerState.valid s n = true) (hP : P.ops.length = n) :
    StabilizerState.valid (apply_PPM_neg s P) n = true

theorem apply_PPM_pos_inserts_P (s : StabilizerState) (P : PauliString)
    (h : (find_anticommuting s P).isSome = true) : P ∈ apply_PPM_pos s P

inductive PauliKind
  | I | X | Y | Z
  deriving Repr, DecidableEq

structure PauliFactor

abbrev PauliString

structure LogicalOpDef

structure CodeBlockWithLogicalOps

def pauli_string_qubits (p : PauliString) : List Nat

def pauli_string_in_atoms (p : PauliString) (allowed : List Nat) : Bool

def CodeBlockWithLogicalOps.find_op
    (block : CodeBlockWithLogicalOps) (local_idx : Nat) :
    Option LogicalOpDef

def verify_logical_pauli_measurement
    (clayout : CodedLogicalLayout)
    (blocks_with_ops : List CodeBlockWithLogicalOps)
    (logical_id : Nat)
    (kind : PauliKind)
    (physical : PauliString) : Bool

structure PauliMeasurementClaim

inductive Pauli

def commutes : Pauli → Pauli → Bool
  | .I, _ => true
  | _, .I => true
  | a, b => a == b

inductive Phase

def neg : Phase → Phase
  | .plus    => .minus
  | .minus   => .plus
  | .plus_i  => .minus_i
  | .minus_i => .plus_i

def mul : Phase → Phase → Phase
  | .plus,     b           => b
  | a,         .plus       => a
  | .minus,    .minus      => .plus
  | .minus,    .plus_i     => .minus_i
  | .minus,    .minus_i    => .plus_i
  | .plus_i,   .minus      => .minus_i
  | .plus_i,   .plus_i     => .minus
  | .plus_i,   .minus_i    => .plus
  | .minus_i,  .minus      => .plus_i
  | .minus_i,  .plus_i     => .plus
  | .minus_i,  .minus_i    => .minus

instance : Mul Phase

theorem mul_assoc (a b c : Phase) : (a * b) * c = a * (b * c)

theorem mul_plus (a : Phase) : a * .plus = a

theorem plus_mul (a : Phase) : Phase.plus * a = a

def mul : Pauli → Pauli → Phase × Pauli
  | .I, p => (.plus, p)
  | p, .I => (.plus, p)
  | .X, .X => (.plus, .I)
  | .Y, .Y => (.plus, .I)
  | .Z, .Z => (.plus, .I)
  | .X, .Y => (.plus_i,  .Z)
  | .Y, .X => (.minus_i, .Z)
  | .Y, .Z => (.plus_i,  .X)
  | .Z, .Y => (.minus_i, .X)
  | .Z, .X => (.plus_i,  .Y)
  | .X, .Z => (.minus_i, .Y)

theorem mul_self_is_I (p : Pauli) : (p.mul p).2 = .I

structure PauliString

instance : BEq PauliString

def neg (p : PauliString) : PauliString

def identity (n : Nat) : PauliString

def commutes (p q : PauliString) : Bool

def mul (p q : PauliString) : PauliString

instance : Mul PauliString

example : Pauli.mul .X .Y = (.plus_i, .Z)

example : Pauli.mul .Y .X = (.minus_i, .Z)

example : Pauli.mul .X .X = (.plus, .I)

example :
    PauliString.commutes
      ⟨.plus, [.X, .X]⟩ ⟨.plus, [.Z, .Z]⟩ = true

example :
    PauliString.commutes
      ⟨.plus, [.X, .I]⟩ ⟨.plus, [.Z, .I]⟩ = false

example :
    PauliString.commutes
      ⟨.plus, [.X, .Z]⟩ ⟨.plus, [.Z, .X]⟩ = true

example :
    PauliString.mul ⟨.plus, [.X]⟩ ⟨.plus, [.Y]⟩
    = ⟨.plus_i, [.Z]⟩

example :
    PauliString.mul ⟨.plus, [.X, .X]⟩ ⟨.plus, [.Z, .Z]⟩
    = ⟨.minus, [.Y, .Y]⟩

example :
    PauliString.mul (PauliString.identity 1) ⟨.plus, [.X]⟩
    = ⟨.plus, [.X]⟩

example :
    PauliString.commutes
      ⟨.plus_i, [.X, .Y, .Z]⟩ ⟨.plus_i, [.X, .Y, .Z]⟩ = true

def applyCorrection (Q : PauliString) (s : StabilizerState) : StabilizerState

inductive StabOp
  | meas : PauliString → StabOp   -- measure a Pauli (records an outcome)
  | corr : PauliString → StabOp   -- apply a Pauli correction (back-action)
  deriving Repr, Inhabited

abbrev StabProgram

def runProgram : StabProgram → List Bool → StabilizerState → StabilizerState
  | [], _, s => s
  | StabOp.corr Q :: ops, outcomes, s =>
      runProgram ops outcomes (applyCorrection Q s)
  | StabOp.meas P :: ops, [], s =>
      runProgram ops [] (apply_PPM_pos s P)
  | StabOp.meas P :: ops, b :: bs, s =>
      runProgram ops bs (if b then apply_PPM_neg s P else apply_PPM_pos s P)

def hProgram : StabProgram

def cnotProgram : StabProgram

theorem hProgram_runs_as_gadget (s : StabilizerState) :
    runProgram hProgram [false, false] s = hGadget s

theorem cnotProgram_runs_as_gadget (s : StabilizerState) :
    runProgram cnotProgram [false, false, false] s = cnotGadget s

theorem hProgram_truth_table :
    outputB (runProgram hProgram [false, false] input0)     = some (.plus,  .X)
  ∧ outputB (runProgram hProgram [false, false] input1)     = some (.minus, .X)
  ∧ outputB (runProgram hProgram [false, false] inputPlus)  = some (.plus,  .Z)
  ∧ outputB (runProgram hProgram [false, false] inputMinus) = some (.minus, .Z)

theorem cnotProgram_truth_table :
    runProgram cnotProgram [false,false,false] cnot_in00
        = [⟨.plus,  [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus,  [.Z,.Z,.Z]⟩]
  ∧ runProgram cnotProgram [false,false,false] cnot_in01
        = [⟨.plus,  [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]
  ∧ runProgram cnotProgram [false,false,false] cnot_in10
        = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.plus,  [.Z,.Z,.Z]⟩]
  ∧ runProgram cnotProgram [false,false,false] cnot_in11
        = [⟨.minus, [.Z,.I,.I]⟩, ⟨.plus, [.I,.Z,.I]⟩, ⟨.minus, [.Z,.Z,.Z]⟩]

theorem applyCorrection_length (Q : PauliString) (s : StabilizerState) :
    (applyCorrection Q s).length = s.length

def outputBPauli (s : StabilizerState) : Option Pauli

theorem hProgram_input0_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] input0) = some .X

theorem hProgram_input1_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] input1) = some .X

theorem hProgram_inputPlus_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] inputPlus) = some .Z

theorem hProgram_inputMinus_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] inputMinus) = some .Z

theorem sProgram_input0_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] sInput0) = some .Z

theorem sProgram_inputPlus_all_branches (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] sInputPlus) = some .Y

theorem hProgram_deferred_frame_correct (b₁ b₂ : Bool) :
    outputBPauli (runProgram hProgram [b₁, b₂] input0)     = some .X
  ∧ outputBPauli (runProgram hProgram [b₁, b₂] input1)     = some .X
  ∧ outputBPauli (runProgram hProgram [b₁, b₂] inputPlus)  = some .Z
  ∧ outputBPauli (runProgram hProgram [b₁, b₂] inputMinus) = some .Z

theorem cnotProgram_input00_ops_all_branches (b₁ b₂ b₃ : Bool) :
    (runProgram cnotProgram [b₁, b₂, b₃] cnot_in00).map (fun g => g.ops)
      = [[.Z, .I, .I], [.I, .Z, .I], [.Z, .Z, .Z]]

theorem cnotProgram_input10_ops_all_branches (b₁ b₂ b₃ : Bool) :
    (runProgram cnotProgram [b₁, b₂, b₃] cnot_in10).map (fun g => g.ops)
      = [[.Z, .I, .I], [.I, .Z, .I], [.Z, .Z, .Z]]

def indicator (i n : Nat) : BoolVec

def encodeBasisState (bits : Nat → Bool) (n : Nat) : StabilizerState

theorem signedZRow_commutes_eq (b : Bool) (l : BoolVec) (q : PauliString) :
    (signedZRow b l).commutes q = (zRow l).commutes q

theorem encode_all_commute_Z (bits : Nat → Bool) (n : Nat) (sup : BoolVec) :
    ∀ g ∈ encodeBasisState bits n, g.commutes (zRow sup) = true

theorem encode_Z_nondisturbing (bits : Nat → Bool) (n : Nat) (sup : BoolVec) :
    apply_PPM_pos (encodeBasisState bits n) (zRow sup) = encodeBasisState bits n

example : StabilizerState.valid (encodeBasisState (fun _ => false) 3) 3 = true

example : StabilizerState.valid (encodeBasisState (fun i => decide (i = 1)) 3) 3 = true

example :
    apply_PPM_pos (encodeBasisState (fun i => decide (i = 1) || decide (i = 2)) 3)
        (zRow [true, false, true])
      = encodeBasisState (fun i => decide (i = 1) || decide (i = 2)) 3

example :
    selectedSignedZProduct [true, false, true]
        [indicator 0 3, indicator 1 3, indicator 2 3] [false, true, true]
      = signedZRow true [true, false, true]

def tProj : Bool → Matrix (Fin 4) (Fin 4) ℂ
  | false => projLow0
  | true  => projLow1

noncomputable def tCorrection : Bool → Matrix (Fin 4) (Fin 4) ℂ
  | false => 1
  | true  => Shigh

noncomputable def tBorn : Bool → ℂ
  | false => 1 / Real.sqrt 2
  | true  => ω / Real.sqrt 2

noncomputable def tAnc : Bool → StateVec 1
  | false => basisState 0
  | true  => basisState 1

theorem t_gadget_with_feedback (ψ : StateVec 1) (b : Bool) :
    tCorrection b * (tProj b * (cnotMatrix * (ψ ⊗ᵥ tKet)))
      = tBorn b • (Tdata ψ ⊗ᵥ tAnc b)

theorem t_gadget_data_is_T (ψ : StateVec 1) (b : Bool) :
    ∃ c : ℂ, tCorrection b * (tProj b * (cnotMatrix * (ψ ⊗ᵥ tKet)))
      = c • (Tdata ψ ⊗ᵥ tAnc b)

def ccxPerm (k : Fin 8) : Fin 8

noncomputable def ccxPermMat : Matrix (Fin 8) (Fin 8) ℂ

noncomputable def Hbar3 : Matrix (Fin 8) (Fin 8) ℂ

theorem Hbar3_ccz_Hbar3 :
    Hbar3 * cczMat * Hbar3 = (2 : ℂ) • ccxPermMat

noncomputable def Had3 : Matrix (Fin 8) (Fin 8) ℂ

theorem inv_sqrt2_sq : ((1 : ℂ) / Real.sqrt 2) * ((1 : ℂ) / Real.sqrt 2) = 1 / 2

theorem had_ccz_had_eq_ccxPermMat :
    Had3 * cczMat * Had3 = ccxPermMat

theorem had_tDecomp_had_eq_ccxPermMat :
    Had3 * tDecompMat * Had3 = ccxPermMat

theorem ccxPerm_is_boolean_toffoli (k : Fin 8) :
    (aOf (ccxPerm k), bOf (ccxPerm k), cOf (ccxPerm k))
      = (aOf k, bOf k, xor (cOf k) (aOf k && bOf k))

theorem ccxPermMat_mulVec_basis (k : Fin 8) :
    ccxPermMat *ᵥ (fun j => if j = k then (1 : ℂ) else 0)
      = (fun i => if i = ccxPerm k then (1 : ℂ) else 0)

structure ToffoliScheme

noncomputable def cczTeleportScheme : ToffoliScheme

noncomputable def eightTScheme : ToffoliScheme

theorem schemes_realise_same_gate :
    cczTeleportScheme.gate = eightTScheme.gate

def bitfun (k : Fin 8) : Nat → Bool

theorem scheme_implements_gate_applyNat (k : Fin 8) :
    bitfun (ccxPerm k) = Gate.applyNat (Gate.CCX 0 1 2) (bitfun k)

theorem eightTScheme_implements_boolean_toffoli (k : Fin 8) :
    bitfun (ccxPerm k) = Gate.applyNat (Gate.CCX 0 1 2) (bitfun k)

def tripleAction (a b c : Bool) : Bool × Bool × Bool

theorem applyNat_CCX_as_tripleAction (a b c : Nat) (f : Nat → Bool) :
    Gate.applyNat (Gate.CCX a b c) f
      = (fun i => if i = c then (tripleAction (f a) (f b) (f c)).2.2 else f i)

theorem ccxPerm_certifies_tripleAction (k : Fin 8) :
    (aOf (ccxPerm k), bOf (ccxPerm k), cOf (ccxPerm k))
      = tripleAction (aOf k) (bOf k) (cOf k)

theorem scheme_realises_tripleAction (S : ToffoliScheme) (k : Fin 8) :
    S.gate *ᵥ (fun j => if j = k then (1 : ℂ) else 0)
      = (fun i => if i = ccxPerm k then (1 : ℂ) else 0)
    ∧ (aOf (ccxPerm k), bOf (ccxPerm k), cOf (ccxPerm k))
        = tripleAction (aOf k) (bOf k) (cOf k)

theorem teleportCCXProgram_realises_scheme_toffoli
    (F : TFactoryContract) (a b c : Nat)
    (input : Nat → Bool) (s σ' : MagicBasisPPMState)
    (hobs : (magicBasisRefinesApplyNat F).observesBits s input)
    (hrun : MagicPPMProgramRel F (teleportCCXProgram a b c) s σ') :
    (magicBasisRefinesApplyNat F).observesBits σ'
        (fun i => if i = c then (tripleAction (input a) (input b) (input c)).2.2 else input i)
    ∧ (∀ (S : ToffoliScheme) (k : Fin 8),
        S.gate *ᵥ (fun j => if j = k then (1 : ℂ) else 0)
            = (fun i => if i = ccxPerm k then (1 : ℂ) else 0)
          ∧ (aOf (ccxPerm k), bOf (ccxPerm k), cOf (ccxPerm k))
              = tripleAction (aOf k) (bOf k) (cOf k))

def fuse (sp1 sp2 : ZXSpider) : ZXSpider

theorem fuseZ_toPauli (S1 S2 : BoolVec) (h : S1.length = S2.length) :
    (zRow S1).mul (zRow S2) = zRow (vec_xor S1 S2)

theorem fuseX_toPauli (S1 S2 : BoolVec) (h : S1.length = S2.length) :
    (xRow S1).mul (xRow S2) = xRow (vec_xor S1 S2)

theorem fuse_toPauli (sp1 sp2 : ZXSpider) (hc : sp1.color = sp2.color)
    (h : sp1.support.length = sp2.support.length) :
    (fuse sp1 sp2).toPauli = (sp1.toPauli).mul (sp2.toPauli)

theorem fuse_toStabOp (sp1 sp2 : ZXSpider) (hc : sp1.color = sp2.color)
    (h : sp1.support.length = sp2.support.length) :
    (fuse sp1 sp2).toStabOp = StabOp.meas ((sp1.toPauli).mul (sp2.toPauli))

example :
    (fuse { color

example :
    (fuse { color

inductive ZXColor | Z | X
  deriving DecidableEq, Repr

structure ZXSpider

def ZXSpider.toPauli (sp : ZXSpider) : PauliString

def ZXSpider.toStabOp (sp : ZXSpider) : StabOp

def mkSpider (color : ZXColor) (idxs : List Nat) (n : Nat) : ZXSpider

abbrev ZXDiagram

def zxToPPM (d : ZXDiagram) : StabProgram

def zxRun (d : ZXDiagram) (s : StabilizerState) : StabilizerState

def mergeToZX_X (g : SurgeryGadget) : ZXDiagram

def mergeToZX_Z (g : SurgeryGadget) : ZXDiagram

theorem mergeZX_X_eq_schedule (g : SurgeryGadget) :
    zxToPPM (mergeToZX_X g) = (merged_stabilizers_X g).map StabOp.meas

theorem mergeZX_X_runs_as_surgery (g : SurgeryGadget) (s : StabilizerState) :
    zxRun (mergeToZX_X g) s = measureChecks (merged_stabilizers_X g) s

theorem mergeZX_Z_eq_schedule (g : SurgeryGadget) :
    zxToPPM (mergeToZX_Z g) = (merged_stabilizers_Z g).map StabOp.meas

theorem mergeZX_Z_runs_as_surgery (g : SurgeryGadget) (s : StabilizerState) :
    zxRun (mergeToZX_Z g) s = measureChecks (merged_stabilizers_Z g) s

example (s : StabilizerState) :
    zxRun [{ color