structure SurgeryGadget

def merged_n (g : SurgeryGadget) : Nat

def merged_hx (g : SurgeryGadget) : BoolMat

def merged_hz (g : SurgeryGadget) : BoolMat

def dimensions_consistent (g : SurgeryGadget) : Bool

def targets_logical_correctly (g : SurgeryGadget) : Bool

def tau_s_sufficient (g : SurgeryGadget) : Bool

def merged_is_qldpc (g : SurgeryGadget) : Bool

def verify_surgery_gadget (g : SurgeryGadget) : Bool

def verify_surgery_schedule (gadgets : List SurgeryGadget) : Bool

def factory121_zx : ZXDiagram

example : factory121_zx.length = 97

example : (zxToPPM factory121_zx).length = factory121_zx.length

def majority_gate_zx : ZXDiagram

def majority_gate_hwalls : List (List Nat)

example : majority_gate_zx.length = 43

example : (zxToPPM majority_gate_zx).length = majority_gate_zx.length

structure PPMScheduleCert

theorem all_invariants_ok_of_cert (c : PPMScheduleCert) :
    capacity_in_arch_ok c.arch c.syscalls
      && capacity_per_cycle_ok c.arch c.syscalls
      && exclusivity_ok c.syscalls
      && feedback_latency_ok c.arch.t_cycle_us c.syscalls = true

theorem throughput_ok_of_cert (c : PPMScheduleCert) :
    window_throughput_ok c.syscalls c.window_us c.max_per_window = true

theorem wallclock_is_derived (c : PPMScheduleCert) :
    c.wallclock_us
      = c.syscalls.foldl (fun acc sc => Nat.max acc sc.end_us) 0

def ge2021_ppm_schedule_cert : PPMScheduleCert

theorem ge2021_ppm_schedule_cert_all_ok :
    capacity_in_arch_ok ge2021_ppm_schedule_cert.arch
        ge2021_ppm_schedule_cert.syscalls
      && capacity_per_cycle_ok ge2021_ppm_schedule_cert.arch
        ge2021_ppm_schedule_cert.syscalls
      && exclusivity_ok ge2021_ppm_schedule_cert.syscalls
      && feedback_latency_ok ge2021_ppm_schedule_cert.arch.t_cycle_us
        ge2021_ppm_schedule_cert.syscalls = true

theorem ge2021_ppm_schedule_cert_wallclock :
    ge2021_ppm_schedule_cert.wallclock_us = 16

def ppm_pair_arch : ZonedArch

def ppm_block (start_us data anc decoder_id : Nat) : List SysCall

def ppm_pair_sequential_syscalls : List SysCall

theorem ppm_pair_sequential_capacity_in_arch_ok :
    capacity_in_arch_ok ppm_pair_arch ppm_pair_sequential_syscalls = true

theorem ppm_pair_sequential_exclusivity_ok :
    exclusivity_ok ppm_pair_sequential_syscalls = true

theorem ppm_pair_sequential_feedback_latency_ok :
    feedback_latency_ok ppm_pair_arch.t_cycle_us ppm_pair_sequential_syscalls = true

theorem ppm_pair_sequential_decoder_react_ok :
    decoder_react_ok 10 ppm_pair_sequential_syscalls = true

theorem ppm_pair_sequential_throughput_ok :
    window_throughput_ok ppm_pair_sequential_syscalls 1000 1000 = true

theorem ppm_pair_sequential_all_invariants_ok :
    all_invariants_ok ppm_pair_arch ppm_pair_sequential_syscalls 1000 1000
      (fun _ => 0) = true

def ppm_pair_parallel_distinct_syscalls : List SysCall

theorem ppm_pair_parallel_distinct_exclusivity_ok :
    exclusivity_ok ppm_pair_parallel_distinct_syscalls = true

theorem ppm_pair_parallel_distinct_all_invariants_ok :
    all_invariants_ok ppm_pair_arch ppm_pair_parallel_distinct_syscalls 1000 1000
      (fun _ => 0) = true

def ppm_pair_parallel_alias_syscalls : List SysCall

theorem ppm_pair_parallel_alias_exclusivity_fails :
    exclusivity_ok ppm_pair_parallel_alias_syscalls = false

theorem ppm_pair_parallel_alias_fails_only_exclusivity :
    capacity_in_arch_ok ppm_pair_arch ppm_pair_parallel_alias_syscalls = true
  ∧ feedback_latency_ok ppm_pair_arch.t_cycle_us
      ppm_pair_parallel_alias_syscalls = true
  ∧ decoder_react_ok 10 ppm_pair_parallel_alias_syscalls = true
  ∧ window_throughput_ok ppm_pair_parallel_alias_syscalls 1000 1000 = true
  ∧ exclusivity_ok ppm_pair_parallel_alias_syscalls = false

def capacity_bad_schedule : List SysCall

theorem capacity_bad_oversubscription_fails :
    capacity_in_arch_ok ppm_pair_arch capacity_bad_schedule = false

theorem capacity_bad_fails_only_capacity :
    capacity_in_arch_ok ppm_pair_arch capacity_bad_schedule = false
  ∧ exclusivity_ok capacity_bad_schedule = true
  ∧ feedback_latency_ok ppm_pair_arch.t_cycle_us capacity_bad_schedule = true
  ∧ decoder_react_ok 10 capacity_bad_schedule = true
  ∧ window_throughput_ok capacity_bad_schedule 1000 1000 = true

def feedback_bad_slow_schedule : List SysCall

theorem feedback_bad_latency_fails :
    feedback_latency_ok ppm_pair_arch.t_cycle_us feedback_bad_slow_schedule = false

theorem feedback_bad_fails_only_feedback_latency :
    capacity_in_arch_ok ppm_pair_arch feedback_bad_slow_schedule = true
  ∧ exclusivity_ok feedback_bad_slow_schedule = true
  ∧ decoder_react_ok 10 feedback_bad_slow_schedule = true
  ∧ window_throughput_ok feedback_bad_slow_schedule 1000 1000 = true
  ∧ feedback_latency_ok ppm_pair_arch.t_cycle_us feedback_bad_slow_schedule = false

def syscall_factory_claims : SysCall → List Nat
  | sc => match sc.kind with
          | .RequestMagicState zone_id => [200 + zone_id]
          | _                          => []

def factory_exclusivity_ok (sched : List SysCall) : Bool

def magic_factory_distinct_schedule : List SysCall

theorem magic_factory_distinct_ports_ok :
    factory_exclusivity_ok magic_factory_distinct_schedule = true

def magic_factory_same_port_schedule : List SysCall

theorem magic_factory_same_port_fails :
    factory_exclusivity_ok magic_factory_same_port_schedule = false

theorem magic_factory_same_port_passes_standard_exclusivity :
    exclusivity_ok magic_factory_same_port_schedule = true

def ppm_pair_sequential_wallclock_us : Nat

theorem ppm_pair_sequential_wallclock_value :
    ppm_pair_sequential_wallclock_us = 14

def ppm_pair_parallel_distinct_wallclock_us : Nat

theorem ppm_pair_parallel_distinct_wallclock_value :
    ppm_pair_parallel_distinct_wallclock_us = 4

theorem ppm_pair_sequential_wallclock_is_derived :
    ppm_pair_sequential_wallclock_us =
      ppm_pair_sequential_syscalls.foldl (fun acc sc => Nat.max acc sc.end_us) 0

theorem ppm_pair_parallel_distinct_wallclock_is_derived :
    ppm_pair_parallel_distinct_wallclock_us =
      ppm_pair_parallel_distinct_syscalls.foldl
        (fun acc sc => Nat.max acc sc.end_us) 0

def exclusivity_with_factory_ports_ok (sched : List SysCall) : Bool

theorem exclusivity_with_factory_ports_detects_same_port :
    exclusivity_with_factory_ports_ok magic_factory_same_port_schedule = false

theorem exclusivity_with_factory_ports_accepts_distinct_ports :
    exclusivity_with_factory_ports_ok magic_factory_distinct_schedule = true

theorem standard_exclusivity_misses_same_factory_port :
    exclusivity_ok magic_factory_same_port_schedule = true

def all_invariants_with_factory_ports_ok
    (arch : ZonedArch) (sched : List SysCall)
    (t_react_us window_us max_per_window : Nat) : Bool

def paper_I1_ok (arch : ZonedArch) (sched : List SysCall) : Bool

def paper_I2_strengthened_ok (sched : List SysCall) : Bool

def paper_I3_ok (arch : ZonedArch) (sched : List SysCall) (t_react_us : Nat) : Bool

def paper_I4_ok (sched : List SysCall) (window_us max_per_window : Nat) : Bool

