theorem adder_n1_repeated_10_expanded_strict_ok :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        adder_n1_system_models.arch
        adder_n1_system_models.opCap
        adder_n1_system_models.slotCap
        adder_n1_system_models.ancillaModel
        (CompressedSchedule.rep 10 (CompressedSchedule.atom adder_n1_syscalls)).expand
        adder_n1_system_models.t_react_us
        adder_n1_system_models.window_us
        adder_n1_system_models.max_per_window = true

theorem adder_n1_repeated_1000000_symbolic_ok :
    symbolic_rep_strict_ok
        adder_n1_system_models adder_n1_syscalls 1000000 = true

theorem adder_n1_repeated_1000000_resource_wallclock :
    (CompressedSchedule.rep 1000000
        (CompressedSchedule.atom adder_n1_syscalls)).resource.wallclock_us
      = 48000000

theorem adder_n1_repeated_1000000_resource_gate2q :
    (CompressedSchedule.rep 1000000
        (CompressedSchedule.atom adder_n1_syscalls)).resource.gate2q_count
      = 18000000

theorem adder_n1_repeated_1000000_resource_syscall_count :
    (CompressedSchedule.rep 1000000
        (CompressedSchedule.atom adder_n1_syscalls)).resource.syscall_count
      = 48000000

theorem adder_n1_scheduleWithinWallclock :
    scheduleWithinWallclock adder_n1_syscalls = true

private def adder_seq2 : List SysCall

theorem adder_seq2_length : adder_seq2.length = 96

theorem adder_seq2_wallclock : scheduleWallclockUs adder_seq2 = 96

theorem adder_seq2_exclusivity_ok :
    exclusivity_ok adder_seq2 = true

theorem adder_seq2_factory_exclusivity_ok :
    factory_exclusivity_ok adder_seq2 = true

theorem adder_seq2_operation_capacity_ok :
    operation_capacity_ok
        adder_n1_system_models.opCap adder_seq2 = true

theorem adder_seq2_slot_capacity_ok :
    slot_capacity_ok
        adder_n1_system_models.slotCap adder_seq2 = true

theorem adder_seq2_obligation_A_ok :
    exclusivity_ok adder_seq2 = true
    ∧ factory_exclusivity_ok adder_seq2 = true
    ∧ operation_capacity_ok adder_n1_system_models.opCap adder_seq2 = true
    ∧ slot_capacity_ok adder_n1_system_models.slotCap adder_seq2 = true

private def adder_seq3 : List SysCall

theorem adder_seq3_length : adder_seq3.length = 144

theorem adder_seq3_wallclock : scheduleWallclockUs adder_seq3 = 144

theorem adder_seq3_obligation_A_ok :
    exclusivity_ok adder_seq3 = true
    ∧ factory_exclusivity_ok adder_seq3 = true
    ∧ operation_capacity_ok adder_n1_system_models.opCap adder_seq3 = true
    ∧ slot_capacity_ok adder_n1_system_models.slotCap adder_seq3 = true

theorem adder_repeated_100_feedback_after_decode_ok :
    feedback_after_decode_ok
        (CompressedSchedule.rep 100 (CompressedSchedule.atom adder_n1_syscalls)).expand
      = true

def feedback_bad_body_for_repeat : List SysCall

theorem feedback_bad_body_fails_feedback_check :
    feedback_after_decode_ok feedback_bad_body_for_repeat = false

theorem feedback_bad_body_repeat_symbolic_rejected :
    symbolic_rep_strict_ok
        adder_n1_system_models feedback_bad_body_for_repeat 10 = false

theorem adder_repeated_3_ancilla_freshness_ok :
    ancilla_freshness_ok
        adder_n1_system_models.ancillaModel
        (CompressedSchedule.rep 3 (CompressedSchedule.atom adder_n1_syscalls)).expand
      = true

theorem adder_repeated_10_ancilla_freshness_ok :
    ancilla_freshness_ok
        adder_n1_system_models.ancillaModel
        (CompressedSchedule.rep 10 (CompressedSchedule.atom adder_n1_syscalls)).expand
      = true

def freshness_bad_body_for_repeat : List SysCall

theorem freshness_bad_body_fails_freshness_check :
    ancilla_freshness_ok
        adder_n1_system_models.ancillaModel freshness_bad_body_for_repeat = false

theorem freshness_bad_body_repeat_symbolic_rejected :
    symbolic_rep_strict_ok
        adder_n1_system_models freshness_bad_body_for_repeat 10 = false

theorem countActiveKindAt_append
    (pred : SysCallKind → Bool) (t : Nat) (xs ys : List SysCall) :
    countActiveKindAt pred t (xs ++ ys)
      = countActiveKindAt pred t xs + countActiveKindAt pred t ys

theorem countActiveKindAt_shiftSchedule
    (pred : SysCallKind → Bool) (t dt : Nat) (xs : List SysCall) :
    countActiveKindAt pred (t + dt) (shiftSchedule dt xs)
      = countActiveKindAt pred t xs

theorem countActiveKindAt_eq_zero_of_within_wallclock_at_or_after
    (pred : SysCallKind → Bool) (t : Nat) (xs : List SysCall)
    (hwithin : scheduleWithinWallclock xs = true)
    (h : scheduleWallclockUs xs ≤ t) :
    countActiveKindAt pred t xs = 0

theorem countActiveKindAt_shiftSchedule_eq_zero_before_offset
    (pred : SysCallKind → Bool) (t dt : Nat) (ys : List SysCall)
    (h : t < dt) :
    countActiveKindAt pred t (shiftSchedule dt ys) = 0

private def op_cap_check_at (opCap : OperationCapacityModel)
    (L : List SysCall) (t : Nat) : Bool

private theorem operation_capacity_ok_eq
    (opCap : OperationCapacityModel) (L : List SysCall) :
    operation_capacity_ok opCap L
      = (scheduleEventTimes L).all (op_cap_check_at opCap L)