theorem all_invariants_with_factory_ports_eq_paper_invariants
    (arch : ZonedArch) (sched : List SysCall)
    (t_react_us window_us max_per_window : Nat) :
    all_invariants_with_factory_ports_ok arch sched
        t_react_us window_us max_per_window
      = (paper_I1_ok arch sched
         && paper_I2_strengthened_ok sched
         && paper_I3_ok arch sched t_react_us
         && paper_I4_ok sched window_us max_per_window)

structure PPMScheduleCertWithFactoryPorts

theorem all_invariants_ok_of_cert (c : PPMScheduleCertWithFactoryPorts) :
    all_invariants_with_factory_ports_ok
        c.arch c.syscalls c.t_react_us c.window_us c.max_per_window = true

theorem wallclock_is_derived (c : PPMScheduleCertWithFactoryPorts) :
    c.wallclock_us
      = c.syscalls.foldl (fun acc sc => Nat.max acc sc.end_us) 0

theorem ge2021_ppm_block_factory_exclusivity_ok :
    factory_exclusivity_ok ppm_block_syscalls = true

def ge2021_ppm_schedule_cert_with_factory_ports : PPMScheduleCertWithFactoryPorts

theorem ge2021_ppm_schedule_cert_with_factory_ports_all_ok :
    all_invariants_with_factory_ports_ok
        ge2021_ppm_schedule_cert_with_factory_ports.arch
        ge2021_ppm_schedule_cert_with_factory_ports.syscalls
        ge2021_ppm_schedule_cert_with_factory_ports.t_react_us
        ge2021_ppm_schedule_cert_with_factory_ports.window_us
        ge2021_ppm_schedule_cert_with_factory_ports.max_per_window = true

theorem ppm_pair_sequential_factory_exclusivity_ok :
    factory_exclusivity_ok ppm_pair_sequential_syscalls = true

theorem ppm_pair_sequential_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch ppm_pair_sequential_syscalls 10 1000 1000 = true

theorem ppm_pair_parallel_distinct_factory_exclusivity_ok :
    factory_exclusivity_ok ppm_pair_parallel_distinct_syscalls = true

theorem ppm_pair_parallel_distinct_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch ppm_pair_parallel_distinct_syscalls 10 1000 1000 = true

def magic_factory_arch : ZonedArch

theorem magic_factory_same_port_fails_strengthened_bundle :
    all_invariants_with_factory_ports_ok
        magic_factory_arch magic_factory_same_port_schedule
        10 15 2 = false

theorem magic_factory_same_port_fails_only_factory_exclusivity :
    capacity_in_arch_ok magic_factory_arch magic_factory_same_port_schedule = true
  ∧ capacity_per_cycle_ok magic_factory_arch magic_factory_same_port_schedule = true
  ∧ exclusivity_ok magic_factory_same_port_schedule = true
  ∧ factory_exclusivity_ok magic_factory_same_port_schedule = false
  ∧ feedback_latency_ok magic_factory_arch.t_cycle_us
      magic_factory_same_port_schedule = true
  ∧ decoder_react_ok 10 magic_factory_same_port_schedule = true
  ∧ window_throughput_ok magic_factory_same_port_schedule 15 2 = true

theorem magic_factory_same_port_passes_standard_bundle :
    all_invariants_ok magic_factory_arch magic_factory_same_port_schedule
        15 2 (fun _ => 0) = true

theorem magic_factory_same_port_standard_vs_strengthened :
    all_invariants_ok magic_factory_arch magic_factory_same_port_schedule
        15 2 (fun _ => 0) = true
  ∧ all_invariants_with_factory_ports_ok
        magic_factory_arch magic_factory_same_port_schedule
        10 15 2 = false

def per_cycle_three_active_schedule : List SysCall

theorem per_cycle_three_active_capacity_passes :
    capacity_per_cycle_ok ppm_pair_arch per_cycle_three_active_schedule = true

theorem per_cycle_three_active_exclusivity_passes :
    exclusivity_ok per_cycle_three_active_schedule = true

def scheduleWallclockUs (xs : List SysCall) : Nat

def shiftSysCall (dt : Nat) (sc : SysCall) : SysCall

def shiftSchedule (dt : Nat) (xs : List SysCall) : List SysCall

def seqSchedules (xs ys : List SysCall) : List SysCall

def parSchedules (xs ys : List SysCall) : List SysCall

theorem scheduleWallclockUs_def (xs : List SysCall) :
    scheduleWallclockUs xs
      = xs.foldl (fun acc sc => Nat.max acc sc.end_us) 0

theorem shiftSchedule_length (dt : Nat) (xs : List SysCall) :
    (shiftSchedule dt xs).length = xs.length

theorem seqSchedules_length (xs ys : List SysCall) :
    (seqSchedules xs ys).length = xs.length + ys.length

theorem parSchedules_length (xs ys : List SysCall) :
    (parSchedules xs ys).length = xs.length + ys.length

theorem seqSchedules_wallclock_is_derived (xs ys : List SysCall) :
    scheduleWallclockUs (seqSchedules xs ys)
      = (seqSchedules xs ys).foldl (fun acc sc => Nat.max acc sc.end_us) 0

theorem parSchedules_wallclock_is_derived (xs ys : List SysCall) :
    scheduleWallclockUs (parSchedules xs ys)
      = (parSchedules xs ys).foldl (fun acc sc => Nat.max acc sc.end_us) 0

def seqManySchedules : List (List SysCall) → List SysCall
  | []         => []
  | xs :: rest => seqSchedules xs (seqManySchedules rest)

def parManySchedules : List (List SysCall) → List SysCall
  | []         => []
  | xs :: rest => parSchedules xs (parManySchedules rest)

theorem seqManySchedules_nil :
    seqManySchedules [] = []

theorem parManySchedules_nil :
    parManySchedules [] = []

theorem seqManySchedules_singleton (xs : List SysCall) :
    seqManySchedules [xs] = xs

theorem parManySchedules_singleton (xs : List SysCall) :
    parManySchedules [xs] = xs

structure PPMComposeContext

def validateScheduleWithFactoryPorts
    (arch : ZonedArch) (syscalls : List SysCall)
    (t_react_us window_us max_per_window : Nat) : Bool

def PPMComposeContext.validate
    (ctx : PPMComposeContext) (syscalls : List SysCall) : Bool

def mkPPMScheduleCertWithFactoryPorts
    (arch : ZonedArch) (syscalls : List SysCall)
    (t_react_us window_us max_per_window : Nat)
    (h_cap : capacity_in_arch_ok arch syscalls = true)
    (h_per_cycle : capacity_per_cycle_ok arch syscalls = true)
    (h_excl : exclusivity_ok syscalls = true)
    (h_fact : factory_exclusivity_ok syscalls = true)
    (h_fbk : feedback_latency_ok arch.t_cycle_us syscalls = true)
    (h_decode : decoder_react_ok t_react_us syscalls = true)
    (h_throt : window_throughput_ok syscalls window_us max_per_window = true) :
    PPMScheduleCertWithFactoryPorts

theorem mkPPMScheduleCertWithFactoryPorts_of_valid
    (arch : ZonedArch) (syscalls : List SysCall)
    (t_react_us window_us max_per_window : Nat)
    (h : all_invariants_with_factory_ports_ok arch syscalls
           t_react_us window_us max_per_window = true) :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = arch
      ∧ cert.syscalls = syscalls
      ∧ cert.t_react_us = t_react_us
      ∧ cert.window_us = window_us
      ∧ cert.max_per_window = max_per_window
      ∧ cert.wallclock_us = scheduleWallclockUs syscalls

theorem seq_ppm_pair_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ppm_pair_arch
      ∧ cert.syscalls = ppm_pair_sequential_syscalls
      ∧ cert.wallclock_us = scheduleWallclockUs ppm_pair_sequential_syscalls

theorem par_ppm_pair_distinct_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ppm_pair_arch
      ∧ cert.syscalls = ppm_pair_parallel_distinct_syscalls
      ∧ cert.wallclock_us = scheduleWallclockUs ppm_pair_parallel_distinct_syscalls

theorem validate_parallel_alias_false :
    validateScheduleWithFactoryPorts
        ppm_pair_arch ppm_pair_parallel_alias_syscalls 10 1000 1000 = false

def ppm_compose_A : List SysCall

def ppm_compose_B_same_anc : List SysCall

def ppm_compose_B_distinct_anc : List SysCall

def ppm_compose_C_distinct_anc : List SysCall

def seq_compose_AB : List SysCall

theorem seq_compose_AB_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch seq_compose_AB 10 1000 1000 = true

theorem seq_compose_AB_wallclock_is_derived :
    scheduleWallclockUs seq_compose_AB
      = seq_compose_AB.foldl (fun acc sc => Nat.max acc sc.end_us) 0

def par_compose_AB_distinct : List SysCall

theorem par_compose_AB_distinct_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch par_compose_AB_distinct 10 1000 1000 = true

def par_compose_AB_alias : List SysCall

theorem par_compose_AB_alias_rejected :
    validateScheduleWithFactoryPorts
        ppm_pair_arch par_compose_AB_alias 10 1000 1000 = false

def ppm_triple_sequential_syscalls : List SysCall

theorem ppm_triple_sequential_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch ppm_triple_sequential_syscalls 10 1000 1000 = true

theorem ppm_triple_sequential_wallclock_is_derived :
    scheduleWallclockUs ppm_triple_sequential_syscalls
      = ppm_triple_sequential_syscalls.foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

def ppm_triple_parallel_distinct_syscalls : List SysCall

theorem ppm_triple_parallel_distinct_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok
        ppm_pair_arch ppm_triple_parallel_distinct_syscalls 10 1000 1000 = true

theorem ppm_triple_parallel_distinct_wallclock_is_derived :
    scheduleWallclockUs ppm_triple_parallel_distinct_syscalls
      = ppm_triple_parallel_distinct_syscalls.foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

theorem composeSeqSchedulesWithFactoryPorts_of_valid
    (ctx : PPMComposeContext) (blocks : List (List SysCall))
    (h : all_invariants_with_factory_ports_ok ctx.arch
           (seqManySchedules blocks)
           ctx.t_react_us ctx.window_us ctx.max_per_window = true) :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ctx.arch
      ∧ cert.syscalls = seqManySchedules blocks
      ∧ cert.wallclock_us = scheduleWallclockUs (seqManySchedules blocks)

theorem composeParSchedulesWithFactoryPorts_of_valid
    (ctx : PPMComposeContext) (blocks : List (List SysCall))
    (h : all_invariants_with_factory_ports_ok ctx.arch
           (parManySchedules blocks)
           ctx.t_react_us ctx.window_us ctx.max_per_window = true) :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ctx.arch
      ∧ cert.syscalls = parManySchedules blocks
      ∧ cert.wallclock_us = scheduleWallclockUs (parManySchedules blocks)

def ppm_triple_ctx : PPMComposeContext

theorem ppm_triple_sequential_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ppm_triple_ctx.arch
      ∧ cert.syscalls = ppm_triple_sequential_syscalls

theorem ppm_triple_parallel_distinct_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ppm_triple_ctx.arch
      ∧ cert.syscalls = ppm_triple_parallel_distinct_syscalls

def cczInjectionSchedule (mA mB mC : SurgeryGadget) : Schedule

theorem cczInjection_reduces (mA mB mC : SurgeryGadget) (s : StabilizerState) :
    zxRun (scheduleProgramX (cczInjectionSchedule mA mB mC)) s
      = runScheduleX (cczInjectionSchedule mA mB mC) s

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

theorem cczInjection_rounds (mA mB mC : SurgeryGadget) :
    scheduleTotalRounds (cczInjectionSchedule mA mB mC)
      = mA.tau_s + mB.tau_s + mC.tau_s

theorem cczInjection_verified (mA mB mC : SurgeryGadget)
    (hA : SurgeryGadget.verify_surgery_gadget mA = true)
    (hB : SurgeryGadget.verify_surgery_gadget mB = true)
    (hC : SurgeryGadget.verify_surgery_gadget mC = true) :
    (cczInjectionSchedule mA mB mC).all
        (fun g => SurgeryGadget.verify_surgery_gadget g) = true

theorem teleportCCX_surface_realisation (a b c : Nat) (s : StabilizerState) :
    -- (i) operational reduction of the lattice-surgery realisation:
    (zxRun (scheduleProgramX
        (cczInjectionSchedule surface3_x_surgery surface3_x_surgery surface3_x_surgery)) s
      = runScheduleX
        (cczInjectionSchedule surface3_x_surgery surface3_x_surgery surface3_x_surgery) s)
    -- (ii) all three merges structurally verified:
    ∧ (cczInjectionSchedule surface3_x_surgery surface3_x_surgery surface3_x_surgery).all
        (fun g => SurgeryGadget.verify_surgery_gadget g) = true
    -- (iii) one magic state consumed:
    ∧ magicPPMRequestCount [MagicPPMCommand.teleportCCX a b c] = 1
    -- (iv) surgery time = 6 syndrome rounds:

def gadgetFootprint (g : SurgeryGadget) : Nat

def surgeryToStimAt (g : SurgeryGadget) (off : Nat) : String

def emitScheduleStimFrom : Schedule → Nat → String
  | [],        _   => ""
  | g :: rest, off =>
      surgeryToStimAt g off ++ "TICK\n" ++ emitScheduleStimFrom rest (off + gadgetFootprint g)

def emitScheduleStim (sched : Schedule) : String

def scheduleFootprint (sched : Schedule) : Nat

private theorem foldl_add_replicate (n acc c : Nat) :
    (List.replicate n c).foldl (· + ·) acc = acc + n * c

theorem scheduleFootprint_replicate (n : Nat) (g : SurgeryGadget) :
    scheduleFootprint (List.replicate n g) = n * gadgetFootprint g

def rowSupport (row : List Bool) : List Nat

private def nl : String

def xCheckBlock (anc : Nat) (support : List Nat) : String

def zCheckBlock (anc : Nat) (support : List Nat) : String

def surgeryToStim (g : SurgeryGadget) : String

def shorSched : List SysCall

def shorDeps : DepGraph

def shorCtx : SystemCtx

theorem shorCtx_resource_ok : checkAll baseInvariants shorCtx = true

theorem shorCtx_causality_ok : respectsCausality shorSched shorDeps = true

theorem shorCtx_fully_valid :
    checkAll (baseInvariants ++ [causalityInv shorDeps]) shorCtx = true

def badCausalSched : List SysCall

def badCausalCtx : SystemCtx

theorem badCausal_resource_ok : checkAll baseInvariants badCausalCtx = true

theorem badCausal_causality_fails :
    (causalityInv shorDeps).check badCausalCtx = false

theorem badCausal_unified_fails :
    checkAll (baseInvariants ++ [causalityInv shorDeps]) badCausalCtx = false

def badThroughputSched : List SysCall

def badThroughputCtx : SystemCtx

theorem badThroughput_resource_fails :
    checkAll baseInvariants badThroughputCtx = false

theorem two_magic_requests :
    (shorSched.filter (fun sc => match sc.kind with
      | SysCallKind.RequestMagicState _ => true | _ => false)).length = 2

theorem six_merge_measurements :
    (shorSched.filter (fun sc => match sc.kind with
      | SysCallKind.Measure q _ => decide (10 ≤ q) | _ => false)).length = 6

def demoSchedule : Schedule

theorem demoSchedule_verified :
    demoSchedule.all (fun g => SurgeryGadget.verify_surgery_gadget g) = true

theorem demoSchedule_reduces (s : StabilizerState) :
    zxRun (scheduleProgramX demoSchedule) s = runScheduleX demoSchedule s

private theorem foldl_add_replicate (n acc c : Nat) :
    (List.replicate n c).foldl (· + ·) acc = acc + n * c

theorem schedule_rounds_replicate (n : Nat) (g : SurgeryGadget) :
    scheduleTotalRounds (List.replicate n g) = n * g.tau_s

theorem demoSchedule_total_rounds : scheduleTotalRounds demoSchedule = 6

theorem demoSchedule_space : surgeryPhysQubits surface3_x_surgery = 28

theorem surface_schedule_full_stack (s : StabilizerState) :
    demoSchedule.all (fun g => SurgeryGadget.verify_surgery_gadget g) = true
    ∧ zxRun (scheduleProgramX demoSchedule) s = runScheduleX demoSchedule s
    ∧ scheduleTotalRounds demoSchedule = 6
    ∧ surgeryPhysQubits surface3_x_surgery = 28