private theorem op_cap_check_at_mono
    (opCap : OperationCapacityModel) (L L' : List SysCall) (t : Nat)
    (h1 : countActiveKindAt kindIsGate1q t L' ≤ countActiveKindAt kindIsGate1q t L)
    (h2 : countActiveKindAt kindIsGate2q t L' ≤ countActiveKindAt kindIsGate2q t L)
    (h3 : countActiveKindAt kindIsMeasure t L' ≤ countActiveKindAt kindIsMeasure t L)
    (h4 : countActiveKindAt kindIsDecode t L' ≤ countActiveKindAt kindIsDecode t L)
    (h5 : countActiveKindAt kindIsFeedback t L' ≤ countActiveKindAt kindIsFeedback t L)
    (h6 : countActiveKindAt kindIsMagicReq t L' ≤ countActiveKindAt kindIsMagicReq t L)
    (h7 : countActiveKindAt kindIsFreshAnc t L' ≤ countActiveKindAt kindIsFreshAnc t L)
    (h8 : countActiveKindAt kindIsTransit t L' ≤ countActiveKindAt kindIsTransit t L)
    (hL : op_cap_check_at opCap L t = true) :
    op_cap_check_at opCap L' t = true

private theorem op_cap_check_at_shiftSchedule
    (opCap : OperationCapacityModel) (xs : List SysCall) (t dt : Nat) :
    op_cap_check_at opCap (shiftSchedule dt xs) (t + dt)
      = op_cap_check_at opCap xs t

theorem operation_capacity_ok_shiftSchedule_eq
    (opCap : OperationCapacityModel) (dt : Nat) (xs : List SysCall) :
    operation_capacity_ok opCap (shiftSchedule dt xs)
      = operation_capacity_ok opCap xs

theorem operation_capacity_ok_seqSchedules
    (opCap : OperationCapacityModel) (xs ys : List SysCall)
    (hxs : operation_capacity_ok opCap xs = true)
    (hys : operation_capacity_ok opCap ys = true)
    (hwithin : scheduleWithinWallclock xs = true) :
    operation_capacity_ok opCap (seqSchedules xs ys) = true

theorem operation_capacity_ok_seqMany_replicate_block
    (opCap : OperationCapacityModel) (block : List SysCall) (n : Nat)
    (hblock : operation_capacity_ok opCap block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    operation_capacity_ok opCap (seqManySchedules (List.replicate n block)) = true

theorem operation_capacity_ok_repeated_block_expand
    (opCap : OperationCapacityModel) (block : List SysCall) (n : Nat)
    (hblock : operation_capacity_ok opCap block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    operation_capacity_ok opCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem activeSitesAt_append (t : Nat) (xs ys : List SysCall) :
    activeSitesAt t (xs ++ ys)
      = activeSitesAt t xs ++ activeSitesAt t ys

theorem activeSitesAt_shiftSchedule (t dt : Nat) (xs : List SysCall) :
    activeSitesAt (t + dt) (shiftSchedule dt xs) = activeSitesAt t xs

theorem activeSitesAt_eq_nil_of_within_wallclock_at_or_after
    (t : Nat) (xs : List SysCall)
    (hwithin : scheduleWithinWallclock xs = true)
    (h : scheduleWallclockUs xs ≤ t) :
    activeSitesAt t xs = []

theorem activeSitesAt_shiftSchedule_eq_nil_before_offset
    (t dt : Nat) (ys : List SysCall) (h : t < dt) :
    activeSitesAt t (shiftSchedule dt ys) = []

theorem activeSiteCountInZoneAt_append
    (z : ZoneCapacitySpec) (t : Nat) (xs ys : List SysCall) :
    activeSiteCountInZoneAt z t (xs ++ ys)
      = activeSiteCountInZoneAt z t xs + activeSiteCountInZoneAt z t ys

theorem activeSiteCountInZoneAt_shiftSchedule
    (z : ZoneCapacitySpec) (t dt : Nat) (xs : List SysCall) :
    activeSiteCountInZoneAt z (t + dt) (shiftSchedule dt xs)
      = activeSiteCountInZoneAt z t xs

theorem activeSiteCountInZoneAt_eq_zero_of_within_wallclock_at_or_after
    (z : ZoneCapacitySpec) (t : Nat) (xs : List SysCall)
    (hwithin : scheduleWithinWallclock xs = true)
    (h : scheduleWallclockUs xs ≤ t) :
    activeSiteCountInZoneAt z t xs = 0

theorem activeSiteCountInZoneAt_shiftSchedule_eq_zero_before_offset
    (z : ZoneCapacitySpec) (t dt : Nat) (ys : List SysCall)
    (h : t < dt) :
    activeSiteCountInZoneAt z t (shiftSchedule dt ys) = 0

private def slot_cap_check_at (slotCap : SlotCapacityModel)
    (L : List SysCall) (t : Nat) : Bool

private theorem slot_capacity_ok_eq
    (slotCap : SlotCapacityModel) (L : List SysCall) :
    slot_capacity_ok slotCap L
      = (scheduleEventTimes L).all (slot_cap_check_at slotCap L)

private theorem slot_cap_check_at_shiftSchedule
    (slotCap : SlotCapacityModel) (xs : List SysCall) (t dt : Nat) :
    slot_cap_check_at slotCap (shiftSchedule dt xs) (t + dt)
      = slot_cap_check_at slotCap xs t

theorem slot_capacity_ok_shiftSchedule_eq
    (slotCap : SlotCapacityModel) (dt : Nat) (xs : List SysCall) :
    slot_capacity_ok slotCap (shiftSchedule dt xs)
      = slot_capacity_ok slotCap xs

theorem slot_capacity_ok_seqSchedules
    (slotCap : SlotCapacityModel) (xs ys : List SysCall)
    (hxs : slot_capacity_ok slotCap xs = true)
    (hys : slot_capacity_ok slotCap ys = true)
    (hwithin : scheduleWithinWallclock xs = true) :
    slot_capacity_ok slotCap (seqSchedules xs ys) = true

theorem slot_capacity_ok_seqMany_replicate_block
    (slotCap : SlotCapacityModel) (block : List SysCall) (n : Nat)
    (hblock : slot_capacity_ok slotCap block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    slot_capacity_ok slotCap (seqManySchedules (List.replicate n block)) = true

theorem slot_capacity_ok_repeated_block_expand
    (slotCap : SlotCapacityModel) (block : List SysCall) (n : Nat)
    (hblock : slot_capacity_ok slotCap block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    slot_capacity_ok slotCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem compressed_schedule_cert_repeated_leaf_eq_symbolic_rep_strict_ok_within
    (models : SystemModels) (block : List SysCall) (n : Nat) :
    compressed_schedule_strict_certificate_ok models
        (CompressedSchedule.rep n (CompressedSchedule.atom block))
      = symbolic_rep_strict_ok_within models block n

theorem compressed_schedule_cert_repeated_leaf_of_symbolic_rep_strict_ok_within
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok_within models block n = true) :
    compressed_schedule_strict_certificate_ok models
        (CompressedSchedule.rep n (CompressedSchedule.atom block)) = true

theorem compressed_schedule_cert_leaf_eq_strict_within_and_no_magic
    (models : SystemModels) (block : List SysCall) :
    compressed_schedule_strict_certificate_ok models
        (CompressedSchedule.atom block)
      = (all_invariants_strict_with_slot_capacity_and_freshness_ok
            models.arch models.opCap models.slotCap models.ancillaModel block
            models.t_react_us models.window_us models.max_per_window
         && scheduleWithinWallclock block
         && decide ((block.filter (fun sc => kindIsMagicReq sc.kind)).length = 0))

theorem compressed_schedule_strict_soundness_repeated_leaf
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hCert :
      compressed_schedule_strict_certificate_ok models
          (CompressedSchedule.rep n (CompressedSchedule.atom block)) = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand
        models.t_react_us

theorem compressed_schedule_strict_soundness_leaf
    (models : SystemModels) (block : List SysCall)
    (hCert :
      compressed_schedule_strict_certificate_ok models
          (CompressedSchedule.atom block) = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.atom block).expand
        models.t_react_us

private theorem foldl_max_end_us_ge_acc
    (xs : List SysCall) (acc : Nat) :
    acc ≤ xs.foldl (fun a s => Nat.max a s.end_us) acc

private theorem foldl_max_end_us_ge_of_mem
    (xs : List SysCall) (sc : SysCall) (h : sc ∈ xs) (acc : Nat) :
    sc.end_us ≤ xs.foldl (fun a s => Nat.max a s.end_us) acc

theorem end_us_le_scheduleWallclockUs
    (xs : List SysCall) (sc : SysCall) (h : sc ∈ xs) :
    sc.end_us ≤ scheduleWallclockUs xs

theorem scheduleWithinWallclock_seqSchedules
    (xs ys : List SysCall)
    (hxs : scheduleWithinWallclock xs = true)
    (hys : scheduleWithinWallclock ys = true) :
    scheduleWithinWallclock (seqSchedules xs ys) = true

theorem scheduleWithinWallclock_seqMany_replicate_block
    (block : List SysCall) (n : Nat)
    (hblock : scheduleWithinWallclock block = true) :
    scheduleWithinWallclock (seqManySchedules (List.replicate n block)) = true

theorem scheduleWithinWallclock_repeated_block_expand
    (block : List SysCall) (n : Nat)
    (hblock : scheduleWithinWallclock block = true) :
    scheduleWithinWallclock
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem magic_count_seqSchedules (xs ys : List SysCall) :
    ((seqSchedules xs ys).filter (fun sc => kindIsMagicReq sc.kind)).length
      = (xs.filter (fun sc => kindIsMagicReq sc.kind)).length
        + (ys.filter (fun sc => kindIsMagicReq sc.kind)).length

theorem window_throughput_ok_seqSchedules_of_no_magic
    (xs ys : List SysCall) (window_us max_per_window : Nat)
    (hxs : (xs.filter (fun sc => kindIsMagicReq sc.kind)).length = 0)
    (hys : (ys.filter (fun sc => kindIsMagicReq sc.kind)).length = 0) :
    window_throughput_ok (seqSchedules xs ys) window_us max_per_window = true

theorem all_invariants_strict_with_slot_capacity_and_freshness_ok_seqSchedules
    (models : SystemModels) (xs ys : List SysCall)
    (hxs :
      all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch models.opCap models.slotCap models.ancillaModel xs
        models.t_react_us models.window_us models.max_per_window = true)
    (hys :
      all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch models.opCap models.slotCap models.ancillaModel ys
        models.t_react_us models.window_us models.max_per_window = true)
    (hwithin_xs : scheduleWithinWallclock xs = true)
    (hnoMagic_xs :

theorem expand_seq_cons (c : CompressedSchedule) (rest : List CompressedSchedule) :
    (CompressedSchedule.seq (c :: rest)).expand
      = seqSchedules c.expand (CompressedSchedule.seq rest).expand

theorem strict_bundle_empty (models : SystemModels) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch models.opCap models.slotCap models.ancillaModel
        []
        models.t_react_us models.window_us models.max_per_window = true

theorem scheduleWithinWallclock_empty :
    scheduleWithinWallclock ([] : List SysCall) = true

theorem magic_count_empty :
    (([] : List SysCall).filter (fun sc => kindIsMagicReq sc.kind)).length = 0

theorem compressed_schedule_strict_soundness_seq
    (models : SystemModels) (children : List CompressedSchedule)
    (hCert :
      compressed_schedule_strict_certificate_ok models
          (CompressedSchedule.seq children) = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.seq children).expand
        models.t_react_us

theorem compressed_schedule_strict_soundness
    (models : SystemModels) (cs : CompressedSchedule)
    (hCert : compressed_schedule_strict_certificate_ok models cs = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        cs.expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

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

theorem shiftSchedule_getElem? (dt : Nat) (xs : List SysCall) (i : Nat) :
    (shiftSchedule dt xs)[i]? = Option.map (shiftSysCall dt) (xs[i]?)

private theorem exclusivity_pair_eq_shift
    (dt : Nat) (xs : List SysCall) (i j : Nat) :
    (match (shiftSchedule dt xs)[i]?, (shiftSchedule dt xs)[j]? with
     | some s_i, some s_j =>
         if intervals_overlap s_i.begin_us s_i.end_us
                              s_j.begin_us s_j.end_us = true then
           atoms_disjoint (syscall_acts_on s_i) (syscall_acts_on s_j)
         else true
     | _, _ => true)
      = (match xs[i]?, xs[j]? with
         | some s_i, some s_j =>
             if intervals_overlap s_i.begin_us s_i.end_us

theorem exclusivity_ok_shiftSchedule_eq (dt : Nat) (xs : List SysCall) :
    exclusivity_ok (shiftSchedule dt xs) = exclusivity_ok xs

private def excl_pair_check (L : List SysCall) (i j : Nat) : Bool

private theorem exclusivity_ok_of_pair_check (L : List SysCall)
    (h : ∀ i j, i < j → j < L.length → excl_pair_check L i j = true) :
    exclusivity_ok L = true

private theorem excl_pair_check_of_exclusivity_ok (L : List SysCall)
    (hL : exclusivity_ok L = true) (i j : Nat) (hij : i < j) (hj : j < L.length) :
    excl_pair_check L i j = true

private theorem excl_pair_check_shiftSchedule
    (dt : Nat) (L : List SysCall) (i j : Nat) :
    excl_pair_check (shiftSchedule dt L) i j = excl_pair_check L i j

theorem exclusivity_ok_seqSchedules
    (xs ys : List SysCall)
    (hxs : exclusivity_ok xs = true)
    (hys : exclusivity_ok ys = true)
    (hwithin : scheduleWithinWallclock xs = true) :
    exclusivity_ok (seqSchedules xs ys) = true

theorem exclusivity_ok_seqMany_replicate_block
    (block : List SysCall) (n : Nat)
    (hblock : exclusivity_ok block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    exclusivity_ok (seqManySchedules (List.replicate n block)) = true

theorem exclusivity_ok_repeated_block_expand
    (block : List SysCall) (n : Nat)
    (hblock : exclusivity_ok block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

private theorem factory_exclusivity_pair_eq_shift
    (dt : Nat) (xs : List SysCall) (i j : Nat) :
    (match (shiftSchedule dt xs)[i]?, (shiftSchedule dt xs)[j]? with
     | some s_i, some s_j =>
         if intervals_overlap s_i.begin_us s_i.end_us
                              s_j.begin_us s_j.end_us = true then
           atoms_disjoint (syscall_factory_claims s_i)
                          (syscall_factory_claims s_j)
         else true
     | _, _ => true)
      = (match xs[i]?, xs[j]? with
         | some s_i, some s_j =>

theorem factory_exclusivity_ok_shiftSchedule_eq (dt : Nat) (xs : List SysCall) :
    factory_exclusivity_ok (shiftSchedule dt xs) = factory_exclusivity_ok xs

private def factory_excl_pair_check (L : List SysCall) (i j : Nat) : Bool

private theorem factory_exclusivity_ok_of_pair_check (L : List SysCall)
    (h : ∀ i j, i < j → j < L.length → factory_excl_pair_check L i j = true) :
    factory_exclusivity_ok L = true

private theorem factory_excl_pair_check_of_factory_exclusivity_ok
    (L : List SysCall) (hL : factory_exclusivity_ok L = true)
    (i j : Nat) (hij : i < j) (hj : j < L.length) :
    factory_excl_pair_check L i j = true

private theorem factory_excl_pair_check_shiftSchedule
    (dt : Nat) (L : List SysCall) (i j : Nat) :
    factory_excl_pair_check (shiftSchedule dt L) i j
      = factory_excl_pair_check L i j

theorem factory_exclusivity_ok_seqSchedules
    (xs ys : List SysCall)
    (hxs : factory_exclusivity_ok xs = true)
    (hys : factory_exclusivity_ok ys = true)
    (hwithin : scheduleWithinWallclock xs = true) :
    factory_exclusivity_ok (seqSchedules xs ys) = true

theorem factory_exclusivity_ok_seqMany_replicate_block
    (block : List SysCall) (n : Nat)
    (hblock : factory_exclusivity_ok block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    factory_exclusivity_ok (seqManySchedules (List.replicate n block)) = true

theorem factory_exclusivity_ok_repeated_block_expand
    (block : List SysCall) (n : Nat)
    (hblock : factory_exclusivity_ok block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    factory_exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

def decode_matches_feedback (cid b : Nat) (d : SysCall) : Bool

theorem decode_matches_feedback_shift_same
    (cid b dt : Nat) (d : SysCall) :
    decode_matches_feedback cid (b + dt) (shiftSysCall dt d)
      = decode_matches_feedback cid b d

theorem any_decode_matches_feedback_shift_same
    (cid b dt : Nat) (xs : List SysCall) :
    (shiftSchedule dt xs).any (decode_matches_feedback cid (b + dt))
      = xs.any (decode_matches_feedback cid b)

theorem feedback_after_decode_ok_shiftSchedule
    (dt : Nat) (xs : List SysCall) :
    feedback_after_decode_ok (shiftSchedule dt xs)
      = feedback_after_decode_ok xs

theorem feedback_after_decode_ok_shiftSchedule_of_ok
    (dt : Nat) (xs : List SysCall)
    (h : feedback_after_decode_ok xs = true) :
    feedback_after_decode_ok (shiftSchedule dt xs) = true

theorem List_any_append_left
    {α : Type _} (xs ys : List α) (p : α → Bool)
    (h : xs.any p = true) :
    (xs ++ ys).any p = true

theorem List_any_append_right
    {α : Type _} (xs ys : List α) (p : α → Bool)
    (h : ys.any p = true) :
    (xs ++ ys).any p = true

theorem feedback_after_decode_ok_append
    (xs ys : List SysCall)
    (hxs : feedback_after_decode_ok xs = true)
    (hys : feedback_after_decode_ok ys = true) :
    feedback_after_decode_ok (xs ++ ys) = true

theorem feedback_after_decode_ok_seqSchedules
    (xs ys : List SysCall)
    (hxs : feedback_after_decode_ok xs = true)
    (hys : feedback_after_decode_ok ys = true) :
    feedback_after_decode_ok (seqSchedules xs ys) = true

theorem feedback_after_decode_ok_seqMany_replicate
    (body : List SysCall) (n : Nat)
    (hbody : feedback_after_decode_ok body = true) :
    feedback_after_decode_ok
        (seqManySchedules (List.replicate n body)) = true

theorem feedback_after_decode_ok_repeated_atom_expand
    (body : List SysCall) (n : Nat)
    (hbody : feedback_after_decode_ok body = true) :
    feedback_after_decode_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom body)).expand = true

theorem symbolic_rep_ok_implies_body_feedback_after_decode_ok
    (models : SystemModels) (body : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok models body n = true) :
    feedback_after_decode_ok body = true

theorem symbolic_rep_implies_expanded_feedback_after_decode_ok
    (models : SystemModels) (body : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok models body n = true) :
    feedback_after_decode_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom body)).expand = true

def lifecycleEquivalent (a b : SiteLifecycle) : Bool

def state_equivalent
    (s1 s2 : List (Nat × SiteLifecycle)) : Prop

theorem state_equivalent_refl (s : List (Nat × SiteLifecycle)) :
    state_equivalent s s

theorem state_equivalent_symm
    {s1 s2 : List (Nat × SiteLifecycle)}
    (h : state_equivalent s1 s2) : state_equivalent s2 s1

theorem state_equivalent_live_iff
    {s1 s2 : List (Nat × SiteLifecycle)} (site : Nat)
    (h : state_equivalent s1 s2) :
    (lifecycleOf s1 site = SiteLifecycle.Live)
      ↔ (lifecycleOf s2 site = SiteLifecycle.Live)

theorem isLive_eq_under_state_equivalent
    {s1 s2 : List (Nat × SiteLifecycle)} (site : Nat)
    (h : state_equivalent s1 s2) :
    (match lifecycleOf s1 site with | .Live => true | _ => false)
      = (match lifecycleOf s2 site with | .Live => true | _ => false)

def stateNormalized (s : List (Nat × SiteLifecycle)) : Prop

theorem stateNormalized_nil :
    stateNormalized ([] : List (Nat × SiteLifecycle))

theorem lifecycleOf_nil (site : Nat) :
    lifecycleOf ([] : List (Nat × SiteLifecycle)) site = SiteLifecycle.Free

theorem noDanglingLive_implies_state_equivalent_empty
    (s : List (Nat × SiteLifecycle))
    (h : noDanglingLive s = true) :
    state_equivalent s []

def dropSite (s : List (Nat × SiteLifecycle)) (site : Nat) : List (Nat × SiteLifecycle)

def setLifecycleBool (s : List (Nat × SiteLifecycle)) (site : Nat)
    (lc : SiteLifecycle) : List (Nat × SiteLifecycle)

theorem setLifecycle_eq_setLifecycleBool
    (s : List (Nat × SiteLifecycle)) (site : Nat) (lc : SiteLifecycle) :
    setLifecycle s site lc = setLifecycleBool s site lc

theorem mem_dropSite_iff
    {s : List (Nat × SiteLifecycle)} {site : Nat}
    {p : Nat × SiteLifecycle} :
    p ∈ dropSite s site ↔ p ∈ s ∧ p.1 ≠ site

theorem not_mem_dropSite_same
    {s : List (Nat × SiteLifecycle)} {site : Nat} :
    ∀ p ∈ dropSite s site, p.1 ≠ site

private theorem find?_dropSite_eq_none
    (s : List (Nat × SiteLifecycle)) (site : Nat) :
    (dropSite s site).find? (fun p => decide (p.1 = site)) = none

theorem lifecycleOf_setLifecycleBool_same
    (s : List (Nat × SiteLifecycle)) (site : Nat) (lc : SiteLifecycle) :
    lifecycleOf (setLifecycleBool s site lc) site = lc

private theorem find?_dropSite_other
    (s : List (Nat × SiteLifecycle)) (site site' : Nat) (hne : site' ≠ site) :
    (dropSite s site).find? (fun p => decide (p.1 = site'))
      = s.find? (fun p => decide (p.1 = site'))

theorem lifecycleOf_setLifecycleBool_other
    (s : List (Nat × SiteLifecycle)) (site site' : Nat) (lc : SiteLifecycle)
    (hne : site' ≠ site) :
    lifecycleOf (setLifecycleBool s site lc) site' = lifecycleOf s site'

theorem lifecycleOf_setLifecycle_same
    (s : List (Nat × SiteLifecycle)) (site : Nat) (lc : SiteLifecycle) :
    lifecycleOf (setLifecycle s site lc) site = lc

theorem lifecycleOf_setLifecycle_other
    (s : List (Nat × SiteLifecycle)) (site site' : Nat) (lc : SiteLifecycle)
    (hne : site' ≠ site) :
    lifecycleOf (setLifecycle s site lc) site' = lifecycleOf s site'

theorem stateNormalized_dropSite
    {s : List (Nat × SiteLifecycle)} (h : stateNormalized s)
    (site : Nat) :
    stateNormalized (dropSite s site)

theorem stateNormalized_setLifecycleBool
    {s : List (Nat × SiteLifecycle)} (h : stateNormalized s)
    (site : Nat) (lc : SiteLifecycle) :
    stateNormalized (setLifecycleBool s site lc)

theorem stateNormalized_setLifecycle
    {s : List (Nat × SiteLifecycle)} (h : stateNormalized s)
    (site : Nat) (lc : SiteLifecycle) :
    stateNormalized (setLifecycle s site lc)

theorem freshnessStep_result_form
    (model : AncillaModel) (state : List (Nat × SiteLifecycle))
    (sc : SysCall) (state' : List (Nat × SiteLifecycle))
    (hStep : freshnessStep model state sc = some state') :
    state' = state ∨ ∃ site lc, state' = setLifecycle state site lc

theorem freshnessStep_preserves_stateNormalized
    (model : AncillaModel) (state : List (Nat × SiteLifecycle))
    (sc : SysCall) (state' : List (Nat × SiteLifecycle))
    (hNorm : stateNormalized state)
    (hStep : freshnessStep model state sc = some state') :
    stateNormalized state'

theorem runFreshness_preserves_stateNormalized
    (model : AncillaModel) (sched : List SysCall)
    (state : List (Nat × SiteLifecycle))
    (state' : List (Nat × SiteLifecycle))
    (hNorm : stateNormalized state)
    (hRun : runFreshness model state sched = some state') :
    stateNormalized state'

theorem state_equivalent_set_same
    {s1 s2 : List (Nat × SiteLifecycle)}
    (h : state_equivalent s1 s2)
    (site : Nat) (lc : SiteLifecycle) :
    state_equivalent
        (setLifecycle s1 site lc) (setLifecycle s2 site lc)

theorem freshnessStep_state_equivalent
    (model : AncillaModel) (sc : SysCall)
    (s1 s2 s1' s2' : List (Nat × SiteLifecycle))
    (hEq : state_equivalent s1 s2)
    (h1 : freshnessStep model s1 sc = some s1')
    (h2 : freshnessStep model s2 sc = some s2') :
    state_equivalent s1' s2'

theorem runFreshness_state_equivalent
    (model : AncillaModel) (sched : List SysCall)
    (s1 s2 s1' s2' : List (Nat × SiteLifecycle))
    (hEq : state_equivalent s1 s2)
    (h1 : runFreshness model s1 sched = some s1')
    (h2 : runFreshness model s2 sched = some s2') :
    state_equivalent s1' s2'

theorem lifecycleOf_eq_of_mem_normalized
    {s : List (Nat × SiteLifecycle)} (hnorm : stateNormalized s)
    {p : Nat × SiteLifecycle} (hp : p ∈ s) :
    lifecycleOf s p.1 = p.2

theorem state_equivalent_empty_implies_noDanglingLive
    (s : List (Nat × SiteLifecycle))
    (h : state_equivalent s []) (hnorm : stateNormalized s) :
    noDanglingLive s = true

theorem state_equivalent_trans
    {s1 s2 s3 : List (Nat × SiteLifecycle)}
    (h12 : state_equivalent s1 s2) (h23 : state_equivalent s2 s3) :
    state_equivalent s1 s3

theorem runFreshness_append
    (model : AncillaModel) (state : List (Nat × SiteLifecycle))
    (xs ys : List SysCall) :
    runFreshness model state (xs ++ ys)
      = (match runFreshness model state xs with
         | none => none
         | some state' => runFreshness model state' ys)

theorem freshnessStep_state_equivalent_some_form
    (model : AncillaModel) (sc : SysCall)
    (s1 s2 t2 : List (Nat × SiteLifecycle))
    (hEq : state_equivalent s1 s2)
    (h2 : freshnessStep model s2 sc = some t2) :
    ∃ t1, freshnessStep model s1 sc = some t1 ∧ state_equivalent t1 t2

theorem runFreshness_state_equivalent_some_form
    (model : AncillaModel) (sched : List SysCall)
    (s1 s2 s2' : List (Nat × SiteLifecycle))
    (hEq : state_equivalent s1 s2)
    (h2 : runFreshness model s2 sched = some s2') :
    ∃ s1', runFreshness model s1 sched = some s1' ∧ state_equivalent s1' s2'

theorem ancilla_freshness_ok_seqSchedules
    (model : AncillaModel) (xs ys : List SysCall)
    (hxs : ancilla_freshness_ok model xs = true)
    (hys : ancilla_freshness_ok model ys = true) :
    ancilla_freshness_ok model (seqSchedules xs ys) = true

theorem ancilla_freshness_ok_seqMany_replicate_block
    (model : AncillaModel) (block : List SysCall) (n : Nat)
    (hblock : ancilla_freshness_ok model block = true) :
    ancilla_freshness_ok model
        (seqManySchedules (List.replicate n block)) = true

theorem ancilla_freshness_ok_repeated_block_expand
    (model : AncillaModel) (block : List SysCall) (n : Nat)
    (hblock : ancilla_freshness_ok model block = true) :
    ancilla_freshness_ok model
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_ok_implies_body_ancilla_freshness_ok
    (models : SystemModels) (body : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok models body n = true) :
    ancilla_freshness_ok models.ancillaModel body = true

theorem symbolic_rep_implies_expanded_block_ancilla_freshness_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    ancilla_freshness_ok models.ancillaModel
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem capacity_in_arch_ok_seqSchedules
    (arch : ZonedArch) (xs ys : List SysCall)
    (hxs : capacity_in_arch_ok arch xs = true)
    (hys : capacity_in_arch_ok arch ys = true) :
    capacity_in_arch_ok arch (seqSchedules xs ys) = true

theorem capacity_in_arch_ok_seqMany_replicate_block
    (arch : ZonedArch) (block : List SysCall) (n : Nat)
    (hblock : capacity_in_arch_ok arch block = true) :
    capacity_in_arch_ok arch
        (seqManySchedules (List.replicate n block)) = true

theorem capacity_in_arch_ok_repeated_block_expand
    (arch : ZonedArch) (block : List SysCall) (n : Nat)
    (hblock : capacity_in_arch_ok arch block = true) :
    capacity_in_arch_ok arch
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem feedback_latency_ok_seqSchedules
    (t_cycle_us : Nat) (xs ys : List SysCall)
    (hxs : feedback_latency_ok t_cycle_us xs = true)
    (hys : feedback_latency_ok t_cycle_us ys = true) :
    feedback_latency_ok t_cycle_us (seqSchedules xs ys) = true

theorem feedback_latency_ok_seqMany_replicate_block
    (t_cycle_us : Nat) (block : List SysCall) (n : Nat)
    (hblock : feedback_latency_ok t_cycle_us block = true) :
    feedback_latency_ok t_cycle_us
        (seqManySchedules (List.replicate n block)) = true

theorem feedback_latency_ok_repeated_block_expand
    (t_cycle_us : Nat) (block : List SysCall) (n : Nat)
    (hblock : feedback_latency_ok t_cycle_us block = true) :
    feedback_latency_ok t_cycle_us
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem decoder_react_ok_seqSchedules
    (t_react_us : Nat) (xs ys : List SysCall)
    (hxs : decoder_react_ok t_react_us xs = true)
    (hys : decoder_react_ok t_react_us ys = true) :
    decoder_react_ok t_react_us (seqSchedules xs ys) = true

theorem decoder_react_ok_seqMany_replicate_block
    (t_react_us : Nat) (block : List SysCall) (n : Nat)
    (hblock : decoder_react_ok t_react_us block = true) :
    decoder_react_ok t_react_us
        (seqManySchedules (List.replicate n block)) = true

theorem decoder_react_ok_repeated_block_expand
    (t_react_us : Nat) (block : List SysCall) (n : Nat)
    (hblock : decoder_react_ok t_react_us block = true) :
    decoder_react_ok t_react_us
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem magic_count_append (xs ys : List SysCall) :
    ((xs ++ ys).filter (fun sc => kindIsMagicReq sc.kind)).length
      = (xs.filter (fun sc => kindIsMagicReq sc.kind)).length
        + (ys.filter (fun sc => kindIsMagicReq sc.kind)).length

theorem magic_count_seqMany_replicate
    (block : List SysCall) (n : Nat)
    (h : (block.filter (fun sc => kindIsMagicReq sc.kind)).length = 0) :
    ((seqManySchedules (List.replicate n block)).filter
        (fun sc => kindIsMagicReq sc.kind)).length = 0

theorem magic_count_repeated_block_expand
    (block : List SysCall) (n : Nat)
    (h : (block.filter (fun sc => kindIsMagicReq sc.kind)).length = 0) :
    (((CompressedSchedule.rep n (CompressedSchedule.atom block)).expand).filter
        (fun sc => kindIsMagicReq sc.kind)).length = 0

theorem window_throughput_ok_of_no_magic
    (sched : List SysCall) (window_us max_per_window : Nat)
    (h : (sched.filter (fun sc => kindIsMagicReq sc.kind)).length = 0) :
    window_throughput_ok sched window_us max_per_window = true

private def cap_per_cycle_check_at
    (arch : ZonedArch) (L : List SysCall) (t : Nat) : Bool

private theorem capacity_per_cycle_ok_eq
    (arch : ZonedArch) (L : List SysCall) :
    capacity_per_cycle_ok arch L
      = (scheduleEventTimes L).all (cap_per_cycle_check_at arch L)

private theorem cap_per_cycle_check_at_shiftSchedule
    (arch : ZonedArch) (xs : List SysCall) (t dt : Nat) :
    cap_per_cycle_check_at arch (shiftSchedule dt xs) (t + dt)
      = cap_per_cycle_check_at arch xs t

theorem capacity_per_cycle_ok_shiftSchedule_eq
    (arch : ZonedArch) (dt : Nat) (xs : List SysCall) :
    capacity_per_cycle_ok arch (shiftSchedule dt xs)
      = capacity_per_cycle_ok arch xs

theorem capacity_per_cycle_ok_seqSchedules
    (arch : ZonedArch) (xs ys : List SysCall)
    (hxs : capacity_per_cycle_ok arch xs = true)
    (hys : capacity_per_cycle_ok arch ys = true)
    (hwithin : scheduleWithinWallclock xs = true) :
    capacity_per_cycle_ok arch (seqSchedules xs ys) = true

theorem capacity_per_cycle_ok_seqMany_replicate_block
    (arch : ZonedArch) (block : List SysCall) (n : Nat)
    (hblock : capacity_per_cycle_ok arch block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    capacity_per_cycle_ok arch
        (seqManySchedules (List.replicate n block)) = true

theorem capacity_per_cycle_ok_repeated_block_expand
    (arch : ZonedArch) (block : List SysCall) (n : Nat)
    (hblock : capacity_per_cycle_ok arch block = true)
    (hwithin : scheduleWithinWallclock block = true) :
    capacity_per_cycle_ok arch
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem resourceOfSysCalls_nil :
    resourceOfSysCalls [] = CompressedResourceSummary.zero

theorem resourceOfSysCalls_seqSchedules (xs ys : List SysCall) :
    resourceOfSysCalls (seqSchedules xs ys)
      = seqCombine (resourceOfSysCalls xs) (resourceOfSysCalls ys)

theorem resourceOfSysCalls_parSchedules (xs ys : List SysCall) :
    resourceOfSysCalls (parSchedules xs ys)
      = parCombine (resourceOfSysCalls xs) (resourceOfSysCalls ys)

theorem resourceOfSysCalls_seqMany (ls : List (List SysCall)) :
    resourceOfSysCalls (seqManySchedules ls)
      = (ls.map resourceOfSysCalls).foldr seqCombine zero

theorem resourceOfSysCalls_parMany (ls : List (List SysCall)) :
    resourceOfSysCalls (parManySchedules ls)
      = (ls.map resourceOfSysCalls).foldr parCombine zero

theorem scale_succ (n : Nat) (r : CompressedResourceSummary) :
    scale (n + 1) r = seqCombine r (scale n r)

theorem foldr_seqCombine_replicate (n : Nat) (r : CompressedResourceSummary) :
    (List.replicate n r).foldr seqCombine zero = scale n r

theorem resource_eq_expand :
    (cs : CompressedSchedule) →
      cs.resource = resourceOfSysCalls cs.expand
  | .atom xs =>

theorem resource_wallclock_eq (cs : CompressedSchedule) :
    cs.resource.wallclock_us = wallclockUs cs.expand

theorem resource_syscall_count_eq (cs : CompressedSchedule) :
    cs.resource.syscall_count = opCountS cs.expand

theorem resource_gate2q_eq (cs : CompressedSchedule) :
    cs.resource.gate2q_count = countGate2q cs.expand

theorem resource_magic_req_eq (cs : CompressedSchedule) :
    cs.resource.magic_req_count = countMagicReq cs.expand

theorem shiftSysCall_duration (dt : Nat) (sc : SysCall) :
    (shiftSysCall dt sc).end_us - (shiftSysCall dt sc).begin_us
      = sc.end_us - sc.begin_us

theorem syscall_acts_on_shiftSysCall (dt : Nat) (sc : SysCall) :
    syscall_acts_on (shiftSysCall dt sc) = syscall_acts_on sc

theorem syscall_factory_claims_shiftSysCall (dt : Nat) (sc : SysCall) :
    syscall_factory_claims (shiftSysCall dt sc) = syscall_factory_claims sc

theorem capacity_in_arch_ok_shiftSchedule
    (arch : ZonedArch) (dt : Nat) (xs : List SysCall) :
    capacity_in_arch_ok arch (shiftSchedule dt xs)
      = capacity_in_arch_ok arch xs

theorem capacity_in_arch_ok_shiftSchedule_of_ok
    (arch : ZonedArch) (dt : Nat) (xs : List SysCall)
    (h : capacity_in_arch_ok arch xs = true) :
    capacity_in_arch_ok arch (shiftSchedule dt xs) = true

theorem feedback_latency_ok_shiftSchedule
    (t_cycle_us dt : Nat) (xs : List SysCall) :
    feedback_latency_ok t_cycle_us (shiftSchedule dt xs)
      = feedback_latency_ok t_cycle_us xs

theorem feedback_latency_ok_shiftSchedule_of_ok
    (t_cycle_us dt : Nat) (xs : List SysCall)
    (h : feedback_latency_ok t_cycle_us xs = true) :
    feedback_latency_ok t_cycle_us (shiftSchedule dt xs) = true

theorem decoder_react_ok_shiftSchedule
    (t_react_us dt : Nat) (xs : List SysCall) :
    decoder_react_ok t_react_us (shiftSchedule dt xs)
      = decoder_react_ok t_react_us xs

theorem decoder_react_ok_shiftSchedule_of_ok
    (t_react_us dt : Nat) (xs : List SysCall)
    (h : decoder_react_ok t_react_us xs = true) :
    decoder_react_ok t_react_us (shiftSchedule dt xs) = true

theorem freshnessStep_shiftSysCall
    (model : AncillaModel) (state : List (Nat × SiteLifecycle))
    (dt : Nat) (sc : SysCall) :
    freshnessStep model state (shiftSysCall dt sc)
      = freshnessStep model state sc

theorem runFreshness_shiftSchedule
    (model : AncillaModel) (state : List (Nat × SiteLifecycle))
    (dt : Nat) (xs : List SysCall) :
    runFreshness model state (shiftSchedule dt xs)
      = runFreshness model state xs

theorem ancilla_freshness_ok_shiftSchedule
    (model : AncillaModel) (dt : Nat) (xs : List SysCall) :
    ancilla_freshness_ok model (shiftSchedule dt xs)
      = ancilla_freshness_ok model xs

theorem ancilla_freshness_ok_shiftSchedule_of_ok
    (model : AncillaModel) (dt : Nat) (xs : List SysCall)
    (h : ancilla_freshness_ok model xs = true) :
    ancilla_freshness_ok model (shiftSchedule dt xs) = true

theorem kindIsMagicReq_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsMagicReq (shiftSysCall dt sc).kind = kindIsMagicReq sc.kind

theorem kindIsGate2q_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsGate2q (shiftSysCall dt sc).kind = kindIsGate2q sc.kind

theorem kindIsMeasure_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsMeasure (shiftSysCall dt sc).kind = kindIsMeasure sc.kind

theorem kindIsDecode_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsDecode (shiftSysCall dt sc).kind = kindIsDecode sc.kind

theorem kindIsFeedback_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsFeedback (shiftSysCall dt sc).kind = kindIsFeedback sc.kind

theorem kindIsFreshAnc_shiftSysCall (dt : Nat) (sc : SysCall) :
    kindIsFreshAnc (shiftSysCall dt sc).kind = kindIsFreshAnc sc.kind

theorem magic_count_shiftSchedule (dt : Nat) (xs : List SysCall) :
    ((shiftSchedule dt xs).filter (fun sc => kindIsMagicReq sc.kind)).length
      = (xs.filter (fun sc => kindIsMagicReq sc.kind)).length

theorem no_magic_shiftSchedule
    (dt : Nat) (xs : List SysCall)
    (h : (xs.filter fun sc => kindIsMagicReq sc.kind).length = 0) :
    ((shiftSchedule dt xs).filter fun sc => kindIsMagicReq sc.kind).length = 0

def scheduleWithinWallclock (xs : List SysCall) : Bool

theorem scheduleWithinWallclock_end_le
    (xs : List SysCall) (sc : SysCall)
    (hmem : sc ∈ xs) (h : scheduleWithinWallclock xs = true) :
    sc.end_us ≤ scheduleWallclockUs xs

theorem scheduleWithinWallclock_begin_lt_end
    (xs : List SysCall) (sc : SysCall)
    (hmem : sc ∈ xs) (h : scheduleWithinWallclock xs = true) :
    sc.begin_us < sc.end_us

theorem shifted_begin_ge_offset
    (dt : Nat) (ys : List SysCall) (sc : SysCall)
    (hmem : sc ∈ shiftSchedule dt ys) :
    dt ≤ sc.begin_us

theorem intervals_overlap_shift_same
    (a_lo a_hi b_lo b_hi dt : Nat) :
    intervals_overlap (a_lo + dt) (a_hi + dt) (b_lo + dt) (b_hi + dt)
      = intervals_overlap a_lo a_hi b_lo b_hi

theorem intervals_overlap_disjoint_when_le
    (a_lo a_hi b_lo b_hi : Nat) (h : a_hi ≤ b_lo) :
    intervals_overlap a_lo a_hi b_lo b_hi = false

theorem cross_pair_no_overlap
    (xs ys : List SysCall)
    (sc₁ sc₂ : SysCall)
    (h₁ : sc₁ ∈ xs)
    (h₂ : sc₂ ∈ shiftSchedule (scheduleWallclockUs xs) ys)
    (hwithin : scheduleWithinWallclock xs = true) :
    intervals_overlap sc₁.begin_us sc₁.end_us sc₂.begin_us sc₂.end_us = false

theorem rep_atom_expand_eq (body : List SysCall) (n : Nat) :
    (CompressedSchedule.rep n (CompressedSchedule.atom body)).expand
      = seqManySchedules (List.replicate n body)

theorem symbolic_rep_ok_implies_body_exclusivity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    exclusivity_ok block = true

theorem symbolic_rep_ok_implies_body_factory_exclusivity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    factory_exclusivity_ok block = true

theorem symbolic_rep_ok_implies_body_operation_capacity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    operation_capacity_ok models.opCap block = true

theorem symbolic_rep_ok_implies_body_slot_capacity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    slot_capacity_ok models.slotCap block = true

theorem symbolic_rep_implies_expanded_block_exclusivity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_factory_exclusivity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    factory_exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_operation_capacity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    operation_capacity_ok models.opCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_slot_capacity_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    slot_capacity_ok models.slotCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_combined_strict_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true
    ∧ factory_exclusivity_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true
    ∧ operation_capacity_ok models.opCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true
    ∧ slot_capacity_ok models.slotCap
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_ok_implies_body_capacity_in_arch_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    capacity_in_arch_ok models.arch block = true

theorem symbolic_rep_ok_implies_body_capacity_per_cycle_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    capacity_per_cycle_ok models.arch block = true

theorem symbolic_rep_ok_implies_body_feedback_latency_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    feedback_latency_ok models.arch.t_cycle_us block = true

theorem symbolic_rep_ok_implies_body_decoder_react_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    decoder_react_ok models.t_react_us block = true

theorem symbolic_rep_ok_implies_body_no_magic
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    (block.filter (fun sc => kindIsMagicReq sc.kind)).length = 0

theorem symbolic_rep_implies_expanded_block_capacity_in_arch_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    capacity_in_arch_ok models.arch
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_capacity_per_cycle_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    capacity_per_cycle_ok models.arch
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_feedback_latency_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    feedback_latency_ok models.arch.t_cycle_us
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_decoder_react_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    decoder_react_ok models.t_react_us
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand = true

theorem symbolic_rep_implies_expanded_block_window_throughput_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true) :
    window_throughput_ok
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand
        models.window_us models.max_per_window = true

theorem symbolic_rep_implies_expanded_block_strict_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hSym : symbolic_rep_strict_ok models block n = true)
    (hwithin : scheduleWithinWallclock block = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand
        models.t_react_us
        models.window_us

def symbolic_rep_strict_ok_within
    (models : SystemModels) (block : List SysCall) (n : Nat) : Bool

theorem symbolic_rep_strict_ok_within_implies_symbolic_rep_strict_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hCert : symbolic_rep_strict_ok_within models block n = true) :
    symbolic_rep_strict_ok models block n = true

theorem symbolic_rep_strict_ok_within_implies_scheduleWithinWallclock
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hCert : symbolic_rep_strict_ok_within models block n = true) :
    scheduleWithinWallclock block = true

theorem symbolic_rep_strict_ok_within_implies_expanded_block_strict_ok
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hCert : symbolic_rep_strict_ok_within models block n = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

theorem hardware_generic_repeated_block_strict_soundness
    (models : SystemModels) (block : List SysCall) (n : Nat)
    (hCert : symbolic_rep_strict_ok_within models block n = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch
        models.opCap
        models.slotCap
        models.ancillaModel
        (CompressedSchedule.rep n (CompressedSchedule.atom block)).expand
        models.t_react_us
        models.window_us
        models.max_per_window = true

inductive CompressedSchedule

def CompressedSchedule.expand : CompressedSchedule → List SysCall
  | .atom xs    => xs
  | .seq blocks => seqManySchedules (blocks.map CompressedSchedule.expand)
  | .par blocks => parManySchedules (blocks.map CompressedSchedule.expand)
  | .rep n body => seqManySchedules (List.replicate n body.expand)

structure CompressedResourceSummary

def zero : CompressedResourceSummary

def seqCombine (a b : CompressedResourceSummary) : CompressedResourceSummary

def parCombine (a b : CompressedResourceSummary) : CompressedResourceSummary

def scale (n : Nat) (r : CompressedResourceSummary) : CompressedResourceSummary

def resourceOfSysCalls (xs : List SysCall) : CompressedResourceSummary

def CompressedSchedule.resource : CompressedSchedule → CompressedResourceSummary
  | .atom xs    => resourceOfSysCalls xs
  | .seq blocks =>
      (blocks.map CompressedSchedule.resource).foldr
        CompressedResourceSummary.seqCombine CompressedResourceSummary.zero
  | .par blocks =>
      (blocks.map CompressedSchedule.resource).foldr
        CompressedResourceSummary.parCombine CompressedResourceSummary.zero
  | .rep n body => CompressedResourceSummary.scale n body.resource

structure CompressedScheduleArtifact

structure VerifiedCompressedSchedule

theorem verified_compressed_schedule_of_expanded_strict_ok
    (artifact : CompressedScheduleArtifact) (models : SystemModels)
    (h : all_invariants_strict_with_slot_capacity_and_freshness_ok
            models.arch models.opCap models.slotCap models.ancillaModel
            artifact.schedule.expand
            models.t_react_us models.window_us models.max_per_window = true) :
    ∃ cert : VerifiedCompressedSchedule,
      cert.artifact = artifact
      ∧ cert.models = models
      ∧ cert.resources = artifact.schedule.resource

structure ExternalCompressedScheduleCertificate

def external_compressed_schedule_strict_ok
    (models : SystemModels) (c : ExternalCompressedScheduleCertificate) : Bool

def adder_n1_compressed_atom : CompressedSchedule

theorem adder_n1_compressed_atom_expand :
    adder_n1_compressed_atom.expand = adder_n1_syscalls

theorem adder_n1_compressed_atom_resource_wallclock :
    adder_n1_compressed_atom.resource.wallclock_us = 48

theorem adder_n1_compressed_atom_resource_syscall_count :
    adder_n1_compressed_atom.resource.syscall_count = 48

theorem adder_n1_compressed_atom_resource_gate2q :
    adder_n1_compressed_atom.resource.gate2q_count = 18

def python_generated_compressed_atom_example :
    ExternalCompressedScheduleCertificate

theorem adder_n1_compressed_atom_checked :
    external_compressed_schedule_strict_ok
        adder_n1_system_models python_generated_compressed_atom_example = true

def adder_n1_repeated_3 : CompressedSchedule

theorem adder_n1_repeated_3_resource_wallclock :
    adder_n1_repeated_3.resource.wallclock_us = 144

theorem adder_n1_repeated_3_resource_gate2q :
    adder_n1_repeated_3.resource.gate2q_count = 54

theorem adder_n1_repeated_3_resource_syscall_count :
    adder_n1_repeated_3.resource.syscall_count = 144

theorem adder_n1_repeated_3_expand_wallclock :
    scheduleWallclockUs adder_n1_repeated_3.expand = 144

def python_generated_compressed_rep_example :
    ExternalCompressedScheduleCertificate

theorem adder_n1_repeated_3_checked :
    external_compressed_schedule_strict_ok
        adder_n1_system_models python_generated_compressed_rep_example = true

def python_bad_compressed_wallclock_example :
    ExternalCompressedScheduleCertificate

theorem python_bad_compressed_wallclock_rejected :
    external_compressed_schedule_strict_ok
        adder_n1_system_models python_bad_compressed_wallclock_example = false

def python_bad_compressed_gate2q_example :
    ExternalCompressedScheduleCertificate

theorem python_bad_compressed_gate2q_rejected :
    external_compressed_schedule_strict_ok
        adder_n1_system_models python_bad_compressed_gate2q_example = false

def bad_parallel_compressed_adder_schedule : CompressedSchedule

def bad_parallel_compressed_adder_example :
    ExternalCompressedScheduleCertificate

theorem bad_parallel_compressed_adder_rejected :
    external_compressed_schedule_strict_ok
        adder_n1_system_models bad_parallel_compressed_adder_example = false

def repeat_boundary_clean (body : List SysCall) : Bool

def repeat_safe_block_ok
    (models : SystemModels) (body : List SysCall) : Bool

def symbolic_rep_strict_ok
    (models : SystemModels) (body : List SysCall) (_reps : Nat) : Bool

structure RepeatSafeBlock

structure RepeatedScheduleCertificate

def RepeatedScheduleCertificate.toCompressedSchedule
    (c : RepeatedScheduleCertificate) : CompressedSchedule

theorem repeated_schedule_resource_wallclock
    (body : List SysCall) (n : Nat) :
    (CompressedSchedule.rep n (CompressedSchedule.atom body)).resource.wallclock_us
      = n * scheduleWallclockUs body

theorem repeated_schedule_resource_syscall_count
    (body : List SysCall) (n : Nat) :
    (CompressedSchedule.rep n (CompressedSchedule.atom body)).resource.syscall_count
      = n * FormalRV.Resource.SysCallCount.opCountS body

theorem repeated_schedule_resource_gate2q
    (body : List SysCall) (n : Nat) :
    (CompressedSchedule.rep n (CompressedSchedule.atom body)).resource.gate2q_count
      = n * FormalRV.Resource.SysCallCount.countGate2q body

theorem symbolic_rep_ok_implies_body_ok
    (models : SystemModels) (body : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok models body n = true) :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        models.arch models.opCap models.slotCap models.ancillaModel
        body
        models.t_react_us models.window_us models.max_per_window = true

theorem symbolic_rep_ok_implies_body_boundary_clean
    (models : SystemModels) (body : List SysCall) (n : Nat)
    (h : symbolic_rep_strict_ok models body n = true) :
    repeat_boundary_clean body = true

structure ExternalRepeatedScheduleCertificate

def external_repeated_schedule_symbolic_ok
    (models : SystemModels) (c : ExternalRepeatedScheduleCertificate) : Bool

theorem adder_n1_repeat_block_ok :
    repeat_safe_block_ok adder_n1_system_models adder_n1_syscalls = true

theorem adder_n1_repeated_3_symbolic_ok :
    symbolic_rep_strict_ok adder_n1_system_models adder_n1_syscalls 3 = true

theorem adder_n1_repeated_3_expanded_strict_ok :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        adder_n1_system_models.arch
        adder_n1_system_models.opCap
        adder_n1_system_models.slotCap
        adder_n1_system_models.ancillaModel
        (CompressedSchedule.rep 3 (CompressedSchedule.atom adder_n1_syscalls)).expand
        adder_n1_system_models.t_react_us
        adder_n1_system_models.window_us
        adder_n1_system_models.max_per_window = true

def python_repeated_adder_symbolic_example :
    ExternalRepeatedScheduleCertificate

theorem python_repeated_adder_symbolic_example_checked :
    external_repeated_schedule_symbolic_ok
        adder_n1_system_models python_repeated_adder_symbolic_example = true

def python_repeated_adder_bad_wallclock_example :
    ExternalRepeatedScheduleCertificate

theorem python_repeated_adder_bad_wallclock_rejected :
    external_repeated_schedule_symbolic_ok
        adder_n1_system_models python_repeated_adder_bad_wallclock_example = false

def python_repeated_bad_body : List SysCall

def python_repeated_bad_body_example :
    ExternalRepeatedScheduleCertificate

theorem python_repeated_bad_body_rejected :
    external_repeated_schedule_symbolic_ok
        adder_n1_system_models python_repeated_bad_body_example = false

inductive ArtifactLayer

structure ArtifactMetadata

structure GateArtifact

structure SurgeryArtifact

structure SysCallScheduleArtifact

structure SystemModels

structure VerifiedSysCallSchedule

theorem verified_syscall_schedule_of_strict_ok
    (artifact : SysCallScheduleArtifact) (models : SystemModels)
    (h : all_invariants_strict_with_slot_capacity_and_freshness_ok
            models.arch models.opCap models.slotCap models.ancillaModel
            artifact.syscalls
            models.t_react_us models.window_us models.max_per_window = true) :
    ∃ cert : VerifiedSysCallSchedule,
      cert.artifact = artifact
      ∧ cert.models = models
      ∧ cert.wallclock_us = scheduleWallclockUs artifact.syscalls

structure LayerCompiler (α β : Type)

def simpleSurgeryToSysCallCompiler :
    LayerCompiler SchedulableSurgeryGadget SysCallScheduleArtifact

def topologySurgeryToSysCallCompiler :
    LayerCompiler TopologySchedulableSurgeryGadget SysCallScheduleArtifact

def adder_n1_syscall_artifact : SysCallScheduleArtifact

def adder_n1_system_models : SystemModels

theorem adder_n1_artifact_verified :
    ∃ cert : VerifiedSysCallSchedule,
      cert.artifact = adder_n1_syscall_artifact
      ∧ cert.models = adder_n1_system_models
      ∧ cert.wallclock_us
          = scheduleWallclockUs adder_n1_syscall_artifact.syscalls

structure ExternalScheduleCertificate

def external_wallclock_matches (c : ExternalScheduleCertificate) : Bool

def external_syscall_count_matches (c : ExternalScheduleCertificate) : Bool

def external_gate2q_count_matches (c : ExternalScheduleCertificate) : Bool

def external_schedule_strict_ok
    (models : SystemModels) (c : ExternalScheduleCertificate) : Bool

def python_generated_adder_example : ExternalScheduleCertificate

theorem python_generated_adder_example_checked :
    external_schedule_strict_ok
        adder_n1_system_models python_generated_adder_example = true

def python_bad_wallclock_example : ExternalScheduleCertificate

theorem python_bad_wallclock_example_rejected :
    external_schedule_strict_ok
        adder_n1_system_models python_bad_wallclock_example = false

def python_bad_gate2q_example : ExternalScheduleCertificate

theorem python_bad_gate2q_example_rejected :
    external_schedule_strict_ok
        adder_n1_system_models python_bad_gate2q_example = false

def magicFloorN   (K fq prod Q : Nat) : Nat

def decoderFloorN (K tReact nDec : Nat) : Nat

def parFloorN     (K opTime maxPar : Nat) : Nat

def depthFloorN   (depth tMeas tReact : Nat) : Nat

def physQubitsN   (L d : Nat) : Nat

theorem decoderFloor_mono_tReact (K nDec : Nat) {t t' : Nat} (h : t ≤ t') :
    decoderFloorN K t nDec ≤ decoderFloorN K t' nDec

theorem depthFloor_mono_tReact (depth tMeas : Nat) {t t' : Nat} (h : t ≤ t') :
    depthFloorN depth tMeas t ≤ depthFloorN depth tMeas t'

theorem decoderFloor_anti_nDec (K t : Nat) {n n' : Nat} (hpos : 0 < n) (h : n ≤ n') :
    decoderFloorN K t n' ≤ decoderFloorN K t n

theorem magicFloor_anti_Q (K fq prod : Nat) {Q Q' : Nat} (hpos : 0 < Q) (h : Q ≤ Q') :
    magicFloorN K fq prod Q' ≤ magicFloorN K fq prod Q

theorem magicFloor_mono_prod (K fq Q : Nat) {p p' : Nat} (h : p ≤ p') :
    magicFloorN K fq p Q ≤ magicFloorN K fq p' Q

theorem magicFloor_mono_fq (K prod Q : Nat) {f f' : Nat} (h : f ≤ f') :
    magicFloorN K f prod Q ≤ magicFloorN K f' prod Q

theorem parFloor_mono_opTime (K maxPar : Nat) {o o' : Nat} (h : o ≤ o') :
    parFloorN K o maxPar ≤ parFloorN K o' maxPar

theorem depthFloor_mono_tMeas (depth tReact : Nat) {m m' : Nat} (h : m ≤ m') :
    depthFloorN depth m tReact ≤ depthFloorN depth m' tReact

theorem parFloor_anti_maxPar (K o : Nat) {p p' : Nat} (hpos : 0 < p) (h : p ≤ p') :
    parFloorN K o p' ≤ parFloorN K o p

theorem physQubits_mono_d (L : Nat) {d d' : Nat} (h : d ≤ d') :
    physQubitsN L d ≤ physQubitsN L d'

structure HW

def HW.timeLB (h : HW) (K depth : Nat) : Nat

def ge2021 : HW

def gidney2025 : HW

def ge2021_K : Nat

def gidney2025_K : Nat

theorem both_papers :
    magicFloorN ge2021_K ge2021.fq ge2021.prod 3600000000 = 22425149
    ∧ magicFloorN gidney2025_K gidney2025.fq gidney2025.prod 3600000000 = 55575000
    ∧ physQubitsN 6189 ge2021.d = 9704352
    ∧ physQubitsN 6189 gidney2025.d = 8367528

theorem magicFloor_matches_rsa2048 :
    magicFloorN ge2021_K ge2021.fq ge2021.prod 3600000000
      = ScheduleLowerBound.rsa2048_floor_qubit_hours

def naiveOp (k : Nat) : DeviceOp

def naiveFrom (s : Nat) : Nat → DSchedule
  | 0     => []
  | M + 1 => naiveOp s :: naiveFrom (s + 1) M

def naiveSchedule (M : Nat) : DSchedule

theorem naiveFrom_begin_ge : ∀ (s M : Nat) (o : DeviceOp), o ∈ naiveFrom s M → s ≤ o.begin_t
  | _, 0,     o, h => by simp [naiveFrom] at h
  | s, M + 1, o, h =>

theorem naiveFrom_footprint : ∀ (s M : Nat) (o : DeviceOp), o ∈ naiveFrom s M → o.footprint = [0]
  | _, 0,     o, h => by simp [naiveFrom] at h
  | s, M + 1, o, h =>

theorem naiveFrom_dur : ∀ (s M : Nat) (o : DeviceOp), o ∈ naiveFrom s M → o.dur_t = 1
  | _, 0,     o, h => by simp [naiveFrom] at h
  | s, M + 1, o, h =>

theorem naiveFrom_deps : ∀ (s M : Nat) (o : DeviceOp), o ∈ naiveFrom s M → o.deps = []
  | _, 0,     o, h => by simp [naiveFrom] at h
  | s, M + 1, o, h =>

theorem head_no_conflict (s M : Nat) :
    (naiveFrom (s + 1) M).all (fun o => ! (naiveOp s).conflictsWith o) = true

theorem conflictFree_naiveFrom : ∀ (s M : Nat), conflictFree (naiveFrom s M) = true
  | _, 0     => rfl
  | s, M + 1 =>

theorem naiveFrom_filter_empty (P : DeviceOp → Bool) (t : Nat)
    (hP : ∀ o, P o = true → o.activeAt t = true) :
    ∀ (s M : Nat), t < s → (naiveFrom s M).filter P = []

theorem naiveFrom_filter_le_one (P : DeviceOp → Bool) (t : Nat)
    (hP : ∀ o, P o = true → o.activeAt t = true) :
    ∀ (s M : Nat), ((naiveFrom s M).filter P).length ≤ 1

theorem naiveFrom_atMostOneActive (t s M : Nat) :
    ((naiveFrom s M).filter (fun o => o.activeAt t)).length ≤ 1

theorem decoderActive_naive_le_one (t s M : Nat) :
    ((naiveFrom s M).filter (fun o => o.isDecode && o.activeAt t)).length ≤ 1

theorem mapsum_footprint_le_one : ∀ (L : List DeviceOp), L.length ≤ 1 →
    (∀ o ∈ L, o.footprint.length = 1) →
    (L.map (fun o => o.footprint.length)).sum ≤ 1
  | [],          _,  _  => by simp
  | [o],         _,  h2 =>

theorem activeFootprintSize_naive_le_one (s M t : Nat) :
    activeFootprintSize (naiveFrom s M) t ≤ 1

def adequate (dev : Device) : Prop

theorem capacityRespected_naive (dev : Device) (M : Nat) (h : 1 ≤ dev.totalResources) :
    capacityRespected dev (naiveSchedule M) = true

theorem decoderQueueRespected_naive (dev : Device) (M : Nat) (h : 1 ≤ dev.nDecoders) :
    decoderQueueRespected dev (naiveSchedule M) = true

theorem reactionRespected_naive (dev : Device) (M : Nat) (h : 1 ≤ dev.reactionTime) :
    reactionRespected dev (naiveSchedule M) = true

theorem depsRespected_naive (M : Nat) : depsRespected (naiveSchedule M) = true

theorem naiveSchedule_valid (dev : Device) (M : Nat) (hdev : adequate dev) :
    scheduleValid dev (naiveSchedule M) = true

theorem naiveFrom_total_order (s M : Nat) (o1 o2 : DeviceOp)
    (h1 : o1 ∈ naiveFrom s M) (hlt : o1.begin_t < o2.begin_t) :
    o1.end_t ≤ o2.begin_t

def rsa2048_opCount : Nat

theorem rsa2048_opCount_value : rsa2048_opCount = 7868473344

theorem rsa2048_naive_schedule_valid (dev : Device) (hdev : adequate dev) :
    scheduleValid dev (naiveSchedule rsa2048_opCount) = true

def naiveEstimate (hw : Hardware) (w : Workload) (c : QECCode) (factory : Nat) :
    ResourceEstimate

theorem naive_time (hw : Hardware) (w : Workload) (c : QECCode) (factory : Nat) :
    (naiveEstimate hw w c factory).time_us_tenths
      = w.n_toff * c.d * hw.cycle_time_us_tenths

theorem naive_qubits (hw : Hardware) (w : Workload) (c : QECCode) (factory : Nat) :
    (naiveEstimate hw w c factory).qubits
      = w.n_logical * (2 * physPerLogical c) + factory

def naivePeak (footprint : Nat) : Nat → Nat
  | 0 => 0
  | k + 1 => max footprint (naivePeak footprint k)

theorem naivePeak_le_footprint (footprint k : Nat) :
    naivePeak footprint k ≤ footprint

theorem naive_peak_within_estimate
    (hw : Hardware) (w : Workload) (c : QECCode) (factory k : Nat) :
    naivePeak ((naiveEstimate hw w c factory).qubits) k
      ≤ (naiveEstimate hw w c factory).qubits

def naiveMakespan (hw : Hardware) (d k : Nat) : Nat

theorem naiveMakespan_at_full
    (hw : Hardware) (w : Workload) (c : QECCode) (factory : Nat) :
    naiveMakespan hw c.d w.n_toff = (naiveEstimate hw w c factory).time_us_tenths

example : checkAll baseInvariants demoCtx = true

def ge2021_hw : Hardware

def ge2021_work : Workload

def ge2021_code : QECCode

def ge2021_naive : ResourceEstimate

def ge2021_reported_qubits : Nat

def ge2021_reported_time_us_tenths : Nat

example : ge2021_naive.qubits = 19_443_200

example : ge2021_naive.qubits ≤ ge2021_reported_qubits

example : ge2021_reported_qubits - ge2021_naive.qubits ≤ 600_000

example : ge2021_naive.time_us_tenths = 729_000_000_000

example : ge2021_reported_time_us_tenths ≤ ge2021_naive.time_us_tenths

example : 2 * ge2021_reported_time_us_tenths ≤ ge2021_naive.time_us_tenths

example : ge2021_naive.time_us_tenths ≤ 3 * ge2021_reported_time_us_tenths

def parallelTwoFactories : DSchedule

def parDev : Device

theorem parallelTwoFactories_valid : scheduleValid parDev parallelTwoFactories = true

theorem parallelTwoFactories_parallel :
    opsTimeOverlap parallelTwoFactories[0]! parallelTwoFactories[1]! = true
    ∧ conflictFree parallelTwoFactories = true

theorem parallel_1093_within_8h :
    magicSupplyTimeUs 2622824448 1093 ccz_spec_qianxu ≤ 8 * 3600000000
    ∧ 7 * 3600000000 ≤ magicSupplyTimeUs 2622824448 1093 ccz_spec_qianxu

theorem parallel_speedup :
    1000 * magicSupplyTimeUs 2622824448 1093 ccz_spec_qianxu
      ≤ magicSupplyTimeUs 2622824448 1 ccz_spec_qianxu

theorem parallel_supply_above_floor :
    -- the 1093-factory magic supply, as qubit·µs over the data+factory device, is ≥ the floor
    ScheduleLowerBound.rsa2048_floor_qubit_us
      ≤ (9633792 + 1093 * 2565) * magicSupplyTimeUs 2622824448 1093 ccz_spec_qianxu

def babbush_ecc256_floor_qubit_hours : Nat

theorem babbush_ecc256_floor_value : babbush_ecc256_floor_qubit_hours = 769500

def naiveSerialHours (K : Nat) : Nat

theorem babbush_ecc256_naive_hours : naiveSerialHours 90000000 = 301

def schedulePeak (sched : DSchedule) : Nat

private theorem foldl_max_le : ∀ (L : List Nat) (acc c : Nat),
    acc ≤ c → (∀ x ∈ L, x ≤ c) → L.foldl max acc ≤ c
  | [],      acc, c, ha, _ => ha
  | x :: xs, acc, c, ha, h =>

theorem naive_peak_le_one (M : Nat) : schedulePeak (naiveSchedule M) ≤ 1

theorem naive_peak_le_total (dev : Device) (M : Nat) (h : 1 ≤ dev.totalResources) :
    schedulePeak (naiveSchedule M) ≤ dev.totalResources

theorem resource_bracket (sched : DSchedule) (T Q fq prod : Nat)
    (hfit : ∀ o ∈ sched, o.end_t ≤ T)
    (hcap : ∀ t ∈ Finset.range T, activeFootprintSize sched t ≤ Q)
    (hf : ∀ o ∈ sched, fq ≤ o.footprint.length)
    (hd : ∀ o ∈ sched, prod ≤ o.dur_t) :
    sched.length * (fq * prod) ≤ workload sched ∧ workload sched ≤ Q * T

theorem causal_two (a b : DeviceOp) (h : a.end_t ≤ b.begin_t) :
    a.begin_t + a.dur_t + b.dur_t ≤ b.end_t

theorem causal_chain4 (distill inject meas decode : DeviceOp)
    (h1 : distill.end_t ≤ inject.begin_t) (h2 : inject.end_t ≤ meas.begin_t)
    (h3 : meas.end_t ≤ decode.begin_t) :
    distill.begin_t + distill.dur_t + inject.dur_t + meas.dur_t + decode.dur_t ≤ decode.end_t

def opWork (o : DeviceOp) : Nat

def workload (sched : DSchedule) : Nat

def spacetimeUsed (sched : DSchedule) (T : Nat) : Nat

theorem activeFootprintSize_eq_indicator (sched : DSchedule) (t : Nat) :
    activeFootprintSize sched t
      = (sched.map (fun o => if o.activeAt t then o.footprint.length else 0)).sum

theorem sum_range_listmap (T : Nat) {α : Type _} (L : List α) (g : Nat → α → Nat) :
    ∑ t ∈ Finset.range T, (L.map (fun a => g t a)).sum
      = (L.map (fun a => ∑ t ∈ Finset.range T, g t a)).sum

theorem card_active_slots (o : DeviceOp) (T : Nat) (h : o.end_t ≤ T) :
    ((Finset.range T).filter (fun t => o.activeAt t = true)).card = o.dur_t

theorem op_slice (o : DeviceOp) (T : Nat) (h : o.end_t ≤ T) :
    (∑ t ∈ Finset.range T, if o.activeAt t then o.footprint.length else 0) = opWork o

theorem spacetimeUsed_eq_workload (sched : DSchedule) (T : Nat)
    (hfit : ∀ o ∈ sched, o.end_t ≤ T) :
    spacetimeUsed sched T = workload sched

theorem spacetimeUsed_le (sched : DSchedule) (T Q : Nat)
    (hcap : ∀ t ∈ Finset.range T, activeFootprintSize sched t ≤ Q) :
    spacetimeUsed sched T ≤ Q * T

theorem workload_le (sched : DSchedule) (T Q : Nat)
    (hfit : ∀ o ∈ sched, o.end_t ≤ T)
    (hcap : ∀ t ∈ Finset.range T, activeFootprintSize sched t ≤ Q) :
    workload sched ≤ Q * T

theorem workload_ge_of_uniform (sched : DSchedule) (fq prod : Nat)
    (hf : ∀ o ∈ sched, fq ≤ o.footprint.length) (hd : ∀ o ∈ sched, prod ≤ o.dur_t) :
    sched.length * (fq * prod) ≤ workload sched

theorem magic_spacetime_floor (sched : DSchedule) (T Q fq prod : Nat)
    (hfit : ∀ o ∈ sched, o.end_t ≤ T)
    (hcap : ∀ t ∈ Finset.range T, activeFootprintSize sched t ≤ Q)
    (hf : ∀ o ∈ sched, fq ≤ o.footprint.length) (hd : ∀ o ∈ sched, prod ≤ o.dur_t) :
    sched.length * (fq * prod) ≤ Q * T

def rsa2048_toffoli_budget : Nat

def rsa2048_floor_qubit_us : Nat

def rsa2048_floor_qubit_hours : Nat

theorem rsa2048_floor_value : rsa2048_floor_qubit_hours = 22425149

theorem rsa2048_floor_gaps :
    7 * rsa2048_floor_qubit_hours ≤ 20000000 * 8
    ∧ 20000000 * 8 ≤ 8 * rsa2048_floor_qubit_hours
    ∧ 3773 * rsa2048_floor_qubit_hours ≤ 9636357 * 8782
    ∧ 9636357 * 8782 ≤ 3774 * rsa2048_floor_qubit_hours

structure FTSchedule

def FTSchedule.distance_adequate (f : FTSchedule) : Bool

def FTSchedule.ft_ok (f : FTSchedule) : Bool

theorem ftSchedule_guarantee (f : FTSchedule) (h : f.ft_ok = true) :
    all_invariants_ok f.arch f.sched f.window_us f.max_per_window f.distance_fn = true
    ∧ decoder_react_ok f.t_react_us f.sched = true
    ∧ 3 * f.tau_s ≥ 2 * f.code_distance

abbrev countKind : (SysCallKind → Bool) → List SysCall → Nat

abbrev magicStateCount : List SysCall → Nat

abbrev ancillaCount : List SysCall → Nat

abbrev decodeRounds : List SysCall → Nat

abbrev routingMoves : List SysCall → Nat

def wallclock_us (s : List SysCall) : Nat

structure SystemBudget

def FTSchedule.budget (f : FTSchedule) : SystemBudget

def demoArch : ZonedArch

def demoDist : Nat → Nat

def demoSched : List SysCall

def demoFT : FTSchedule

example : demoFT.ft_ok = true

example : demoFT.budget =
    { magic_states

theorem demoFT_guarantee :
    all_invariants_ok demoFT.arch demoFT.sched demoFT.window_us demoFT.max_per_window
        demoFT.distance_fn = true
    ∧ decoder_react_ok demoFT.t_react_us demoFT.sched = true
    ∧ 3 * demoFT.tau_s ≥ 2 * demoFT.code_distance

def demoSched_slowTransit : List SysCall

def demoFT_slowTransit : FTSchedule

example : demoFT_slowTransit.ft_ok = false

def demoFT_slowDecoder : FTSchedule

example : demoFT_slowDecoder.ft_ok = false

def demoFT_lowTauS : FTSchedule

example : demoFT_lowTauS.ft_ok = false

example : demoFT_lowTauS.distance_adequate = false

theorem intervals_overlap_touching_disjoint :
    intervals_overlap 0 1 1 2 = false

theorem intervals_overlap_strictly_disjoint :
    intervals_overlap 0 2 2 4 = false

theorem intervals_overlap_proper_overlap :
    intervals_overlap 0 2 1 3 = true

theorem intervals_overlap_contained :
    intervals_overlap 0 10 3 7 = true

theorem intervals_overlap_symmetric :
    intervals_overlap 1 3 0 2 = true

theorem connEdges_single_row_three_entries :
    connEdges [[true, false, true, false, true]] = [(0, 0), (0, 2), (0, 4)]

theorem connEdges_three_rows_one_entry :
    connEdges [[false, true], [false, false], [true, false]]
      = [(0, 1), (2, 0)]

theorem connEdges_all_false_empty :
    connEdges [[false, false], [false, false]] = []

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

def topology_demo_target_mutated_gadget : SurgeryGadget

theorem topology_demo_target_mutated_differs :
    topology_demo_target_mutated_gadget.target_pauli
      ≠ topology_demo_gadget.target_pauli

def topology_demo_target_mutated : TopologySchedulableSurgeryGadget

theorem topology_compiler_ignores_target_pauli :
    compileTopologySurgeryToSysCalls topology_demo_target_mutated
      = compileTopologySurgeryToSysCalls topology_demo

def decoder_dependency_violator : List SysCall

theorem decoder_dependency_violator_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch decoder_dependency_violator
        10 1000 1000 = true

def routing_lane_violator : List SysCall

theorem routing_lane_violator_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch routing_lane_violator
        10 1000 1000 = true

def freshness_use_before_reset : List SysCall

theorem freshness_use_before_reset_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch freshness_use_before_reset
        10 1000 1000 = true

def freshness_reuse_without_reset : List SysCall

theorem freshness_reuse_without_reset_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch freshness_reuse_without_reset
        10 1000 1000 = true

def site_id_conflation : List SysCall

theorem site_id_conflation_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch site_id_conflation
        10 1000 1000 = true

def magic_no_startup_prefix : List SysCall

theorem magic_no_startup_prefix_accepted :
    all_invariants_with_factory_ports_ok
        surgery_arch magic_no_startup_prefix
        10 1000 1 = true

def positive_ancilla_alias : List SysCall

theorem positive_ancilla_alias_rejected :
    all_invariants_with_factory_ports_ok
        surgery_arch positive_ancilla_alias
        10 1000 1000 = false

def positive_factory_port_alias : List SysCall

theorem positive_factory_port_alias_rejected :
    all_invariants_with_factory_ports_ok
        surgery_arch positive_factory_port_alias
        10 1000 1000 = false

def positive_off_arch_claim : List SysCall

theorem positive_off_arch_claim_rejected :
    all_invariants_with_factory_ports_ok
        surgery_arch positive_off_arch_claim
        10 1000 1000 = false

def positive_decoder_too_slow : List SysCall

theorem positive_decoder_too_slow_rejected :
    all_invariants_with_factory_ports_ok
        surgery_arch positive_decoder_too_slow
        10 1000 1000 = false

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 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 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 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

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

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

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

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

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

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 exclusivity_with_factory_ports_ok (sched : List SysCall) : Bool

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

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 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)

inductive QECEvent

abbrev QECProgram

def ofSchedule (s : List SurgeryGadget) : QECProgram

def QECEvent.cczInjection (factory : Nat) (mA mB mC : SurgeryGadget) : QECEvent

def QECEvent.wf : QECEvent → Bool
  | .surgery g          => decide (1 ≤ g.tau_s)
  | .magicSurgery _ gs  => gs.all (fun g => decide (1 ≤ g.tau_s))

def programWf (p : QECProgram) : Bool

structure SurgeryLayout

def gateCount (g : SurgeryGadget) : Nat

def roundLen (g : SurgeryGadget) : Nat

def gadgetLen (g : SurgeryGadget) : Nat

def emitRound (L : SurgeryLayout) (g : SurgeryGadget)
    (t0 rid : Nat) : List SysCall

def emitGadget (L : SurgeryLayout) (g : SurgeryGadget)
    (t base : Nat) : List SysCall

def compileGadgets (L : SurgeryLayout) :
    List SurgeryGadget → Nat → Nat → List SysCall
  | [],      _, _    => []
  | g :: gs, t, base =>
      emitGadget L g t base
      ++ compileGadgets L gs (t + gadgetLen g) (base + g.tau_s)

def gadgetsRounds (gs : List SurgeryGadget) : Nat

def gadgetsDuration (gs : List SurgeryGadget) : Nat

def eventRounds : QECEvent → Nat
  | .surgery g         => g.tau_s
  | .magicSurgery _ gs => gadgetsRounds gs

def eventDuration : QECEvent → Nat
  | .surgery g         => gadgetLen g
  | .magicSurgery _ gs => 1 + gadgetsDuration gs

def eventSyscallCount : QECEvent → Nat
  | .surgery g         => gadgetLen g
  | .magicSurgery _ gs => 1 + (gs.map gadgetLen).sum

def compileEvent (L : SurgeryLayout) (t base : Nat) : QECEvent → List SysCall
  | .surgery g => emitGadget L g t base
  | .magicSurgery factory gs =>
      { kind

def compileEvents (L : SurgeryLayout) :
    QECProgram → Nat → Nat → List SysCall
  | [],      _, _    => []
  | e :: es, t, base =>
      compileEvent L t base e
      ++ compileEvents L es (t + eventDuration e) (base + eventRounds e)

def compileQECProgram (L : SurgeryLayout) (p : QECProgram)
    (t0 : Nat

def programSyscallCount (p : QECProgram) : Nat

def programRounds (p : QECProgram) : Nat

def decode_ids_unique_ok (sched : List SysCall) : Bool

private theorem range'_append_one (s m n : Nat) :
    List.range' s m ++ List.range' (s + m) n = List.range' s (m + n)

theorem decodeIds_emitRound (L : SurgeryLayout) (g : SurgeryGadget)
    (t0 rid : Nat) : decodeIds (emitRound L g t0 rid) = [rid]

theorem decodeIds_emitGadget (L : SurgeryLayout) (g : SurgeryGadget)
    (t base : Nat) :
    decodeIds (emitGadget L g t base) = List.range' base g.tau_s

theorem decodeIds_compileGadgets (L : SurgeryLayout) :
    ∀ (gs : List SurgeryGadget) (t base : Nat),
      decodeIds (compileGadgets L gs t base)
        = List.range' base (gadgetsRounds gs)
  | [], _, _ => by simp [compileGadgets, decodeIds, gadgetsRounds]
  | g :: gs, t, base =>

theorem decodeIds_compileEvent (L : SurgeryLayout) (t base : Nat)
    (e : QECEvent) :
    decodeIds (compileEvent L t base e) = List.range' base (eventRounds e)

theorem decodeIds_compileEvents (L : SurgeryLayout) :
    ∀ (p : QECProgram) (t base : Nat),
      decodeIds (compileEvents L p t base)
        = List.range' base (programRounds p)
  | [], _, _ => by simp [compileEvents, decodeIds, programRounds]
  | e :: es, t, base =>

theorem compileQECProgram_decodeIds_nodup
    (L : SurgeryLayout) (p : QECProgram) (t0 round0 : Nat) :
    (decodeIds (compileQECProgram L p t0 round0)).Nodup

theorem emitRound_length (L : SurgeryLayout) (g : SurgeryGadget)
    (t0 rid : Nat) : (emitRound L g t0 rid).length = roundLen g

theorem emitGadget_length (L : SurgeryLayout) (g : SurgeryGadget)
    (t base : Nat) : (emitGadget L g t base).length = gadgetLen g

theorem compileGadgets_length (L : SurgeryLayout) :
    ∀ (gs : List SurgeryGadget) (t base : Nat),
      (compileGadgets L gs t base).length = (gs.map gadgetLen).sum
  | [], _, _ => rfl
  | g :: gs, t, base =>

theorem compileQECProgram_length (L : SurgeryLayout) :
    ∀ (p : QECProgram) (t0 round0 : Nat),
      (compileQECProgram L p t0 round0).length = programSyscallCount p
  | [], _, _ => rfl
  | e :: es, t, base =>

def demoLayout : SurgeryLayout

def demo_merge_x : SurgeryGadget

def demo_merge_z : SurgeryGadget

def demo_inj (j : Nat) : SurgeryGadget

def demoProgram : QECProgram

theorem demoProgram_wf : programWf demoProgram = true

def demoCompiled : List SysCall

theorem demoCompiled_passes :
    checkScheduleOn adder_d3_magicStock demoCompiled = true

theorem demoCompiled_decode_ids_unique :
    decode_ids_unique_ok demoCompiled = true

theorem demoCompiled_fails_without_reaction_budget :
    checkScheduleOn
      { adder_d3_magicStock with
          decoder

theorem demoCompiled_count :
    demoCompiled.length = programSyscallCount demoProgram

theorem demoCompiled_count_value : programSyscallCount demoProgram = 44

def ge2021Layout : SurgeryLayout

def ge2021_merge (hz : List (List Bool)) (cx cz : List (List Bool))
    (tp : List Bool) : SurgeryGadget

def ge2021Probe : QECProgram

def ge2021ProbeCompiled : List SysCall

theorem ge2021_probe_passes :
    checkScheduleOn ge2021_logical ge2021ProbeCompiled = true

theorem ge2021_probe_fails_without_reaction_budget :
    checkScheduleOn
      { ge2021_logical with
          decoder

theorem ge2021_probe_decode_ids_unique :
    decode_ids_unique_ok ge2021ProbeCompiled = true

theorem ge2021_probe_count :
    ge2021ProbeCompiled.length = programSyscallCount ge2021Probe

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

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 verifiedToffoli : Nat

theorem verifiedToffoli_eq_composed_circuit (W : Nat) (T : Nat → Nat) :
    EGate.toffoli (modExp 10 W 2048 T 246 1024) = verifiedToffoli

theorem verifiedToffoli_eq_value_correct_circuit
    (W : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start : Nat) :
    EGate.toffoli (modExpAt 10 W 2048 Tfam q_start 246 1024) = verifiedToffoli

theorem magicBudget_is_paper_formula :
    (FormalRV.System.RSA2048.magicBudget : ℚ) = toffoliCount 2048 3072 11

theorem verifiedToffoli_le_magicBudget :
    verifiedToffoli ≤ FormalRV.System.RSA2048.magicBudget

theorem composed_circuit_within_budget (W : Nat) (T : Nat → Nat) :
    EGate.toffoli (modExp 10 W 2048 T 246 1024) ≤ FormalRV.System.RSA2048.magicBudget

theorem verifiedToffoli_CCZMagic :
    numCCZMagic (circuitToPPM 8 (modmultBlock verifiedToffoli 0)) = verifiedToffoli

theorem verifiedToffoli_Meas :
    numMeas (circuitToPPM 8 (modmultBlock verifiedToffoli 0)) = 3 * verifiedToffoli

def verifiedFactoriesNeeded : Nat

theorem verifiedFactoriesNeeded_value : verifiedFactoriesNeeded = 1075

theorem verifiedFactories_le_provisioned :
    verifiedFactoriesNeeded ≤ FormalRV.System.RSA2048.factoriesNeeded

def reactionLimitedDepthUs : Nat

theorem reactionLimitedDepthUs_value : reactionLimitedDepthUs = 25789931520

theorem depth_below_magic_pipeline :
    reactionLimitedDepthUs ≤
      deliveryLatency ccz_spec_qianxu 15
        + magicSupplyTimeUs verifiedToffoli 1093 ccz_spec_qianxu

theorem windowed_rsa2048_runtime_concrete :
    circuitRuntimeUs reactionLimitedDepthUs verifiedToffoli 1093 ccz_spec_qianxu 15
      = deliveryLatency ccz_spec_qianxu 15
        + magicSupplyTimeUs verifiedToffoli 1093 ccz_spec_qianxu

theorem windowed_rsa2048_runtime_value :
    circuitRuntimeUs reactionLimitedDepthUs verifiedToffoli 1093 ccz_spec_qianxu 15
      = 28314672015

theorem rsa2048_resource_after_composed_circuit (W : Nat) (T : Nat → Nat) :
    EGate.toffoli (modExp 10 W 2048 T 246 1024) = verifiedToffoli
    ∧ verifiedToffoli ≤ FormalRV.System.RSA2048.magicBudget
    ∧ numCCZMagic (circuitToPPM 8 (modmultBlock verifiedToffoli 0)) = verifiedToffoli
    ∧ verifiedFactoriesNeeded ≤ FormalRV.System.RSA2048.factoriesNeeded
    ∧ circuitRuntimeUs reactionLimitedDepthUs verifiedToffoli 1093 ccz_spec_qianxu 15
        = deliveryLatency ccz_spec_qianxu 15
          + magicSupplyTimeUs verifiedToffoli 1093 ccz_spec_qianxu

inductive ZoneRole
  | Memory     -- long-term storage of logical qubits
  | Processor  --

instance : BEq ZoneRole

structure Zone

inductive ChannelKind
  | AncillaSupply    -- Ancilla zone → Processor (fresh helpers)
  | MagicSupply      -- Factory zone → Processor (T / CCZ states)
  | MemorySave       -- Processor → Memory (commit logical qubit)
  | MemoryLoad       -- Memory → Processor (fetch logical qubit)
  | InterRouting     -- generic transit (any-to-any)
  deriving DecidableEq, Repr

instance : BEq ChannelKind

structure Channel

inductive SysCallKind
  /-- Single-qubit gate, parameterised by gate id. -/
  | Gate1q          (qubit : Nat) (gate_id : Nat)
  /-- Two-qubit gate (e.g. CZ, MS, CR). -/
  | Gate2q          (q1 q2 : Nat) (gate_id : Nat)
  /-- Single-qubit projective measurement (Z-basis default; `basis`
      indexes alternative bases like X, Y).  Non-unitary; produces
      a classical bit.  Required for magic-state injection and
      syndrome readout. -/
  | Measure         (qubit : Nat) (basis : Nat)
  /-- Transit a qubit through a channel between zones. -/
  | TransitQubit    (qubit : Nat) (channel_id : Nat)

structure SysCall

abbrev Schedule

structure Architecture

def find_zone (arch : Architecture) (zid : Nat) : Option Zone

def find_channel (arch : Architecture) (cid : Nat) : Option Channel

def SysCall.duration_us (sc : SysCall) : Nat

def latency_ok (arch : Architecture) (sched : Schedule) : Prop

def capacity_ok (arch : Architecture) (sched : Schedule) : Prop

def channel_bandwidth_ok (arch : Architecture) (sched : Schedule) : Prop

def verifies (arch : Architecture) (sched : Schedule) : Prop

abbrev InitialPlacement

def InitialPlacement.zone_of (placement : InitialPlacement) (qubit : Nat) :
    Option Nat

def latest_transit_for_qubit (sched : Schedule) (qubit : Nat) (t : Nat) :
    Option (Nat × Nat)

def qubit_zone_at (placement : InitialPlacement) (arch : Architecture)
    (sched : Schedule) (qubit : Nat) (t : Nat) : Option Nat

def zone_occupancy_at (placement : InitialPlacement) (arch : Architecture)
    (sched : Schedule) (z_id : Nat) (t : Nat) (qubit_universe : List Nat) :
    Nat

def transit_boundaries (sched : Schedule) : List Nat

def capacity_ok_strict (placement : InitialPlacement) (arch : Architecture)
    (sched : Schedule) (qubit_universe : List Nat) : Prop

def qubit_discarded_at (sched : Schedule) (qubit : Nat) (t : Nat) : Bool

def qubit_alive_at (sched : Schedule) (qubit : Nat) (t : Nat) : Bool

def zone_occupancy_at_alive (placement : InitialPlacement)
    (arch : Architecture) (sched : Schedule) (z_id : Nat) (t : Nat)
    (qubit_universe : List Nat) : Nat

def capacity_ok_strict_alive (placement : InitialPlacement)
    (arch : Architecture) (sched : Schedule)
    (qubit_universe : List Nat) : Prop

def decoder_queue_depth_at (sched : Schedule) (t : Nat) : Nat

def decoder_queue_ok (sched : Schedule) (n_decoders : Nat) : Prop

def syscall_precondition_met
    (placement : InitialPlacement) (arch : Architecture)
    (sched : Schedule) (sc : SysCall) : Bool

def semantically_correct
    (placement : InitialPlacement) (arch : Architecture)
    (sched : Schedule) : Bool

def per_ccz_atom_demand_per_role : Nat

def max_ccz_parallelism (arch : Architecture) : Nat

def min_runtime_us (arch : Architecture) (n_ccz : Nat)
    (tau_ccz_us : Nat) : Nat

structure MagicStateSpec

def ccz_spec_qianxu : MagicStateSpec

def t_spec_qianxu : MagicStateSpec

inductive LogicalGateKind
  /-- Logical Hadamard on a single logical qubit. -/
  | LH       (q : Nat)
  /-- Logical T gate (non-Clifford, requires magic state). -/
  | LT       (q : Nat)
  /-- Logical CNOT (Clifford). -/
  | LCNOT    (ctrl tgt : Nat)
  /-- Logical CCZ (non-Clifford, requires |CCZ⟩ magic state). -/
  | LCCZ     (q1 q2 q3 : Nat)
  /-- Logical CCX (Toffoli) = H_q3; CCZ q1 q2 q3; H_q3 in
      surface-code FT. -/
  | LCCX     (q1 q2 q3 : Nat)

structure LogicalGate

structure LogicalLayout

def physical_of_logical (layout : LogicalLayout) (l_id : Nat) : Option Nat

def LogicalGateKind.targets (k : LogicalGateKind) : List Nat

def assignments_cover_gates (layout : LogicalLayout) : Bool

def gate_indices_valid (lg : LogicalGate) (sched : Schedule) : Bool

def all_gates_have_valid_indices (layout : LogicalLayout)
    (sched : Schedule) : Bool

def gates_time_ordered (layout : LogicalLayout) : Bool

def consistent (layout : LogicalLayout) (sched : Schedule) : Bool

structure LogicalStep

abbrev LogicalSchedule

def find_impl (layout : LogicalLayout) (step_id : Nat) : Option LogicalGate

def step_implemented (step : LogicalStep) (layout : LogicalLayout)
    (psched : Schedule) : Bool

def physical_implements_logical
    (lsched : LogicalSchedule) (layout : LogicalLayout)
    (psched : Schedule) : Bool

def fid_step (acc : Nat) (f_x1e6 : Nat) : Nat

def schedule_fidelity_ppm (arch : Architecture) (sched : Schedule)
    (f_1q_x1e6 f_2q_x1e6 f_meas_x1e6 : Nat) : Nat

def neutral_atom_mini : Architecture

def trapped_ion_mini : Architecture

def superconducting_mini : Architecture

example : verifies neutral_atom_mini []

example : verifies trapped_ion_mini []

example : verifies superconducting_mini []

example :
    (neutral_atom_mini.find_zone 0).map Zone.role = some ZoneRole.Memory

example :
    (neutral_atom_mini.find_channel 1).map Channel.kind
      = some ChannelKind.MagicSupply

example : superconducting_mini.t_coherence_us = 100

structure CodeBlockBinding

structure LogicalQubitBinding

structure CodedLogicalLayout

def find_block (clayout : CodedLogicalLayout) (bid : Nat) :
    Option CodeBlockBinding

def find_binding (clayout : CodedLogicalLayout) (lid : Nat) :
    Option LogicalQubitBinding

def blocks_have_correct_size (clayout : CodedLogicalLayout) : Bool

def bindings_in_range (clayout : CodedLogicalLayout) : Bool

def all_gate_targets_bound (clayout : CodedLogicalLayout) : Bool

def consistent (clayout : CodedLogicalLayout) : Bool

def syscall_acts_on (sc : SysCall) : List Nat

def allowed_atoms_for_logicals
    (clayout : CodedLogicalLayout) (logical_ids : List Nat) : List Nat

def gate_impl_in_scope (clayout : CodedLogicalLayout)
    (lg : LogicalGate) (psched : Schedule) : Bool

def impls_in_scope (clayout : CodedLogicalLayout) (psched : Schedule) : Bool

def gate_impl_in_time_window (lg : LogicalGate) (psched : Schedule) : Bool

def impls_time_consistent (clayout : CodedLogicalLayout)
    (psched : Schedule) : Bool

abbrev scheduleWallclockUs : 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 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_singleton (xs : List SysCall) :
    seqManySchedules [xs] = xs

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

def reactionLimitedModel (decodeLatencyCycles factory : Nat) : CostModel

theorem reactionLimited_time (decodeLatencyCycles factory : Nat)
    (hw : Hardware) (w : Workload) (c : QECCode) (ow p : Nat) :
    (estimateWith (reactionLimitedModel decodeLatencyCycles factory) hw w c ow p).time_us_tenths
      = w.n_toff * decodeLatencyCycles * hw.cycle_time_us_tenths

theorem time_mono_decodeLatency (L L' factory : Nat)
    (hw : Hardware) (w : Workload) (c : QECCode) (ow p : Nat) (h : L ≤ L') :
    (estimateWith (reactionLimitedModel L factory) hw w c ow p).time_us_tenths
      ≤ (estimateWith (reactionLimitedModel L' factory) hw w c ow p).time_us_tenths

def rsa2048_runtime (L : Nat) : Nat

theorem rsa2048_runtime_eq (L : Nat) :
    (estimateWith (reactionLimitedModel L 0) { cycle_time_us_tenths

theorem rsa2048_at_10 : rsa2048_runtime 10 = 270_000_000_000

theorem rsa2048_at_20 : rsa2048_runtime 20 = 540_000_000_000

theorem rsa2048_at_27 : rsa2048_runtime 27 = 729_000_000_000

theorem rsa2048_at_40 : rsa2048_runtime 40 = 1_080_000_000_000

theorem crossover_at_distance :
    rsa2048_runtime 27 = ReactionLimitedRuntime.dCycleRuntime 2_700_000_000 27 10

theorem coupling_10 :
    rsa2048_runtime 10 = 270_000_000_000
    ∧ arrivalsPerWindow 6200 10 = 62_000

theorem coupling_20 :
    rsa2048_runtime 20 = 540_000_000_000
    ∧ arrivalsPerWindow 6200 20 = 124_000

theorem decode_latency_drives_time_and_lanes
    (L p factory : Nat) (hw : Hardware) (w : Workload) (c : QECCode) (ow pp : Nat) :
    (estimateWith (reactionLimitedModel L factory) hw w c ow pp).time_us_tenths
        = w.n_toff * L * hw.cycle_time_us_tenths
    ∧ arrivalsPerWindow p L = p * L

def arrivalsPerWindow (patches decodeLatency : Nat) : Nat

def servicesPerWindow (lanes : Nat) : Nat

def backlogFree (patches decodeLatency lanes : Nat) : Bool

def backlogGrowthPerWindow (patches decodeLatency lanes : Nat) : Nat

def backlogAfter (k patches decodeLatency lanes : Nat) : Nat

theorem provisioned_no_backlog (k patches decodeLatency lanes : Nat)
    (h : backlogFree patches decodeLatency lanes = true) :
    backlogAfter k patches decodeLatency lanes = 0

theorem underprovisioned_unbounded_backlog (patches decodeLatency lanes : Nat)
    (h : backlogFree patches decodeLatency lanes = false) (bound : Nat) :
    ∃ k, bound < backlogAfter k patches decodeLatency lanes

def outstandingWork (k patches decodeLatency lanes : Nat) : Nat

theorem underprovisioned_work_diverges (patches decodeLatency lanes : Nat)
    (h : backlogFree patches decodeLatency lanes = false) (bound : Nat) :
    ∃ k, bound < outstandingWork k patches decodeLatency lanes

theorem ge2021_provisioned_62000 (k : Nat) : backlogAfter k 6200 10 62000 = 0

theorem ge2021_underprovisioned_6200 (bound : Nat) :
    ∃ k, bound < backlogAfter k 6200 10 6200

theorem ge2021_threshold : arrivalsPerWindow 6200 10 = 62_000

def reactionTime_tenthsUs : Nat

def reactionLimitedRuntime (toffoliDepth : Nat) : Nat

def dCycleRuntime (toffoli d cycle_tenthsUs : Nat) : Nat

theorem rsa2048_dcycle : dCycleRuntime 2_700_000_000 27 10 = 729_000_000_000

theorem rsa2048_reaction_limited : reactionLimitedRuntime 2_700_000_000 = 270_000_000_000

theorem gap_is_dcycle_vs_reaction :
    2 * reactionLimitedRuntime 2_700_000_000 ≤ dCycleRuntime 2_700_000_000 27 10
    ∧ dCycleRuntime 2_700_000_000 27 10 ≤ 3 * reactionLimitedRuntime 2_700_000_000

def rsa2048_patches : Nat

def syndromeRoundsPerSec : Nat

def realtimeDecodeLoad : Nat

theorem realtimeDecodeLoad_value : realtimeDecodeLoad = 6_200_000_000

theorem reaction_limited_assumes_decoder (toffoli : Nat) :
    reactionLimitedRuntime toffoli = toffoli * reactionTime_tenthsUs

def decoderThroughputOk (patches decodeLatencyCycles nLanes : Nat) : Bool

def decoderThroughputInv (patches decodeLatencyCycles nLanes : Nat) : SpaceTimeInvariant

theorem ge2021_decode_lanes_worstcase : 6200 * 10 = 62_000

theorem ge2021_decoder_oneper_patch_fails :
    decoderThroughputOk 6200 10 6200 = false

theorem ge2021_decoder_provisioned_ok :
    decoderThroughputOk 6200 10 62_000 = true

def modexpDepthFloorCycles : Nat

theorem modexpDepthFloor_value : modexpDepthFloorCycles = 247_726_080

theorem runtime_is_100x_depth_floor :
    100 * modexpDepthFloorCycles ≤ 27_000_000_000

theorem mixed_cost_pushes_above_8h :
    28_800_000_000 < (85 * 10 + 15 * 27) * 27_000_000

def surfaceCycleTime (tGate tMeasure tReset gateLayers : Nat) : Nat

def hwOfLatencies (tGate tMeasure tReset gateLayers : Nat) : Hardware

theorem runtime_with_measurement_latency
    (T L factory d tGate tMeasure tReset gateLayers ow p : Nat) :
    (estimateWith (surfaceModel factory) (hwOfLatencies tGate tMeasure tReset gateLayers)
        (shorWorkload T L) (surfaceCodeD d) ow p).time_us_tenths
      = T * d * surfaceCycleTime tGate tMeasure tReset gateLayers

theorem time_mono_measurementLatency
    (T L factory d tGate tM tM' tReset gateLayers ow p : Nat) (h : tM ≤ tM') :
    (estimateWith (surfaceModel factory) (hwOfLatencies tGate tM tReset gateLayers)
        (shorWorkload T L) (surfaceCodeD d) ow p).time_us_tenths
      ≤ (estimateWith (surfaceModel factory) (hwOfLatencies tGate tM' tReset gateLayers)
        (shorWorkload T L) (surfaceCodeD d) ow p).time_us_tenths

def rsa2048_time_at_tMeasure (tMeasure : Nat) : Nat

theorem rsa2048_tM_5 : rsa2048_time_at_tMeasure 5 = 729_000_000_000

theorem rsa2048_tM_15 : rsa2048_time_at_tMeasure 15 = 1_458_000_000_000

theorem rsa2048_tM_35 : rsa2048_time_at_tMeasure 35 = 2_916_000_000_000

theorem measurement_latency_changes_time :
    rsa2048_time_at_tMeasure 5 ≠ rsa2048_time_at_tMeasure 15

def syndromeAncillaPerPatch (d : Nat) : Nat

theorem syndromeAncilla_d27 : syndromeAncillaPerPatch 27 = 1404

def totalSyndromeRounds (nToff d : Nat) : Nat

def totalPhysicalSyndromeMeas (nLogical d nToff : Nat) : Nat

theorem syndrome_overhead_scales_with_all_qubits (d nToff a b : Nat) (h : a ≤ b) :
    totalPhysicalSyndromeMeas a d nToff ≤ totalPhysicalSyndromeMeas b d nToff

structure DepEdge

structure DepGraph

def respectsCausality (sched : List SysCall) (g : DepGraph) : Bool

def causalityInv (g : DepGraph) : SpaceTimeInvariant

theorem no_self_dependency (sched : List SysCall) (g : DepGraph)
    (h : respectsCausality sched g = true)
    (e : DepEdge) (he : e ∈ g.edges) (heq : e.before = e.after)
    (u : SysCall) (hu : sched[e.before]? = some u) (hpos : u.begin_us < u.end_us) :
    False

def toffoliSched : List SysCall

def toffoliDeps : DepGraph

example : respectsCausality toffoliSched toffoliDeps = true

def badToffoliSched : List SysCall

example : respectsCausality badToffoliSched toffoliDeps = false

def toffoliCtx : SystemCtx

example : checkAll (baseInvariants ++ [causalityInv toffoliDeps]) toffoliCtx = true

def badToffoliCtx : SystemCtx

example : checkAll (baseInvariants ++ [causalityInv toffoliDeps]) badToffoliCtx = false

example : checkAll baseInvariants badToffoliCtx = true

example : (causalityInv toffoliDeps).check badToffoliCtx = false

theorem causal_chain_floor (sched : List SysCall) (g : DepGraph)
    (h : respectsCausality sched g = true)
    (e1 e2 : DepEdge) (h1 : e1 ∈ g.edges) (h2 : e2 ∈ g.edges)
    (hmid : e1.after = e2.before)
    (u v w : SysCall)
    (hu : sched[e1.before]? = some u) (hv : sched[e1.after]? = some v)
    (hw : sched[e2.after]? = some w)
    (hvpos : v.begin_us ≤ v.end_us) :
    u.end_us ≤ w.begin_us

def chainMinTotal : List (SysCall × Nat) → Nat
  | []            => 0
  | (_, d) :: rest => d + chainMinTotal rest

def lastEnd : List (SysCall × Nat) → Nat
  | []            => 0
  | [(op, _)]     => op.end_us
  | _ :: rest     => lastEnd rest

def MinChain : List (SysCall × Nat) → Prop
  | []                          => True
  | [(op, d)]                   => op.begin_us + d ≤ op.end_us
  | (op1, d1) :: (op2, d2) :: r =>
      op1.begin_us + d1 ≤ op1.end_us ∧ op1.end_us ≤ op2.begin_us
      ∧ MinChain ((op2, d2) :: r)

theorem critical_path_lower_bound :
    ∀ (op0 : SysCall) (d0 : Nat) (rest : List (SysCall × Nat)),
      MinChain ((op0, d0) :: rest) →
      op0.begin_us + chainMinTotal ((op0, d0) :: rest)
        ≤ lastEnd ((op0, d0) :: rest)
  | op0, d0, [], h =>

theorem critical_path_two (op0 op1 : SysCall) (d0 d1 : Nat)
    (hmin0 : op0.begin_us + d0 ≤ op0.end_us)
    (hdep  : op0.end_us ≤ op1.begin_us)
    (hmin1 : op1.begin_us + d1 ≤ op1.end_us) :
    op0.begin_us + (d0 + d1) ≤ op1.end_us

theorem serial_chain_depth (τ : Nat) (begin_ : Nat → Nat)
    (hdep : ∀ i, begin_ i + τ ≤ begin_ (i + 1)) (n : Nat) :
    begin_ 0 + n * τ ≤ begin_ n

example (τ : Nat) (b : Nat → Nat) (h : ∀ i, b i + τ ≤ b (i + 1)) :
    b 0 + 2048 * τ ≤ b 2048

def modexpToffoliDepth (mults adds_per_mult adder_depth : Nat) : Nat

def runtimeFloorCycles (depth tau_toff_cycles : Nat) : Nat

theorem runtimeFloor_is_lower_bound (τ : Nat) (begin_ : Nat → Nat)
    (hdep : ∀ i, begin_ i + τ ≤ begin_ (i + 1)) (depth : Nat) :
    begin_ 0 + runtimeFloorCycles depth τ ≤ begin_ depth

inductive OpKind

structure DeviceOp

def DeviceOp.end_t (op : DeviceOp) : Nat

abbrev DSchedule

structure Device

def DeviceOp.isDecode (op : DeviceOp) : Bool

def DeviceOp.activeAt (op : DeviceOp) (t : Nat) : Bool

def opsTimeOverlap (a b : DeviceOp) : Bool

def DeviceOp.conflictsWith (a b : DeviceOp) : Bool

def conflictFree : DSchedule → Bool
  | []        => true
  | op :: rest => rest.all (fun o => ! op.conflictsWith o) && conflictFree rest

def findOp (sched : DSchedule) (oid : Nat) : Option DeviceOp

def depsRespected (sched : DSchedule) : Bool

def boundaries (sched : DSchedule) : List Nat

def activeFootprintSize (sched : DSchedule) (t : Nat) : Nat

theorem activeFootprintSize_cons (o : DeviceOp) (rest : DSchedule) (t : Nat) :
    activeFootprintSize (o :: rest) t
      = (if o.activeAt t then o.footprint.length else 0) + activeFootprintSize rest t

def capacityRespected (dev : Device) (sched : DSchedule) : Bool

def decoderQueueRespected (dev : Device) (sched : DSchedule) : Bool

def reactionRespected (dev : Device) (sched : DSchedule) : Bool

def scheduleValid (dev : Device) (sched : DSchedule) : Bool

theorem scheduleValid_components (dev : Device) (sched : DSchedule)
    (h : scheduleValid dev sched = true) :
    conflictFree sched = true ∧ depsRespected sched = true ∧ capacityRespected dev sched = true
    ∧ decoderQueueRespected dev sched = true ∧ reactionRespected dev sched = true

def DeviceOp.placementEffect (op : DeviceOp) (p : Placement) : Placement

def evolvePlacement (sched : DSchedule) (p0 : Placement) : Placement

theorem evolvePlacement_cons (op : DeviceOp) (rest : DSchedule) (p0 : Placement) :
    evolvePlacement (op :: rest) p0 = evolvePlacement rest (op.placementEffect p0)

def DeviceOp.isStatic (op : DeviceOp) : Bool

theorem placementEffect_static (op : DeviceOp) (p : Placement) (h : op.isStatic = true) :
    op.placementEffect p = p

theorem evolvePlacement_static : ∀ (sched : DSchedule) (p0 : Placement),
    sched.all DeviceOp.isStatic = true → evolvePlacement sched p0 = p0
  | [], _, _ => rfl
  | op :: rest, p0, h =>

abbrev Resource

structure ResOp

def ResOp.footprint (op : ResOp) : List Resource

def ResOp.routingQubits (op : ResOp) : Nat

def timeOverlap (a b : ResOp) : Bool

def overlap (s t : List Resource) : Bool

def conflict (a b : ResOp) : Bool

def scheduleValid (ops : List ResOp) : Bool

theorem no_conflict_if_disjoint_time (a b : ResOp) (h : timeOverlap a b = false) :
    conflict a b = false

theorem no_conflict_if_disjoint_footprint (a b : ResOp)
    (h : overlap a.footprint b.footprint = false) : conflict a b = false

theorem routingQubits_is_reserved (op : ResOp) :
    op.footprint.length = op.operands.length + op.routingQubits

theorem conflict_no_routing (a b : ResOp) (ha : a.routing = []) (hb : b.routing = []) :
    conflict a b = (timeOverlap a b && overlap a.operands b.operands)

def latticeSurgeryOp (patch ancillaPath : List Resource) (clk : Nat) : ResOp

theorem litinski_simultaneous_conflict (patch1 path1 patch2 path2 : List Resource) (clk : Nat) :
    conflict (latticeSurgeryOp patch1 path1 clk) (latticeSurgeryOp patch2 path2 clk)
      = overlap (patch1 ++ path1) (patch2 ++ path2)

theorem litinski_routingQubits (patch ancillaPath : List Resource) (clk : Nat) :
    (latticeSurgeryOp patch ancillaPath clk).routingQubits = ancillaPath.length

def transitOp (src dst : Resource) (corridor : List Resource) (begin_t dur_t : Nat) : ResOp

theorem transit_conflict_is_corridor_overlap
    (s1 d1 s2 d2 : Resource) (c1 c2 : List Resource) (b dur : Nat) :
    conflict (transitOp s1 d1 c1 b dur) (transitOp s2 d2 c2 b dur)
      = (decide (0 < dur) && overlap ([s1, d1] ++ c1) ([s2, d2] ++ c2))

def gA : ResOp

def gC : ResOp

theorem shared_routing_conflicts : conflict gA gC = true

theorem shared_routing_ok_when_serialized :
    scheduleValid [gA, { gC with begin_t

theorem disjoint_routing_parallel_ok :
    scheduleValid [gA, { gC with routing

def readyAt (inputEnds : List Nat) (t : Nat) : Bool

theorem must_wait_for_inputs (inputEnds : List Nat) (t e : Nat) (he : e ∈ inputEnds) (hlt : t < e) :
    readyAt inputEnds t = false

abbrev Placement

def Placement.set (p : Placement) (r : Resource) (v : Option Nat) : Placement

inductive RoutingKind

def RoutingKind.applyPlacement : RoutingKind → Placement → Placement
  | .transport q src dst, p => (p.set src none).set dst (some q)
  | .surgery, p => p

structure RoutedOp

def routedConflict (a b : RoutedOp) : Bool

theorem routedConflict_ignores_kind (a b : RoutedOp) (k : RoutingKind) :
    routedConflict { a with kind

theorem surgery_preserves_placement (p : Placement) :
    RoutingKind.surgery.applyPlacement p = p

theorem transport_relocates (q src dst : Resource) (p : Placement) (h : dst ≠ src) :
    (RoutingKind.transport q src dst).applyPlacement p dst = some q
    ∧ (RoutingKind.transport q src dst).applyPlacement p src = none

theorem transport_changes_but_surgery_preserves
    (q src dst : Resource) (p : Placement) (h : dst ≠ src) (hq : p src = some q) (hfree : p dst = none) :
    (RoutingKind.transport q src dst).applyPlacement p ≠ p
    ∧ RoutingKind.surgery.applyPlacement p = p

def adder_n1_syscalls : List SysCall

def adder_demo_arch : ZonedArch

def adder_demo_opCap : OperationCapacityModel

def adder_demo_slotCap : SlotCapacityModel

def adder_demo_ancillaModel : AncillaModel

def adder_demo_t_react_us    : Nat

def adder_demo_window_us     : Nat

def adder_demo_max_per_window : Nat

theorem adder_n1_strict_system_ok :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        adder_demo_arch
        adder_demo_opCap
        adder_demo_slotCap
        adder_demo_ancillaModel
        adder_n1_syscalls
        adder_demo_t_react_us
        adder_demo_window_us
        adder_demo_max_per_window = true

def adder_n1_wallclock_us : Nat

def adder_n1_syscall_count : Nat

def adder_n1_gate2q_count : Nat

def adder_n1_measure_count : Nat

def adder_n1_decode_count : Nat

def adder_n1_feedback_count : Nat

def adder_n1_fresh_ancilla_count : Nat

theorem adder_n1_wallclock_value :
    adder_n1_wallclock_us = 48

theorem adder_n1_syscall_count_value :
    adder_n1_syscall_count = 48

theorem adder_n1_gate2q_count_value :
    adder_n1_gate2q_count = 18

theorem adder_n1_measure_count_value :
    adder_n1_measure_count = 9

theorem adder_n1_decode_count_value :
    adder_n1_decode_count = 9

theorem adder_n1_feedback_count_value :
    adder_n1_feedback_count = 3

theorem adder_n1_fresh_ancilla_count_value :
    adder_n1_fresh_ancilla_count = 9

structure AdderSystemClaim

def optimistic_parallel_adder_claim : AdderSystemClaim

theorem optimistic_adder_claim_underestimates_verified_schedule :
    optimistic_parallel_adder_claim.claimed_wallclock_us
      < adder_n1_wallclock_us

theorem optimistic_adder_claim_understates_verified_gate2qs :
    optimistic_parallel_adder_claim.claimed_gate2q_count
      < adder_n1_gate2q_count

def gate2q_capacity_lower_bound_us
    (num_gate2q max_parallel gate2q_us : Nat) : Nat

theorem adder_n1_gate2q_capacity_lower_bound_value :
    gate2q_capacity_lower_bound_us
        adder_n1_gate2q_count
        adder_demo_opCap.max_gate2q_active
        1 = 18

theorem optimistic_adder_claim_below_gate2q_capacity_lower_bound :
    optimistic_parallel_adder_claim.claimed_wallclock_us
      < gate2q_capacity_lower_bound_us
          adder_n1_gate2q_count
          adder_demo_opCap.max_gate2q_active
          1

def bad_parallel_adder_syscalls : List SysCall

theorem bad_parallel_adder_schedule_rejected :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        adder_demo_arch
        adder_demo_opCap
        adder_demo_slotCap
        adder_demo_ancillaModel
        bad_parallel_adder_syscalls
        adder_demo_t_react_us
        adder_demo_window_us
        adder_demo_max_per_window = false

example : adder_n1_syscalls.length = 3 * 16

def surfaceTile (d : Nat) : Nat

def rsa2048_logical : Nat

def rsa2048_dataPhysical (d : Nat) : Nat

def machineFitsRSA2048 (budget d : Nat) : Bool

theorem rsa2048_dataPhysical_d27 : rsa2048_dataPhysical 27 = 9_721_600

def machine100k : Nat

theorem machine100k_cannot_factor_rsa2048_d27 :
    machineFitsRSA2048 machine100k 27 = false

theorem rsa2048_space_lower_bound (budget : Nat)
    (h : machineFitsRSA2048 budget 27 = true) : 9_721_600 ≤ budget

theorem machine100k_infeasible_even_d3 :
    machineFitsRSA2048 machine100k 3 = false

theorem machine100k_holds_63_logical_d27 :
    machine100k / surfaceTile 27 = 63

theorem machine20M_fits_rsa2048_d27 :
    machineFitsRSA2048 20_000_000 27 = true

def connectivityInv (couples : Nat → Nat → Bool) : SpaceTimeInvariant

def nearestNeighbor1D (q1 q2 : Nat) : Bool

def nnSched : List SysCall

def nnCtx : SystemCtx

theorem nnCtx_connectivity_ok :
    (connectivityInv nearestNeighbor1D).check nnCtx = true

def longRangeSched : List SysCall

def longRangeCtx : SystemCtx

theorem longRange_rejected :
    (connectivityInv nearestNeighbor1D).check longRangeCtx = false

theorem nnCtx_fully_valid :
    checkAll (baseInvariants ++ [connectivityInv nearestNeighbor1D]) nnCtx = true

theorem longRange_ok_on_all_to_all :
    (connectivityInv (fun _ _ => true)).check longRangeCtx = true

def code422Q : FormalRV.Framework.QECCode

def w0 : Workload

example : rowWeight (code422Logical.selectZ [0]) = 2

theorem surgery_ancilla_is_verified_logical_weight :
    ((qldpcModel 0).ancilla code422Q w0 (rowWeight (code422Logical.selectZ [0])) 1).surgery = 2

example : rowWeight (code422Logical.selectZ [0, 1]) = 2

example : ((qldpcModel 0).ancilla code422Q w0 7 1).syndrome = 1

example : ((qldpcModel 0).ancilla code422Q w0 (rowWeight (code422Logical.selectZ [0])) 1).syndrome = 1

example : ((qldpcModel 0).ancilla code422Q w0 (rowWeight (code422Logical.selectZ [0])) 1).surgery = 2

example : ((qldpcModel 0).ancilla code422Q w0 (rowWeight (code422Logical.selectZ [0])) 1).total = 3

def parallelSched : List SysCall

def parallelCtx : SystemCtx

example : ∀ s ∈ parallelSched, s.begin_us = 0 ∧ s.end_us = 10

example : checkAll baseInvariants parallelCtx = true

def conflictCtx : SystemCtx

example : checkAll baseInvariants conflictCtx = false

def throughputViolCtx : SystemCtx

example : checkAll baseInvariants throughputViolCtx = false

def slowDecodeCtx : SystemCtx

example : checkAll baseInvariants slowDecodeCtx = false

def causalSched : Schedule

example : semantically_correct [] neutral_atom_mini causalSched = true

def badCausalSched : Schedule

example : semantically_correct [] neutral_atom_mini badCausalSched = false

example : exclusivity_ok parallelSched = true

def decodeDepthAt (sched : List SysCall) (t : Nat) : Nat

def decoderConcurrencyInv (n_decoders : Nat) : SpaceTimeInvariant

example (c : SystemCtx) (n : Nat) :
    checkAll (baseInvariants ++ [decoderConcurrencyInv n]) c
      = (checkAll baseInvariants c && (decoderConcurrencyInv n).check c)

def twoDecodeCtx : SystemCtx

example : checkAll (baseInvariants ++ [decoderConcurrencyInv 2]) twoDecodeCtx = true

example : checkAll (baseInvariants ++ [decoderConcurrencyInv 1]) twoDecodeCtx = false

example : checkAll baseInvariants twoDecodeCtx = true

def demoArch : ZonedArch

def winUs : Nat

def maxPerWin : Nat

def noDist : Nat → Nat

def ppm (start data anc dec : Nat) : List SysCall

def passSequential : List SysCall

theorem passSequential_ok : all_invariants_ok demoArch passSequential winUs maxPerWin noDist = true

def passParallelDistinct : List SysCall

theorem passParallelDistinct_ok :
    all_invariants_ok demoArch passParallelDistinct winUs maxPerWin noDist = true

theorem passParallelDistinct_overlaps : intervals_overlap 1 2 1 2 = true

def failAlias : List SysCall

theorem failAlias_fails : all_invariants_ok demoArch failAlias winUs maxPerWin noDist = false

theorem failAlias_exclusivity_false : exclusivity_ok failAlias = false

theorem failAlias_capacity_true : capacity_in_arch_ok demoArch failAlias = true

def failThroughput : List SysCall

theorem failThroughput_fails :
    all_invariants_ok demoArch failThroughput winUs maxPerWin noDist = false

theorem failThroughput_window_false : window_throughput_ok failThroughput winUs maxPerWin = false

theorem failThroughput_others_true :
    (capacity_in_arch_ok demoArch failThroughput && exclusivity_ok failThroughput) = true

def failDecodeSlow : List SysCall

theorem failDecodeSlow_fails :
    all_invariants_ok demoArch failDecodeSlow winUs maxPerWin noDist = false

theorem failDecodeSlow_decoder_react_false :
    decoder_react_ok demoArch.t_react_us failDecodeSlow = false

theorem failDecodeSlow_others_true :
    (capacity_in_arch_ok demoArch failDecodeSlow && exclusivity_ok failDecodeSlow
      && window_throughput_ok failDecodeSlow winUs maxPerWin) = true

structure FTSystem

abbrev timeLowerBound : HardwareSensitivity.HW → Nat → Nat → Nat

theorem ftSystem_naive_guarantee
    (S : FTSystem) (M : Nat)
    (hsched : S.sched = naiveSchedule M)
    (hdev : adequate S.dev) :
    scheduleValid S.dev S.sched = true
    ∧ reactionRespected S.dev S.sched = true
    ∧ schedulePeak S.sched ≤ S.dev.totalResources

def geSystem : FTSystem

theorem geSystem_guarantee :
    scheduleValid geSystem.dev geSystem.sched = true
    ∧ reactionRespected geSystem.dev geSystem.sched = true
    ∧ schedulePeak geSystem.sched ≤ geSystem.dev.totalResources

structure Transport

structure SystemCtx

structure SpaceTimeInvariant

def checkAll (invs : List SpaceTimeInvariant) (c : SystemCtx) : Bool

theorem checkAll_append (a b : List SpaceTimeInvariant) (c : SystemCtx) :
    checkAll (a ++ b) c = (checkAll a c && checkAll b c)

theorem checkAll_snoc (invs : List SpaceTimeInvariant) (inv : SpaceTimeInvariant)
    (c : SystemCtx) :
    checkAll (invs ++ [inv]) c = (checkAll invs c && inv.check c)

theorem checkAll_mono (invs extra : List SpaceTimeInvariant) (c : SystemCtx)
    (h : checkAll (invs ++ extra) c = true) : checkAll invs c = true

def capacityInv : SpaceTimeInvariant

def exclusivityInv : SpaceTimeInvariant

def latencyInv : SpaceTimeInvariant

def throughputInv : SpaceTimeInvariant

def decoderInv : SpaceTimeInvariant

def baseInvariants : List SpaceTimeInvariant

def movesOverlap (a b : Transport) : Bool

def sameDisplacement (a b : Transport) : Bool

def neutralAtomRigidMoveInv : SpaceTimeInvariant

def superconductingFixedCouplingInv : SpaceTimeInvariant

def demoArch : ZonedArch

def demoDist : Nat → Nat

def demoSched : List SysCall

def demoMoves : List Transport

def demoCtx : SystemCtx

example : checkAll baseInvariants demoCtx = true

example : checkAll (baseInvariants ++ [neutralAtomRigidMoveInv]) demoCtx
        = (checkAll baseInvariants demoCtx && neutralAtomRigidMoveInv.check demoCtx)

example : neutralAtomRigidMoveInv.check demoCtx = true

example : checkAll (baseInvariants ++ [neutralAtomRigidMoveInv]) demoCtx = true

def badMoveCtx : SystemCtx

example : neutralAtomRigidMoveInv.check badMoveCtx = false

example : checkAll (baseInvariants ++ [neutralAtomRigidMoveInv]) badMoveCtx = false

example : checkAll baseInvariants badMoveCtx = true

structure ArchZone

structure ZonedArch

def zone_of (arch : ZonedArch) (a : Nat) : Option ArchZone

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

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

def exclusivity_ok (sched : List SysCall) : Bool

def feedback_latency_ok (t_cycle_us : Nat) (sched : List SysCall) : Bool

def speed_limit_ok (v_max_um_per_us : Nat)
    (distance_fn : Nat → Nat) (sched : List SysCall) : Bool

def decoder_react_ok (t_react_us : Nat) (sched : List SysCall) : Bool

def latency_speed_ok (t_cycle_us v_max_um_per_us : Nat)
    (distance_fn : Nat → Nat) (sched : List SysCall) : Bool

def latency_speed_decoder_ok
    (t_cycle_us v_max_um_per_us t_react_us : Nat)
    (distance_fn : Nat → Nat) (sched : List SysCall) : Bool

def magicReq_count_in_window (sched : List SysCall) (t0 window : Nat) : Nat

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

def syndrome_bits_in_window (bits_per_measure : Nat) (sched : List SysCall)
    (t0 window_us : Nat) : Nat

def syndrome_bandwidth_ok (bits_per_measure window_us max_bits : Nat)
    (sched : List SysCall) : Bool

def measures_done_by (sched : List SysCall) (t : Nat) : Nat

def decodes_begun_by (sched : List SysCall) (t : Nat) : Nat

def syndrome_causality_ok (sched : List SysCall) : Bool

def magic_begun_by (sched : List SysCall) (t : Nat) : Nat

def magic_available_by (initial period per t : Nat) : Nat

def magic_supply_ok (initial period per : Nat) (sched : List SysCall) : Bool

def all_invariants_ok
    (arch : ZonedArch)
    (sched : List SysCall)
    (window_us max_per_window : Nat)
    (distance_fn : Nat → Nat) : Bool

structure OperationCapacityModel

def scheduleEventTimes (sched : List SysCall) : List Nat

def countActiveKindAt
    (predicate : SysCallKind → Bool) (t : Nat) (sched : List SysCall) : Nat

def operation_capacity_ok
    (cap : OperationCapacityModel) (sched : List SysCall) : Bool

def feedback_after_decode_ok (sched : List SysCall) : Bool

def all_invariants_strict_ok
    (arch : ZonedArch)
    (cap : OperationCapacityModel)
    (sched : List SysCall)
    (t_react_us window_us max_per_window : Nat) : Bool

def demo_arch : ZonedArch

def demo_t_react : Nat

def demo_window : Nat

def demo_max_per_window : Nat

def demo_operation_cap : OperationCapacityModel

def operation_capacity_good_schedule : List SysCall

theorem operation_capacity_good_ok :
    operation_capacity_ok demo_operation_cap
        operation_capacity_good_schedule = true

def operation_capacity_bad_parallel_gates : List SysCall

theorem operation_capacity_bad_parallel_gates_fails :
    operation_capacity_ok demo_operation_cap
        operation_capacity_bad_parallel_gates = false

theorem operation_capacity_bad_parallel_gates_old_bundle_passes :
    all_invariants_with_factory_ports_ok
        demo_arch operation_capacity_bad_parallel_gates
        demo_t_react demo_window demo_max_per_window = true

def feedback_after_decode_good_schedule : List SysCall

theorem feedback_after_decode_good_ok :
    feedback_after_decode_ok feedback_after_decode_good_schedule = true

theorem decoder_dependency_violator_now_rejected :
    feedback_after_decode_ok decoder_dependency_violator = false

def feedback_orphan_schedule : List SysCall

theorem feedback_orphan_rejected :
    feedback_after_decode_ok feedback_orphan_schedule = false

theorem strict_rejects_operation_capacity_bad :
    all_invariants_strict_ok demo_arch demo_operation_cap
        operation_capacity_bad_parallel_gates
        demo_t_react demo_window demo_max_per_window = false

theorem strict_rejects_decoder_dependency_violator :
    all_invariants_strict_ok demo_arch demo_operation_cap
        decoder_dependency_violator
        demo_t_react demo_window demo_max_per_window = false

theorem strict_accepts_surgery_ppm_A :
    all_invariants_strict_ok demo_arch demo_operation_cap
        (compileSurgeryGadgetToSysCalls surgery_ppm_A)
        demo_t_react demo_window demo_max_per_window = true

def high_parallel_operation_cap : OperationCapacityModel

theorem strict_still_accepts_routing_lane_violator :
    all_invariants_strict_ok demo_arch high_parallel_operation_cap
        routing_lane_violator
        demo_t_react demo_window demo_max_per_window = true

theorem strict_still_accepts_freshness_use_before_reset :
    all_invariants_strict_ok demo_arch demo_operation_cap
        freshness_use_before_reset
        demo_t_react demo_window demo_max_per_window = true

theorem strict_still_accepts_magic_no_startup_prefix :
    all_invariants_strict_ok demo_arch demo_operation_cap
        magic_no_startup_prefix
        demo_t_react demo_window 1 = true

structure ZoneCapacitySpec

structure SlotCapacityModel

def activeSitesAt (t : Nat) (sched : List SysCall) : List Nat

def activeSiteCountInZoneAt
    (z : ZoneCapacitySpec) (t : Nat) (sched : List SysCall) : Nat

def slot_capacity_ok
    (slotCap : SlotCapacityModel) (sched : List SysCall) : Bool

def slot_capacity_demo_arch : ZonedArch

def slot_capacity_demo_model : SlotCapacityModel

def slot_capacity_good_schedule : List SysCall

theorem slot_capacity_good_ok :
    slot_capacity_ok slot_capacity_demo_model
        slot_capacity_good_schedule = true

def slot_capacity_bad_three_active_sites : List SysCall

theorem slot_capacity_bad_three_active_sites_fails :
    slot_capacity_ok slot_capacity_demo_model
        slot_capacity_bad_three_active_sites = false

theorem slot_capacity_bad_old_capacity_passes :
    capacity_in_arch_ok slot_capacity_demo_arch
        slot_capacity_bad_three_active_sites = true

theorem slot_capacity_bad_capacity_per_cycle_passes :
    capacity_per_cycle_ok slot_capacity_demo_arch
        slot_capacity_bad_three_active_sites = true

theorem slot_capacity_bad_exclusivity_passes :
    exclusivity_ok slot_capacity_bad_three_active_sites = true

theorem slot_capacity_bad_operation_capacity_passes :
    operation_capacity_ok high_parallel_operation_cap
        slot_capacity_bad_three_active_sites = true

def all_invariants_strict_with_slot_capacity_ok
    (arch : ZonedArch)
    (opCap : OperationCapacityModel)
    (slotCap : SlotCapacityModel)
    (sched : List SysCall)
    (t_react_us window_us max_per_window : Nat) : Bool

theorem strict_with_slot_capacity_rejects_bad_three_active_sites :
    all_invariants_strict_with_slot_capacity_ok
        slot_capacity_demo_arch
        high_parallel_operation_cap
        slot_capacity_demo_model
        slot_capacity_bad_three_active_sites
        demo_t_react demo_window demo_max_per_window = false

theorem strict_without_slot_capacity_accepts_bad_three_active_sites :
    all_invariants_strict_ok
        slot_capacity_demo_arch
        high_parallel_operation_cap
        slot_capacity_bad_three_active_sites
        demo_t_react demo_window demo_max_per_window = true

def generous_slot_capacity_model : SlotCapacityModel

theorem strict_with_slot_capacity_accepts_surgery_ppm_A :
    all_invariants_strict_with_slot_capacity_ok
        surgery_arch demo_operation_cap generous_slot_capacity_model
        (compileSurgeryGadgetToSysCalls surgery_ppm_A)
        demo_t_react demo_window demo_max_per_window = true

inductive SiteLifecycle

structure AncillaZoneSpec

structure AncillaModel

def lifecycleOf
    (state : List (Nat × SiteLifecycle)) (site : Nat) : SiteLifecycle

def setLifecycle
    (state : List (Nat × SiteLifecycle))
    (site : Nat) (lc : SiteLifecycle) : List (Nat × SiteLifecycle)

def siteInAncillaModel (model : AncillaModel) (site : Nat) : Bool

def freshnessStep
    (model : AncillaModel)
    (state : List (Nat × SiteLifecycle)) (sc : SysCall) :
    Option (List (Nat × SiteLifecycle))

def runFreshness
    (model : AncillaModel) (state : List (Nat × SiteLifecycle)) :
    List SysCall → Option (List (Nat × SiteLifecycle))
  | []        => some state
  | sc :: rest =>
      match freshnessStep model state sc with
      | none         => none
      | some state'  => runFreshness model state' rest

def noDanglingLive (state : List (Nat × SiteLifecycle)) : Bool

def ancilla_freshness_ok
    (model : AncillaModel) (sched : List SysCall) : Bool

def demo_ancilla_model : AncillaModel

theorem freshness_use_before_reset_now_rejected :
    ancilla_freshness_ok demo_ancilla_model
        freshness_use_before_reset = false

theorem freshness_reuse_without_reset_now_rejected :
    ancilla_freshness_ok demo_ancilla_model
        freshness_reuse_without_reset = false

def freshness_reuse_after_measure : List SysCall

theorem freshness_reuse_after_measure_rejected :
    ancilla_freshness_ok demo_ancilla_model
        freshness_reuse_after_measure = false

def freshness_orphan_measure : List SysCall

theorem freshness_orphan_measure_rejected :
    ancilla_freshness_ok demo_ancilla_model
        freshness_orphan_measure = false

def freshness_one_slot_model : AncillaModel

def freshness_double_alloc : List SysCall

theorem freshness_double_alloc_rejected :
    ancilla_freshness_ok freshness_one_slot_model
        freshness_double_alloc = false

def freshness_good_short : List SysCall

theorem freshness_good_short_ok :
    ancilla_freshness_ok demo_ancilla_model
        freshness_good_short = true

theorem ancilla_freshness_accepts_surgery_ppm_A :
    ancilla_freshness_ok demo_ancilla_model
        (compileSurgeryGadgetToSysCalls surgery_ppm_A) = true

def all_invariants_strict_with_slot_capacity_and_freshness_ok
    (arch : ZonedArch)
    (opCap : OperationCapacityModel)
    (slotCap : SlotCapacityModel)
    (model : AncillaModel)
    (sched : List SysCall)
    (t_react_us window_us max_per_window : Nat) : Bool

theorem strict_with_freshness_rejects_use_before_reset :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        demo_arch demo_operation_cap generous_slot_capacity_model
        demo_ancilla_model freshness_use_before_reset
        demo_t_react demo_window demo_max_per_window = false

theorem strict_with_freshness_rejects_reuse_without_reset :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        demo_arch demo_operation_cap generous_slot_capacity_model
        demo_ancilla_model freshness_reuse_without_reset
        demo_t_react demo_window demo_max_per_window = false

theorem strict_with_freshness_rejects_reuse_after_measure :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        demo_arch demo_operation_cap generous_slot_capacity_model
        demo_ancilla_model freshness_reuse_after_measure
        demo_t_react demo_window demo_max_per_window = false

theorem strict_with_slot_capacity_accepts_freshness_use_before_reset :
    all_invariants_strict_with_slot_capacity_ok
        demo_arch demo_operation_cap generous_slot_capacity_model
        freshness_use_before_reset
        demo_t_react demo_window demo_max_per_window = true

theorem strict_with_slot_capacity_accepts_freshness_reuse_without_reset :
    all_invariants_strict_with_slot_capacity_ok
        demo_arch demo_operation_cap generous_slot_capacity_model
        freshness_reuse_without_reset
        demo_t_react demo_window demo_max_per_window = true

theorem strict_with_freshness_accepts_surgery_ppm_A :
    all_invariants_strict_with_slot_capacity_and_freshness_ok
        surgery_arch demo_operation_cap generous_slot_capacity_model
        demo_ancilla_model
        (compileSurgeryGadgetToSysCalls surgery_ppm_A)
        demo_t_react demo_window demo_max_per_window = true

def pipelinedReadyTime (i F : Nat) (spec : MagicStateSpec) (routingLatency : Nat) : Nat

def respectsReadiness (consumeBegin : Nat → Nat) (K F : Nat)
    (spec : MagicStateSpec) (lat : Nat) : Bool

def waitingSchedule (F : Nat) (spec : MagicStateSpec) (lat : Nat) : Nat → Nat

theorem waitingSchedule_respectsReadiness (K F : Nat) (spec : MagicStateSpec) (lat : Nat) :
    respectsReadiness (waitingSchedule F spec lat) K F spec lat = true

theorem premature_violates_readiness
    (consumeBegin : Nat → Nat) (K F : Nat) (spec : MagicStateSpec) (lat : Nat)
    (i : Nat) (hi : i < K) (hlt : consumeBegin i < pipelinedReadyTime i F spec lat) :
    respectsReadiness consumeBegin K F spec lat = false

def fullMagicGateSchedule (consumeBegin : Nat) : Schedule

def consumerMagicReady (sched : Schedule) (consumeBegin magicQubit : Nat) : Bool

theorem consume_too_early_not_ready :
    consumerMagicReady (fullMagicGateSchedule 5000) 5000 100 = false

theorem consume_after_wait_ready :
    consumerMagicReady (fullMagicGateSchedule 12015) 12015 100 = true

def circuitRuntimeUs (logicalDepthUs K F : Nat) (spec : MagicStateSpec) (lat : Nat) : Nat

theorem runtime_magic_limited
    (logicalDepthUs K F : Nat) (spec : MagicStateSpec) (lat : Nat)
    (h : logicalDepthUs ≤ deliveryLatency spec lat + magicSupplyTimeUs K F spec) :
    circuitRuntimeUs logicalDepthUs K F spec lat
      = deliveryLatency spec lat + magicSupplyTimeUs K F spec

def deviceQubits (dataQubits factoryQubits routingQubits : Nat) : Nat

def rsa2048_data_qubits  : Nat

def rsa2048_magic_budget : Nat

def rsa2048_factories    : Nat

def rsa2048_factory_qubits : Nat

theorem rsa2048_factories_value : rsa2048_factories = 1093

theorem rsa2048_factory_qubits_value : rsa2048_factory_qubits = 2803545

theorem windowed_rsa2048_device_schedule_ok (routingQubits logicalDepthUs : Nat)
    (h_magic_limited :
      logicalDepthUs ≤ deliveryLatency ccz_spec_qianxu 15
        + magicSupplyTimeUs rsa2048_magic_budget 1 ccz_spec_qianxu) :
    -- (1) waiting: no premature magic consumption
    respectsReadiness (waitingSchedule rsa2048_factories ccz_spec_qianxu 15)
        rsa2048_magic_budget rsa2048_factories ccz_spec_qianxu 15 = true
    -- (2) magic-limited runtime at one factory: the circuit waits on magic
    ∧ circuitRuntimeUs logicalDepthUs rsa2048_magic_budget 1 ccz_spec_qianxu 15
        = deliveryLatency ccz_spec_qianxu 15
          + magicSupplyTimeUs rsa2048_magic_budget 1 ccz_spec_qianxu
    -- (3) device qubit budget = data + factory + routing

def deliveryLatency (spec : MagicStateSpec) (routingLatency : Nat) : Nat

def magicDelivery (f cid magicQubit start : Nat) (spec : MagicStateSpec) (routingLatency : Nat) :
    Schedule

def magicReadyAt (delivery : Schedule) (t : Nat) : Bool

theorem magicReadyAt_magicDelivery
    (f cid mq start : Nat) (spec : MagicStateSpec) (lat t : Nat) :
    magicReadyAt (magicDelivery f cid mq start spec lat) t
      = decide (start + deliveryLatency spec lat ≤ t)

theorem earliest_consume_is_deliveryLatency
    (f cid mq : Nat) (spec : MagicStateSpec) (lat : Nat) :
    magicReadyAt (magicDelivery f cid mq 0 spec lat) (deliveryLatency spec lat) = true
    ∧ ∀ t, t < deliveryLatency spec lat →
        magicReadyAt (magicDelivery f cid mq 0 spec lat) t = false

def ccz_delivery_demo : Schedule

theorem ccz_not_ready_at_5000 : magicReadyAt ccz_delivery_demo 5000 = false

theorem ccz_not_ready_at_12014 : magicReadyAt ccz_delivery_demo 12014 = false

theorem ccz_ready_at_12015 : magicReadyAt ccz_delivery_demo 12015 = true

def factoryFootprint (n : Nat) (spec : MagicStateSpec) : Nat

def footprintFits (n cap : Nat) (spec : MagicStateSpec) : Bool

theorem ccz_footprint_one : factoryFootprint 1 ccz_spec_qianxu = 2565

theorem ccz_footprint_oversubscription :
    footprintFits 1 5000 ccz_spec_qianxu = true
    ∧ footprintFits 3 5000 ccz_spec_qianxu = false

def magicSupplyTimeUs (K F : Nat) (spec : MagicStateSpec) : Nat

def factoriesNeeded (K budgetUs : Nat) (spec : MagicStateSpec) : Nat

def factoryQubitShare (K budgetUs : Nat) (spec : MagicStateSpec) : Nat

theorem windowed_single_factory_is_magic_limited :
    8 * 3600000000 < magicSupplyTimeUs 2622824448 1 ccz_spec_qianxu

structure GateSpec

structure ZoneSpecH

structure DecoderSpec

structure TokenSpec

structure SyndromeSpec

structure HardwareSpec

def HardwareSpec.wellFormed (s : HardwareSpec) : Bool

def HardwareSpec.toZonedArch (s : HardwareSpec) : ZonedArch

def HardwareSpec.toOpCap (s : HardwareSpec) : OperationCapacityModel

def HardwareSpec.toSlotCap (s : HardwareSpec) : SlotCapacityModel

def HardwareSpec.toAncillaModel (s : HardwareSpec) : AncillaModel

abbrev GateTable

def HardwareSpec.toGateTable (s : HardwareSpec) : GateTable

def gate_support_ok (table : GateTable) (sched : List SysCall) : Bool

def HardwareSpec.magicInitialStock (s : HardwareSpec) : Nat

def checkScheduleOn (s : HardwareSpec) (sched : List SysCall) : Bool

private def jsonBool (b : Bool) : String

def ZoneSpecH.toJson (z : ZoneSpecH) : String

def GateSpec.toJson (g : GateSpec) : String

def TokenSpec.toJson (t : TokenSpec) : String

def HardwareSpec.toBackendJson (s : HardwareSpec) : String

def standardGates : List GateSpec

def adder_d3 : HardwareSpec

def adder_d3_dualRail : HardwareSpec

def adder_d3_zeroReaction : HardwareSpec

def adder_d3_tinyQueue : HardwareSpec

def adder_d3_magicStock : HardwareSpec

def adder_d3_magicScarce : HardwareSpec

def adder_d3_staleDecode : HardwareSpec

def adder_d3_strictDecoder : HardwareSpec

def ge2021_physical : HardwareSpec

def ge2021_logical : HardwareSpec

theorem ge2021_logical_fits_physical_budget :
    FormalRV.System.RSA2048.computationZoneQubits
      + FormalRV.System.RSA2048.factoriesNeeded
          * FormalRV.System.RSA2048.cczFactoryQubits
      ≤ FormalRV.System.RSA2048.physicalBudget

theorem ge2021_wellFormed :
    (ge2021_physical.wellFormed && ge2021_logical.wellFormed) = true

def surface_d3_stream : HardwareSpec

def invariant_demo : HardwareSpec

def ppm_pair : HardwareSpec

def ftDemo : HardwareSpec

theorem block_ok_on_adder_d3 :
    checkScheduleOn adder_d3 (compileSurgeryGadgetToSysCalls surgery_ppm_A)
      = true

theorem block_fails_on_zeroReaction :
    checkScheduleOn adder_d3_zeroReaction
      (compileSurgeryGadgetToSysCalls surgery_ppm_A) = false

theorem parallel_fails_on_adder_d3 :
    checkScheduleOn adder_d3 bad_parallel_adder_syscalls = false

theorem parallel_ok_on_dualRail :
    checkScheduleOn adder_d3_dualRail bad_parallel_adder_syscalls = true

def syndromeBurst (rounds cadence : Nat) : List SysCall

theorem syndrome_flood_rejected :
    checkScheduleOn surface_d3_stream (syndromeBurst 40 25) = false

theorem syndrome_paced_accepted :
    checkScheduleOn surface_d3_stream (syndromeBurst 25 40) = true

theorem syndrome_flood_ok_without_link_contract :
    checkScheduleOn { surface_d3_stream with syndrome

def decodesAt (times : List Nat) : List SysCall

theorem decoder_paced_reuse_accepted :
    checkScheduleOn adder_d3_strictDecoder
      (decodesAt [0, 0, 1000, 1000, 2000, 2000]) = true

theorem decoder_premature_reuse_rejected :
    checkScheduleOn adder_d3_strictDecoder
      (decodesAt [0, 0, 999]) = false

theorem decode_after_measure_accepted :
    checkScheduleOn adder_d3
      [ { kind

theorem decode_before_measure_rejected :
    checkScheduleOn adder_d3
      [ { kind

theorem second_magic_unprepared_rejected :
    checkScheduleOn adder_d3_magicScarce
      [ { kind

theorem second_magic_after_production_accepted :
    checkScheduleOn
      { adder_d3_magicScarce with
          magic_period_us

theorem second_magic_during_production_rejected :
    checkScheduleOn
      { adder_d3_magicScarce with
          magic_period_us

theorem adder_d3_arch_eq : adder_d3.toZonedArch = surgery_arch

theorem adder_d3_opCap_eq : adder_d3.toOpCap = adder_demo_opCap

theorem adder_d3_slotCap_eq :
    adder_d3.toSlotCap = generous_slot_capacity_model

theorem adder_d3_ancilla_eq :
    adder_d3.toAncillaModel = demo_ancilla_model

theorem invariant_demo_arch_eq :
    invariant_demo.toZonedArch
      = FormalRV.System.SystemInvariantExamples.demoArch

theorem ppm_pair_arch_eq :
    ppm_pair.toZonedArch
      = FormalRV.System.LatticeSurgeryPPMContract.ppm_pair_arch

theorem ftDemo_arch_eq_checker :
    ftDemo.toZonedArch = FormalRV.System.FTSchedule.demoArch

theorem ftDemo_arch_eq_framework :
    ftDemo.toZonedArch = FormalRV.System.InvariantFramework.demoArch

theorem catalog_wellFormed :
    (adder_d3.wellFormed && adder_d3_dualRail.wellFormed
      && adder_d3_zeroReaction.wellFormed && invariant_demo.wellFormed
      && ppm_pair.wellFormed && ftDemo.wellFormed) = true

structure MachineParams

def MachineParams.ofDevice (dev : Device) : MachineParams

def MachineParams.ofZonedArch (a : ZonedArch) : MachineParams

def MachineParams.ofHW (h : HW) : MachineParams

theorem reaction_device_eq (dev : Device) :
    (MachineParams.ofDevice dev).tReactUs = dev.reactionTime

theorem reaction_arch_eq (a : ZonedArch) :
    (MachineParams.ofZonedArch a).tReactUs = a.t_react_us

theorem reaction_hw_eq (h : HW) :
    (MachineParams.ofHW h).tReactUs = h.tReact

def ftReactionConsistent (f : FTSchedule) : Bool

theorem reaction_ft_eq (f : FTSchedule) (h : ftReactionConsistent f = true) :
    f.t_react_us = (MachineParams.ofZonedArch f.arch).tReactUs

def ge2021Device : Device

theorem ge2021_reaction_canonical :
    (MachineParams.ofHW ge2021).tReactUs = 10
    ∧ (MachineParams.ofDevice ge2021Device).tReactUs = 10

abbrev toffoliReported : Nat

abbrev magicBudget : Nat

abbrev patches : Nat

abbrev decodeLatencyCycles : Nat

abbrev decodeLanesRequired : Nat

abbrev cczFactoryQubits : Nat

abbrev cczWindowUs : Nat

abbrev factoriesNeeded : Nat

abbrev distance : Nat

abbrev tileQubits : Nat

abbrev physicalBudget : Nat

abbrev cycleUs : Nat

abbrev reactionUs : Nat

abbrev computationZoneQubits : Nat

abbrev syndromeBitsPerPatchRound : Nat

theorem decodeLanesRequired_value : decodeLanesRequired = 62_000

theorem computationZoneQubits_value : computationZoneQubits = 9_721_600

theorem syndromeBitsPerPatchRound_value :
    syndromeBitsPerPatchRound = 728

structure ZoneBudget

def ZoneBudget.total (b : ZoneBudget) : Nat

def layoutZones : List (String × Nat) → Nat → List ArchZone
  | [],               _   => []
  | (name, cnt) :: rest, off =>
      { name

def ZoneBudget.toArch (b : ZoneBudget) : ZonedArch

theorem toArch_total (b : ZoneBudget) : b.toArch.total_sites = b.total

theorem layout_zone_capacity (name : String) (cnt : Nat) (rest : List (String × Nat)) (off : Nat) :
    ((layoutZones ((name, cnt) :: rest) off).head?.map ArchZone.capacity) = some cnt

def qianxuBudget (N_m N_p N_res tCycle vMax : Nat) : ZoneBudget

theorem qianxu_total (N_m N_p N_res tCycle vMax : Nat) :
    (qianxuBudget N_m N_p N_res tCycle vMax).total = N_m + N_p + 2565 + 894 + N_res

theorem qianxu_10k_instance :
    (qianxuBudget 4000 2541 0 1 1).total = 10_000

theorem qianxu_10k_arch_total :
    (qianxuBudget 4000 2541 0 1 1).toArch.total_sites = 10_000