theorem surface_shor_ppm_physically_realized
    (F : TFactoryContract)
    (a r N m bits ainv x : Nat)
    (h_setting : ShorSetting a r N m bits)
    (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1)
    (h_ainv_le : ainv ≤ N) (hx : x < N)
    (signs : List Bool)
    (hsig : signs.length = surface3_x_surgery.merged_hx.length) :
    -- (I) PPM-level Shor (reused):
    (FormalRV.SQIRPort.probability_of_success a r N m bits
        (ModMul.ancillaWidth bits) (ModMul.circuitFamily a ainv N bits)

def rowWeight (row : List Bool) : Nat

def surgeryPhysQubits (g : SurgeryGadget) : Nat

def surgeryCNOTs (g : SurgeryGadget) : Nat

def surgeryMeasPerRound (g : SurgeryGadget) : Nat

def surgeryRounds (g : SurgeryGadget) : Nat

def surgeryTotalMeas (g : SurgeryGadget) : Nat

theorem counted_surgery_is_verified :
    SurgeryGadget.verify_surgery_gadget surface3_x_surgery = true

theorem surface3_phys_qubits : surgeryPhysQubits surface3_x_surgery = 28

theorem surface3_cnots : surgeryCNOTs surface3_x_surgery = 45

theorem surface3_meas_per_round : surgeryMeasPerRound surface3_x_surgery = 14

theorem surface3_rounds : surgeryRounds surface3_x_surgery = 2

theorem surface3_total_meas : surgeryTotalMeas surface3_x_surgery = 28

def shorWorkload (T L : Nat) : Workload

theorem surface3_physPerLogical : physPerLogical surface3_qec = 13

theorem surface3_distance : surface3_qec.d = 3

theorem shor_surface_qubits (T L factory : Nat) (hw : Hardware) (ow p : Nat) :
    (estimateWith (surfaceModel factory) hw (shorWorkload T L) surface3_qec ow p).qubits
      = L * 26 + factory

theorem shor_surface_time (T L factory : Nat) (hw : Hardware) (ow p : Nat) :
    (estimateWith (surfaceModel factory) hw (shorWorkload T L) surface3_qec ow p).time_us_tenths
      = T * 3 * hw.cycle_time_us_tenths

theorem ctl_adder4_surface_qubits (L f : Nat) (hw : Hardware) :
    (estimateWith (surfaceModel f) hw
        (shorWorkload (ctl_adder_total_toffolis_n_bit 4) L) surface3_qec 0 0).qubits
      = L * 26 + f

theorem ctl_adder4_surface_time (L f : Nat) (hw : Hardware) :
    (estimateWith (surfaceModel f) hw
        (shorWorkload (ctl_adder_total_toffolis_n_bit 4) L) surface3_qec 0 0).time_us_tenths
      = 8 * 3 * hw.cycle_time_us_tenths

def surfaceCodeD (d : Nat) : FormalRV.Framework.QECCode

theorem surfaceCodeD_k (d : Nat) : (surfaceCodeD d).k = 1

theorem surfaceCodeD_dist (d : Nat) : (surfaceCodeD d).d = d

theorem surfaceCodeD_physPer (d : Nat) :
    physPerLogical (surfaceCodeD d) = (surfaceCodeD d).n

theorem surface27_is_1405 :
    (surfaceCodeD 27).n = 1405 ∧ (surfaceCodeD 27).d = 27
    ∧ physPerLogical (surfaceCodeD 27) = 1405

theorem surfaceShor_qubits_anyD (d T L factory : Nat) (hw : Hardware) (ow p : Nat) :
    (estimateWith (surfaceModel factory) hw (shorWorkload T L) (surfaceCodeD d) ow p).qubits
      = L * (2 * (surfaceCodeD d).n) + factory

theorem surfaceShor_time_anyD (d T L factory : Nat) (hw : Hardware) (ow p : Nat) :
    (estimateWith (surfaceModel factory) hw (shorWorkload T L) (surfaceCodeD d) ow p).time_us_tenths
      = T * d * hw.cycle_time_us_tenths

def patchSize (d : Nat) : Nat

def patchLo (i d : Nat) : Nat

def patchHi (i d : Nat) : Nat

theorem patches_disjoint (i j d : Nat) (h : i < j) : patchHi i d ≤ patchLo j d

def dataSites (d : Nat) : Nat

def syndromeAncilla (d : Nat) : Nat

def routingAncilla (d : Nat) : Nat

theorem patch_site_accounts (d : Nat) :
    patchSize d = dataSites d + routingAncilla d

def magicProducedInWindow (parallelFactories cyclesPerMagic window : Nat) : Nat

def factoryMeetsDemand (demand parallelFactories cyclesPerMagic window : Nat) : Bool

def factorySites (perFactory parallelFactories : Nat) : Nat

theorem factory_meets_demand_demo :
    factoryMeetsDemand 8 4 5 10 = true

theorem magicProduced_mono (P P' cyclesPerMagic window : Nat) (h : P ≤ P') :
    magicProducedInWindow P cyclesPerMagic window
      ≤ magicProducedInWindow P' cyclesPerMagic window

def surfaceShorSched : List SysCall

def surfaceShorCtx : SystemCtx

theorem surfaceShorCtx_valid : checkAll baseInvariants surfaceShorCtx = true

theorem surfaceShor_anyHardware (T L factory : Nat) (hw : Hardware) :
    (estimateWith (surfaceModel factory) hw (shorWorkload T L) (surfaceCodeD 27) 0 0).time_us_tenths
      = T * 27 * hw.cycle_time_us_tenths

def hwSuperconducting : Hardware

def hwTrappedIon      : Hardware

def hwNeutralAtom     : Hardware

example (T L f : Nat) :
    (estimateWith (surfaceModel f) hwSuperconducting (shorWorkload T L)
        (surfaceCodeD 27) 0 0).time_us_tenths = T * 27 * 10

example (T L f : Nat) :
    (estimateWith (surfaceModel f) hwTrappedIon (shorWorkload T L)
        (surfaceCodeD 27) 0 0).time_us_tenths = T * 27 * 1000

example (T L f : Nat) :
    (estimateWith (surfaceModel f) hwNeutralAtom (shorWorkload T L)
        (surfaceCodeD 27) 0 0).time_us_tenths = T * 27 * 10

example : checkAll baseInvariants surfaceShorCtx = true

theorem surfaceShorCtx_valid_superconducting :
    checkAll (baseInvariants ++ [superconductingFixedCouplingInv]) surfaceShorCtx = true

theorem surfaceShorCtx_valid_neutralAtom :
    checkAll (baseInvariants ++ [neutralAtomRigidMoveInv]) surfaceShorCtx = true

def signedXRow (s : Bool) (l : BoolVec) : PauliString

theorem xRow_eq_signedXRow_false (l : BoolVec) : xRow l = signedXRow false l

theorem pmul_xBit_phase (a b : Bool) :
    (Pauli.mul (xBit a) (xBit b)).1 = Phase.plus

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

theorem foldl_phase_plus (l : List (Pauli × Pauli)) (ph0 : Phase)
    (hall : ∀ ab ∈ l, (Pauli.mul ab.1 ab.2).1 = Phase.plus) :
    l.foldl (fun (ph : Phase) ab => ph.mul (Pauli.mul ab.1 ab.2).1) ph0 = ph0

theorem foldl_phase_plus_xBit (a b : BoolVec) :
    ((a.map xBit).zip (b.map xBit)).foldl
        (fun (ph : Phase) ab => ph.mul (Pauli.mul ab.1 ab.2).1) Phase.plus
      = Phase.plus

theorem signedXRow_mul_ops (sa sb : Bool) (a b : BoolVec) (h : a.length = b.length) :
    ((signedXRow sa a).mul (signedXRow sb b)).ops = (xRow (vec_xor a b)).ops

theorem signedXRow_mul_phase (sa sb : Bool) (a b : BoolVec) :
    ((signedXRow sa a).mul (signedXRow sb b)).phase
      = (if (sa != sb) then Phase.minus else Phase.plus)

theorem signedXRow_mul (sa sb : Bool) (a b : BoolVec) (h : a.length = b.length) :
    (signedXRow sa a).mul (signedXRow sb b) = signedXRow (sa != sb) (vec_xor a b)

def selectedParity : BoolVec → List Bool → Bool
  | [],          _       => false
  | _,           []      => false
  | false :: ts, _ :: ss => selectedParity ts ss
  | true :: ts,  s :: ss => s != selectedParity ts ss

def selectedSignedProduct : BoolVec → BoolMat → List Bool → PauliString
  | [],          _,         _       => xRow []
  | _,           [],        _       => xRow []
  | _,           _,         []      => xRow []
  | false :: ts, _ :: tm,   _ :: ss => selectedSignedProduct ts tm ss
  | true :: ts,  row :: tm, s :: ss =>
      let acc

theorem selectedSignedProduct_ops (n : Nat) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length →
      (selectedSignedProduct sel mat ss).ops = (xRow (row_combination sel mat)).ops

theorem parity_false_of_combo_nil (n : Nat) (hn : 0 < n) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length → row_combination sel mat = [] →
      selectedParity sel ss = false

theorem selectedSignedProduct_eq (n : Nat) (hn : 0 < n) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length →
      selectedSignedProduct sel mat ss
        = signedXRow (selectedParity sel ss) (row_combination sel mat)

theorem surgery_eigenvalue (g : SurgeryGadget) (n : Nat) (hn : 0 < n) (signs : List Bool)
    (hshape : ∀ r ∈ g.merged_hx, r.length = n) (hsig : signs.length = g.merged_hx.length)
    (hker : g.targets_logical_correctly = true) :
    selectedSignedProduct g.span_witness g.merged_hx signs
      = signedXRow (selectedParity g.span_witness signs) g.target_pauli

theorem xBit_commutes (x y : Bool) : Pauli.commutes (xBit x) (xBit y) = true

theorem xRow_commutes (a b : BoolVec) : (xRow a).commutes (xRow b) = true

theorem merged_X_checks_commute (g : SurgeryGadget) :
    ∀ p ∈ merged_stabilizers_X g, ∀ q ∈ merged_stabilizers_X g, p.commutes q = true

theorem apply_PPM_pos_preserves_mem_of_commutes
    (s : StabilizerState) (P L : PauliString) (hmem : L ∈ s) (hcomm : L.commutes P = true) :
    L ∈ apply_PPM_pos s P

def measureChecks (checks : List PauliString) (s : StabilizerState) : StabilizerState

theorem mem_measureChecks_of_commutesAll (checks : List PauliString) (L : PauliString)
    (s : StabilizerState) (hmem : L ∈ s) (hcomm : ∀ P ∈ checks, L.commutes P = true) :
    L ∈ measureChecks checks s

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

def SurgeryFaultTolerant (g : SurgeryGadget) (merged_dist : Nat) : Prop

theorem surgery_implements_logical_measurement
    (g : SurgeryGadget) (n : Nat) (signs : List Bool)
    (hn : 0 < n) (hshape : ∀ r ∈ g.merged_hx, r.length = n)
    (hsig : signs.length = g.merged_hx.length)
    (hverify : g.verify_surgery_gadget = true) :
    -- (R) the measured eigenvalue of the target logical = parity of the
    -- selected merged-X-check outcomes
    (selectedSignedProduct g.span_witness g.merged_hx signs
        = signedXRow (selectedParity g.span_witness signs) g.target_pauli)
    -- (N) any logical commuting with the measured set is preserved
    ∧ (∀ (L : PauliString) (s : StabilizerState), L ∈ s →
        (∀ P ∈ merged_stabilizers_X g, L.commutes P = true) →

example :
    selectedSignedProduct [true, true] [[true, false, true], [false, true, true]]
        [false, true]
      = signedXRow true [true, true, false]

def zRow (l : BoolVec) : PauliString

theorem pmul2_zBit (a b : Bool) : pmul2 (zBit a) (zBit b) = zBit (a != b)

theorem zipmap_pmul_zBit (a b : List Bool) (h : a.length = b.length) :
    ((a.map zBit).zip (b.map zBit)).map (fun p => pmul2 p.1 p.2)
      = (vec_xor a b).map zBit

theorem zRow_vec_xor_ops (a b : List Bool) (h : a.length = b.length) :
    ((zRow a).mul (zRow b)).ops = (zRow (vec_xor a b)).ops

def merged_stabilizers_Z (g : SurgeryGadget) : List PauliString

def selectedZProduct (sel : List Bool) (mat : BoolMat) : PauliString

theorem selectedZProduct_ops (n : Nat) :
    ∀ (sel : List Bool) (mat : BoolMat), (∀ r ∈ mat, r.length = n) →
      (selectedZProduct sel mat).ops = (zRow (row_combination sel mat)).ops

def signedZRow (s : Bool) (l : BoolVec) : PauliString

theorem zRow_eq_signedZRow_false (l : BoolVec) : zRow l = signedZRow false l

theorem pmul_zBit_phase (a b : Bool) :
    (Pauli.mul (zBit a) (zBit b)).1 = Phase.plus

theorem foldl_phase_plus_zBit (a b : BoolVec) :
    ((a.map zBit).zip (b.map zBit)).foldl
        (fun (ph : Phase) ab => ph.mul (Pauli.mul ab.1 ab.2).1) Phase.plus
      = Phase.plus

theorem signedZRow_mul_ops (sa sb : Bool) (a b : BoolVec) (h : a.length = b.length) :
    ((signedZRow sa a).mul (signedZRow sb b)).ops = (zRow (vec_xor a b)).ops

theorem signedZRow_mul_phase (sa sb : Bool) (a b : BoolVec) :
    ((signedZRow sa a).mul (signedZRow sb b)).phase
      = (if (sa != sb) then Phase.minus else Phase.plus)

theorem signedZRow_mul (sa sb : Bool) (a b : BoolVec) (h : a.length = b.length) :
    (signedZRow sa a).mul (signedZRow sb b) = signedZRow (sa != sb) (vec_xor a b)

def selectedZParity : BoolVec → List Bool → Bool
  | [],          _       => false
  | _,           []      => false
  | false :: ts, _ :: ss => selectedZParity ts ss
  | true :: ts,  s :: ss => s != selectedZParity ts ss

def selectedSignedZProduct : BoolVec → BoolMat → List Bool → PauliString
  | [],          _,         _       => zRow []
  | _,           [],        _       => zRow []
  | _,           _,         []      => zRow []
  | false :: ts, _ :: tm,   _ :: ss => selectedSignedZProduct ts tm ss
  | true :: ts,  row :: tm, s :: ss =>
      let acc

theorem selectedSignedZProduct_ops (n : Nat) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length →
      (selectedSignedZProduct sel mat ss).ops = (zRow (row_combination sel mat)).ops

theorem parity_false_of_combo_nil_Z (n : Nat) (hn : 0 < n) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length → row_combination sel mat = [] →
      selectedZParity sel ss = false

theorem selectedSignedZProduct_eq (n : Nat) (hn : 0 < n) :
    ∀ (sel : BoolVec) (mat : BoolMat) (ss : List Bool), (∀ r ∈ mat, r.length = n) →
      ss.length = mat.length →
      selectedSignedZProduct sel mat ss
        = signedZRow (selectedZParity sel ss) (row_combination sel mat)

theorem surgery_readout_operator_Z (g : SurgeryGadget) (n : Nat)
    (zwitness ztarget : BoolVec)
    (hshape : ∀ r ∈ g.merged_hz, r.length = n)
    (hzker : row_combination zwitness g.merged_hz = ztarget) :
    (selectedZProduct zwitness g.merged_hz).ops = (zRow ztarget).ops

theorem surgery_eigenvalue_Z (g : SurgeryGadget) (n : Nat) (hn : 0 < n)
    (zwitness ztarget : BoolVec) (signs : List Bool)
    (hshape : ∀ r ∈ g.merged_hz, r.length = n) (hsig : signs.length = g.merged_hz.length)
    (hzker : row_combination zwitness g.merged_hz = ztarget) :
    selectedSignedZProduct zwitness g.merged_hz signs
      = signedZRow (selectedZParity zwitness signs) ztarget

theorem zBit_commutes (x y : Bool) : Pauli.commutes (zBit x) (zBit y) = true

theorem zRow_commutes (a b : BoolVec) : (zRow a).commutes (zRow b) = true

theorem merged_Z_checks_commute (g : SurgeryGadget) :
    ∀ p ∈ merged_stabilizers_Z g, ∀ q ∈ merged_stabilizers_Z g, p.commutes q = true

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

theorem surgery_implements_logical_measurement_Z
    (g : SurgeryGadget) (n : Nat) (zwitness ztarget : BoolVec) (signs : List Bool)
    (hn : 0 < n) (hshape : ∀ r ∈ g.merged_hz, r.length = n)
    (hsig : signs.length = g.merged_hz.length)
    (hzker : row_combination zwitness g.merged_hz = ztarget) :
    -- (R) the measured eigenvalue of the target logical = parity of the
    -- selected merged-Z-check outcomes
    (selectedSignedZProduct zwitness g.merged_hz signs
        = signedZRow (selectedZParity zwitness signs) ztarget)
    -- (N) any logical commuting with the measured set is preserved
    ∧ (∀ (L : PauliString) (s : StabilizerState), L ∈ s →
        (∀ P ∈ merged_stabilizers_Z g, L.commutes P = true) →

example :
    selectedSignedZProduct [true, true] [[true, false, true], [false, true, true]]
        [false, true]
      = signedZRow true [true, true, false]

def surface3x2_dual : Framework.QECCode

def surface3x3_dual : Framework.QECCode

def supp036 : BoolVec

def supp_Z1Z2 : BoolVec

def supp_Z1Z2Z3 : BoolVec

def surface3_zz_merge : SurgeryGadget

theorem surface3_zz_merge_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_zz_merge = true

theorem surface3_zz_merge_target_is_logical :
    (surface3x2_qec.hx.all (fun r => ! gf2dot r supp_Z1Z2)
      && ! inRowspace surface3x2_qec.hz supp_Z1Z2) = true

def surface3_cnot : List SurgeryGadget

theorem surface3_cnot_verifies :
    SurgeryGadget.verify_surgery_schedule surface3_cnot = true

def surface3_zzz_merge : SurgeryGadget

theorem surface3_zzz_merge_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_zzz_merge = true

def surface3_ccx_injection : List SurgeryGadget

theorem surface3_ccx_injection_verifies :
    SurgeryGadget.verify_surgery_schedule surface3_ccx_injection = true

theorem cnot_and_ccx_injection_verified :
    SurgeryGadget.verify_surgery_schedule surface3_cnot = true
    ∧ SurgeryGadget.verify_surgery_schedule surface3_ccx_injection = true

def surface3x2_qec : Framework.QECCode

def supp_X1X2 : BoolVec

def surface3_xx_merge : SurgeryGadget

theorem surface3_xx_merge_dimensions :
    SurgeryGadget.dimensions_consistent surface3_xx_merge = true

theorem surface3_xx_merge_tau_s :
    SurgeryGadget.tau_s_sufficient surface3_xx_merge = true

theorem surface3_xx_merge_qldpc :
    SurgeryGadget.merged_is_qldpc surface3_xx_merge = true

theorem surface3_xx_merge_targets_correctly :
    SurgeryGadget.targets_logical_correctly surface3_xx_merge = true

theorem surface3_xx_merge_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_xx_merge = true

theorem surface3_xx_merge_target_is_logical :
    (surface3x2_qec.hz.all (fun r => ! gf2dot r supp_X1X2)
      && ! inRowspace surface3x2_qec.hx supp_X1X2) = true

theorem surface3_xx_merge_implements_logical
    (signs : List Bool) (hsig : signs.length = surface3_xx_merge.merged_hx.length) :
    (selectedSignedProduct surface3_xx_merge.span_witness surface3_xx_merge.merged_hx signs
        = signedXRow (selectedParity surface3_xx_merge.span_witness signs)
            surface3_xx_merge.target_pauli)
    ∧ (∀ (L : PauliString) (s : StabilizerState), L ∈ s →
        (∀ P ∈ merged_stabilizers_X surface3_xx_merge, L.commutes P = true) →
        L ∈ measureChecks (merged_stabilizers_X surface3_xx_merge) s)
    ∧ (∀ p ∈ merged_stabilizers_X surface3_xx_merge, ∀ q ∈ merged_stabilizers_X surface3_xx_merge,
        p.commutes q = true)

def surface3x3_qec : Framework.QECCode

def supp_X1X2X3 : BoolVec

def surface3_xxx_merge : SurgeryGadget

theorem surface3_xxx_merge_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_xxx_merge = true

theorem surface3_xxx_merge_target_is_logical :
    (surface3x3_qec.hz.all (fun r => ! gf2dot r supp_X1X2X3)
      && ! inRowspace surface3x3_qec.hx supp_X1X2X3) = true

def steane_x_surgery_conn_x : BoolMat

def steane_x_surgery_conn_z : BoolMat

def steane_x_surgery_ancilla_hx : BoolMat

def steane_x_surgery_ancilla_hz : BoolMat

def steane_x_surgery : SurgeryGadget

theorem steane_x_surgery_dimensions :
    SurgeryGadget.dimensions_consistent steane_x_surgery = true

theorem steane_x_surgery_tau_s :
    SurgeryGadget.tau_s_sufficient steane_x_surgery = true

theorem steane_x_surgery_qldpc :
    SurgeryGadget.merged_is_qldpc steane_x_surgery = true

theorem steane_x_surgery_targets_correctly :
    SurgeryGadget.targets_logical_correctly steane_x_surgery = true

theorem steane_x_surgery_verifies :
    SurgeryGadget.verify_surgery_gadget steane_x_surgery = true

def steane_x_surgery_WRONG : SurgeryGadget

theorem steane_x_surgery_WRONG_rejected :
    SurgeryGadget.verify_surgery_gadget steane_x_surgery_WRONG = false

def steane_x_surgery_TAU_TOO_SMALL : SurgeryGadget

theorem steane_x_surgery_TAU_TOO_SMALL_rejected :
    SurgeryGadget.verify_surgery_gadget steane_x_surgery_TAU_TOO_SMALL
      = false

def surface3_qec : QECCode

def supp678 : List Bool

def surface3_x_surgery_conn_x : BoolMat

def surface3_x_surgery_conn_z : BoolMat

def surface3_x_surgery_ancilla_hx : BoolMat

def surface3_x_surgery_ancilla_hz : BoolMat

def surface3_x_surgery : SurgeryGadget

theorem surface3_x_surgery_dimensions :
    SurgeryGadget.dimensions_consistent surface3_x_surgery = true

theorem surface3_x_surgery_tau_s :
    SurgeryGadget.tau_s_sufficient surface3_x_surgery = true

theorem surface3_x_surgery_qldpc :
    SurgeryGadget.merged_is_qldpc surface3_x_surgery = true

theorem surface3_x_surgery_targets_correctly :
    SurgeryGadget.targets_logical_correctly surface3_x_surgery = true

theorem surface3_x_surgery_verifies :
    SurgeryGadget.verify_surgery_gadget surface3_x_surgery = true

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

theorem surface3_x_surgery_checks_commute :
    ∀ p ∈ merged_stabilizers_X surface3_x_surgery,
    ∀ q ∈ merged_stabilizers_X surface3_x_surgery, p.commutes q = true

def surface3_merged_css : CSSCode

theorem surface3_merged_well_shaped : surface3_merged_css.well_shaped = true

theorem surface3_merged_is_CSS : surface3_merged_css.css_condition = true

theorem surface3_merged_syndrome_circuit_implements :
    StabilizerState.valid surface3_merged_css.toStabilizers surface3_merged_css.n = true

abbrev PhysicalResourceId : Type

abbrev PhysicalQubitId    : Type

abbrev SiteId             : Type

abbrev PatchSlotId        : Type

abbrev FactoryPortId      : Type

abbrev RoutingSiteId      : Type

structure SchedulableSurgeryGadget

def compileSurgeryGadgetRound
    (s : SchedulableSurgeryGadget) (round_idx : Nat) : List SysCall

def compileSurgeryGadgetToSysCalls
    (s : SchedulableSurgeryGadget) : List SysCall

theorem compileSurgeryGadgetRound_length
    (s : SchedulableSurgeryGadget) (r : Nat) :
    (compileSurgeryGadgetRound s r).length = 5

private theorem rounds_flatMap_length (s : SchedulableSurgeryGadget) (n : Nat) :
    ((List.range n).flatMap (compileSurgeryGadgetRound s)).length = 5 * n

theorem compileSurgeryGadgetToSysCalls_length
    (s : SchedulableSurgeryGadget) :
    (compileSurgeryGadgetToSysCalls s).length = 5 * s.gadget.tau_s + 1

def trivial_tau3_gadget : SurgeryGadget

def ge2021_basic_ppm_gadget_spec : SchedulableSurgeryGadget

theorem compile_basic_ppm_eq_existing_ppm_block :
    compileSurgeryGadgetToSysCalls ge2021_basic_ppm_gadget_spec
      = ppm_block_syscalls

theorem compile_basic_ppm_all_invariants_ok :
    all_invariants_with_factory_ports_ok
        ge2021_ppm_arch
        (compileSurgeryGadgetToSysCalls ge2021_basic_ppm_gadget_spec)
        10 1000 1000 = true

theorem surgeryGadget_cert_of_valid
    (arch : ZonedArch) (s : SchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : all_invariants_with_factory_ports_ok arch
           (compileSurgeryGadgetToSysCalls s)
           t_react_us window_us max_per_window = true) :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = arch
      ∧ cert.syscalls = compileSurgeryGadgetToSysCalls s
      ∧ cert.wallclock_us
          = scheduleWallclockUs (compileSurgeryGadgetToSysCalls s)

theorem ge2021_basic_ppm_surgery_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = ge2021_ppm_arch
      ∧ cert.syscalls
          = compileSurgeryGadgetToSysCalls ge2021_basic_ppm_gadget_spec

def surgery_ppm_A : SchedulableSurgeryGadget

def surgery_ppm_B_distinct : SchedulableSurgeryGadget

def surgery_ppm_C_distinct : SchedulableSurgeryGadget

def surgery_ppm_B_alias : SchedulableSurgeryGadget

theorem surgery_ppm_A_all_invariants_ok :
    all_invariants_with_factory_ports_ok ge2021_ppm_arch
        (compileSurgeryGadgetToSysCalls surgery_ppm_A) 10 1000 1000 = true

theorem surgery_good_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.syscalls = compileSurgeryGadgetToSysCalls surgery_ppm_A

def surgery_arch : ZonedArch

def surgery_pair_parallel_alias_syscalls : List SysCall

theorem surgery_pair_parallel_alias_rejected :
    validateScheduleWithFactoryPorts
        surgery_arch surgery_pair_parallel_alias_syscalls 10 1000 1000 = false

def surgery_pair_parallel_distinct_syscalls : List SysCall

theorem surgery_pair_parallel_distinct_all_invariants_ok :
    all_invariants_with_factory_ports_ok surgery_arch
        surgery_pair_parallel_distinct_syscalls 10 1000 1000 = true

theorem surgery_pair_parallel_distinct_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.syscalls
        = parSchedules
            (compileSurgeryGadgetToSysCalls surgery_ppm_A)
            (compileSurgeryGadgetToSysCalls surgery_ppm_B_distinct)

def surgery_triple_sequential_syscalls : List SysCall

theorem surgery_triple_sequential_all_invariants_ok :
    all_invariants_with_factory_ports_ok surgery_arch
        surgery_triple_sequential_syscalls 10 1000 1000 = true

theorem surgery_triple_sequential_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.syscalls = surgery_triple_sequential_syscalls

theorem surgery_good_wallclock_is_derived :
    scheduleWallclockUs (compileSurgeryGadgetToSysCalls surgery_ppm_A)
      = (compileSurgeryGadgetToSysCalls surgery_ppm_A).foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

theorem surgery_triple_wallclock_is_derived :
    scheduleWallclockUs surgery_triple_sequential_syscalls
      = surgery_triple_sequential_syscalls.foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

theorem surgery_good_wallclock_value :
    scheduleWallclockUs (compileSurgeryGadgetToSysCalls surgery_ppm_A) = 16

theorem surgery_triple_wallclock_value :
    scheduleWallclockUs surgery_triple_sequential_syscalls = 48

def rowEdgesAux (i : Nat) : Nat → BoolVec → List (Nat × Nat)
  | _, []           => []
  | j, true  :: rest => (i, j) :: rowEdgesAux i (j + 1) rest
  | j, false :: rest => rowEdgesAux i (j + 1) rest

def connEdgesAux : Nat → BoolMat → List (Nat × Nat)
  | _, []           => []
  | i, row :: rest  => rowEdgesAux i 0 row ++ connEdgesAux (i + 1) rest

def connEdges (conn : BoolMat) : List (Nat × Nat)

theorem connEdges_empty : connEdges ([] : BoolMat) = []

structure TopologySchedulableSurgeryGadget

def topologyRoundGateCount (s : TopologySchedulableSurgeryGadget) : Nat

def topologyRoundLength (s : TopologySchedulableSurgeryGadget) : Nat

def emitXEdgeGates
    (s : TopologySchedulableSurgeryGadget)
    (t_start : Nat)
    (edges : List (Nat × Nat)) : List SysCall

def emitZEdgeGates
    (s : TopologySchedulableSurgeryGadget)
    (t_start : Nat)
    (edges : List (Nat × Nat)) : List SysCall

def emitAncillaMeasures
    (s : TopologySchedulableSurgeryGadget) (t_start : Nat) : List SysCall

def compileTopologySurgeryRound
    (s : TopologySchedulableSurgeryGadget) (round_idx : Nat) : List SysCall

def compileTopologySurgeryToSysCalls
    (s : TopologySchedulableSurgeryGadget) : List SysCall

theorem compileTopologySurgery_wallclock_is_derived
    (s : TopologySchedulableSurgeryGadget) :
    scheduleWallclockUs (compileTopologySurgeryToSysCalls s)
      = (compileTopologySurgeryToSysCalls s).foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

def topology_demo_gadget : SurgeryGadget

theorem topology_demo_gadget_verifies :
    SurgeryGadget.verify_surgery_gadget topology_demo_gadget = true

def topology_demo : TopologySchedulableSurgeryGadget

theorem topology_demo_x_edges :
    connEdges topology_demo.gadget.conn_x = [(0, 0)]

theorem topology_demo_z_edges :
    connEdges topology_demo.gadget.conn_z = [(0, 1)]

theorem topology_demo_round_length :
    topologyRoundLength topology_demo = 6

theorem topology_demo_total_syscalls :
    (compileTopologySurgeryToSysCalls topology_demo).length = 13

theorem topology_demo_all_invariants_with_factory_ports_ok :
    all_invariants_with_factory_ports_ok surgery_arch
        (compileTopologySurgeryToSysCalls topology_demo) 10 1000 1000 = true

theorem topology_demo_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = surgery_arch
      ∧ cert.syscalls = compileTopologySurgeryToSysCalls topology_demo

theorem topology_demo_wallclock_is_derived :
    scheduleWallclockUs (compileTopologySurgeryToSysCalls topology_demo)
      = (compileTopologySurgeryToSysCalls topology_demo).foldl
          (fun acc sc => Nat.max acc sc.end_us) 0

theorem topology_demo_wallclock_value :
    scheduleWallclockUs (compileTopologySurgeryToSysCalls topology_demo) = 13

def verify_surgery_gadget_with_schedule
    (s : TopologySchedulableSurgeryGadget)
    (arch : ZonedArch)
    (t_react_us window_us max_per_window : Nat) : Bool

theorem topology_demo_combined_verifies :
    verify_surgery_gadget_with_schedule
      topology_demo surgery_arch 10 1000 1000 = true

def topology_demo_alias : TopologySchedulableSurgeryGadget

def topology_pair_alias_syscalls : List SysCall

theorem topology_pair_alias_rejected :
    validateScheduleWithFactoryPorts
        surgery_arch topology_pair_alias_syscalls 10 1000 1000 = false

def topology_demo_distinct : TopologySchedulableSurgeryGadget

def topology_pair_distinct_syscalls : List SysCall

theorem topology_pair_distinct_all_invariants_ok :
    all_invariants_with_factory_ports_ok surgery_arch
        topology_pair_distinct_syscalls 10 1000 1000 = true

theorem topology_pair_distinct_cert_exists :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.syscalls = topology_pair_distinct_syscalls

theorem verify_surgery_gadget_with_schedule_implies_gadget_ok
    (arch : ZonedArch) (s : TopologySchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : verify_surgery_gadget_with_schedule
            s arch t_react_us window_us max_per_window = true) :
    SurgeryGadget.verify_surgery_gadget s.gadget = true

theorem verify_surgery_gadget_with_schedule_implies_schedule_ok
    (arch : ZonedArch) (s : TopologySchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : verify_surgery_gadget_with_schedule
            s arch t_react_us window_us max_per_window = true) :
    SurgeryGadget.verify_surgery_schedule [s.gadget] = true

theorem verify_surgery_gadget_with_schedule_implies_system_ok
    (arch : ZonedArch) (s : TopologySchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : verify_surgery_gadget_with_schedule
            s arch t_react_us window_us max_per_window = true) :
    all_invariants_with_factory_ports_ok arch
      (compileTopologySurgeryToSysCalls s)
      t_react_us window_us max_per_window = true

theorem verify_surgery_gadget_with_schedule_cert_exists
    (arch : ZonedArch) (s : TopologySchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : verify_surgery_gadget_with_schedule
            s arch t_react_us window_us max_per_window = true) :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = arch
      ∧ cert.syscalls = compileTopologySurgeryToSysCalls s
      ∧ cert.t_react_us = t_react_us
      ∧ cert.window_us = window_us
      ∧ cert.max_per_window = max_per_window
      ∧ cert.wallclock_us

theorem verify_surgery_gadget_with_schedule_sound
    (arch : ZonedArch) (s : TopologySchedulableSurgeryGadget)
    (t_react_us window_us max_per_window : Nat)
    (h : verify_surgery_gadget_with_schedule
            s arch t_react_us window_us max_per_window = true) :
    SurgeryGadget.verify_surgery_gadget s.gadget = true
    ∧ SurgeryGadget.verify_surgery_schedule [s.gadget] = true
    ∧ all_invariants_with_factory_ports_ok arch
        (compileTopologySurgeryToSysCalls s)
        t_react_us window_us max_per_window = true
    ∧ ∃ cert : PPMScheduleCertWithFactoryPorts,
        cert.syscalls = compileTopologySurgeryToSysCalls s

def topology_demo_arch : ZonedArch

def topology_demo_t_react_us : Nat

def topology_demo_window_us : Nat

def topology_demo_max_per_window : Nat

theorem topology_demo_combined_verifies_alias :
    verify_surgery_gadget_with_schedule
      topology_demo topology_demo_arch
      topology_demo_t_react_us topology_demo_window_us
      topology_demo_max_per_window = true

theorem topology_demo_sound :
    SurgeryGadget.verify_surgery_gadget topology_demo.gadget = true
    ∧ SurgeryGadget.verify_surgery_schedule [topology_demo.gadget] = true
    ∧ all_invariants_with_factory_ports_ok topology_demo_arch
        (compileTopologySurgeryToSysCalls topology_demo)
        topology_demo_t_react_us topology_demo_window_us
        topology_demo_max_per_window = true
    ∧ ∃ cert : PPMScheduleCertWithFactoryPorts,
        cert.syscalls = compileTopologySurgeryToSysCalls topology_demo

theorem topology_demo_cert_from_combined_verifier :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = topology_demo_arch
      ∧ cert.syscalls = compileTopologySurgeryToSysCalls topology_demo
      ∧ cert.wallclock_us
          = scheduleWallclockUs (compileTopologySurgeryToSysCalls topology_demo)

def topology_steane_x : TopologySchedulableSurgeryGadget

theorem topology_steane_x_x_edges :
    connEdges topology_steane_x.gadget.conn_x = [(0, 3), (0, 5), (0, 6)]

theorem topology_steane_x_z_edges :
    connEdges topology_steane_x.gadget.conn_z = []

theorem topology_steane_x_round_length :
    topologyRoundLength topology_steane_x = 6

theorem topology_steane_x_combined_verifies :
    verify_surgery_gadget_with_schedule
      topology_steane_x topology_demo_arch
      topology_demo_t_react_us topology_demo_window_us
      topology_demo_max_per_window = true

theorem topology_steane_x_sound :
    SurgeryGadget.verify_surgery_gadget topology_steane_x.gadget = true
    ∧ SurgeryGadget.verify_surgery_schedule [topology_steane_x.gadget] = true
    ∧ all_invariants_with_factory_ports_ok topology_demo_arch
        (compileTopologySurgeryToSysCalls topology_steane_x)
        topology_demo_t_react_us topology_demo_window_us
        topology_demo_max_per_window = true
    ∧ ∃ cert : PPMScheduleCertWithFactoryPorts,
        cert.syscalls = compileTopologySurgeryToSysCalls topology_steane_x

theorem topology_steane_x_cert_from_combined_verifier :
    ∃ cert : PPMScheduleCertWithFactoryPorts,
      cert.arch = topology_demo_arch
      ∧ cert.syscalls = compileTopologySurgeryToSysCalls topology_steane_x
      ∧ cert.wallclock_us
          = scheduleWallclockUs (compileTopologySurgeryToSysCalls topology_steane_x)

theorem topology_alias_pair_system_not_ok :
    all_invariants_with_factory_ports_ok
        topology_demo_arch topology_pair_alias_syscalls
        topology_demo_t_react_us topology_demo_window_us
        topology_demo_max_per_window = false

def xRow (l : List Bool) : PauliString

theorem pmul2_xBit (a b : Bool) : pmul2 (xBit a) (xBit b) = xBit (a != b)

theorem zipmap_pmul_xBit (a b : List Bool) (h : a.length = b.length) :
    ((a.map xBit).zip (b.map xBit)).map (fun p => pmul2 p.1 p.2)
      = (vec_xor a b).map xBit

theorem xRow_vec_xor_ops (a b : List Bool) (h : a.length = b.length) :
    ((xRow a).mul (xRow b)).ops = (xRow (vec_xor a b)).ops

def merged_stabilizers_X (g : SurgeryGadget) : List PauliString

def selectedXProduct (sel : List Bool) (mat : BoolMat) : PauliString

theorem vec_xor_length (a b : BoolVec) :
    (vec_xor a b).length = min a.length b.length

theorem row_combination_length (n : Nat) :
    ∀ (sel : List Bool) (mat : BoolMat), (∀ r ∈ mat, r.length = n) →
      (row_combination sel mat = [] ∨ (row_combination sel mat).length = n)

theorem selectedXProduct_ops (n : Nat) :
    ∀ (sel : List Bool) (mat : BoolMat), (∀ r ∈ mat, r.length = n) →
      (selectedXProduct sel mat).ops = (xRow (row_combination sel mat)).ops

theorem surgery_readout_operator (g : SurgeryGadget) (n : Nat)
    (hshape : ∀ r ∈ g.merged_hx, r.length = n)
    (hker : g.targets_logical_correctly = true) :
    (selectedXProduct g.span_witness g.merged_hx).ops = (xRow g.target_pauli).ops

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

example : (selectedXProduct [true, true] [[true, false, true], [false, true, true]]).ops
    = (xRow [true, true, false]).ops

theorem runProgram_map_meas_nil (checks : List PauliString) (s : StabilizerState) :
    runProgram (checks.map StabOp.meas) [] s
      = checks.foldl (fun st P => apply_PPM_pos st P) s

theorem surgery_schedule_runs_as_merge (g : SurgeryGadget) (s : StabilizerState) :
    runProgram ((merged_stabilizers_X g).map StabOp.meas) [] s
      = measureChecks (merged_stabilizers_X g) s

theorem logical_PPM_reduces_to_surgery_schedule
    (g : SurgeryGadget) (n : Nat) (signs : List Bool)
    (hn : 0 < n) (hshape : ∀ r ∈ g.merged_hx, r.length = n)
    (hsig : signs.length = g.merged_hx.length)
    (hverify : g.verify_surgery_gadget = true) :
    -- (SCHEDULE) the surgery schedule-program IS the merge state-map
    (∀ s, runProgram ((merged_stabilizers_X g).map StabOp.meas) [] s
            = measureChecks (merged_stabilizers_X g) s)
    -- (R) its readout extracts P̄ signed by the merged-check outcome parity
    ∧ (selectedSignedProduct g.span_witness g.merged_hx signs
            = signedXRow (selectedParity g.span_witness signs) g.target_pauli)
    -- (N) it preserves the logical sector commuting with P̄ (of the EXECUTION)

theorem surgery_schedule_runs_as_merge_Z (g : SurgeryGadget) (s : StabilizerState) :
    runProgram ((merged_stabilizers_Z g).map StabOp.meas) [] s
      = measureChecks (merged_stabilizers_Z g) s

theorem logical_PPM_Z_reduces_to_surgery_schedule
    (g : SurgeryGadget) (n : Nat) (zwitness ztarget : BoolVec) (signs : List Bool)
    (hn : 0 < n) (hshape : ∀ r ∈ g.merged_hz, r.length = n)
    (hsig : signs.length = g.merged_hz.length)
    (hzker : row_combination zwitness g.merged_hz = ztarget) :
    (∀ s, runProgram ((merged_stabilizers_Z g).map StabOp.meas) [] s
            = measureChecks (merged_stabilizers_Z g) s)
    ∧ (selectedSignedZProduct zwitness g.merged_hz signs
            = signedZRow (selectedZParity zwitness signs) ztarget)
    ∧ (∀ (L : PauliString) (s : StabilizerState), L ∈ s →
         (∀ P ∈ merged_stabilizers_Z g, L.commutes P = true) →
         L ∈ runProgram ((merged_stabilizers_Z g).map StabOp.meas) [] s)

example (s : StabilizerState) :
    runProgram ([xRow [true, false], xRow [false, true]].map StabOp.meas) [] s
      = measureChecks [xRow [true, false], xRow [false, true]] s

theorem zxRun_eq_foldl (d : ZXDiagram) (s : StabilizerState) :
    zxRun d s = (d.map ZXSpider.toPauli).foldl (fun st P => apply_PPM_pos st P) s

theorem zxRun_append (d1 d2 : ZXDiagram) (s : StabilizerState) :
    zxRun (d1 ++ d2) s = zxRun d2 (zxRun d1 s)

abbrev Schedule

def scheduleProgramX (sched : Schedule) : ZXDiagram

def runScheduleX (sched : Schedule) (s : StabilizerState) : StabilizerState

theorem schedule_runs_as_surgeries (sched : Schedule) (s : StabilizerState) :
    zxRun (scheduleProgramX sched) s = runScheduleX sched s

def scheduleProgramZ (sched : Schedule) : ZXDiagram

def runScheduleZ (sched : Schedule) (s : StabilizerState) : StabilizerState

theorem schedule_runs_as_surgeries_Z (sched : Schedule) (s : StabilizerState) :
    zxRun (scheduleProgramZ sched) s = runScheduleZ sched s

def scheduleTotalRounds (sched : Schedule) : Nat

example (g h : SurgeryGadget) :
    scheduleTotalRounds [g, h] = g.tau_s + h.tau_s