; GraphAtlas proof PQ-01
; Statement: When only the quantum computer sets the date, the latest start is the years until it arrives less the years to keep the data secure and the years to migrate. Nothing later keeps the data safe, and the use is late exactly when those two add up to more than the years until it arrives.
; About: plan in src/kernel/pqc.ts for a use with no government date and nothing waiting for it, where the latest start is Z - X - Y and the exposure flag is X + Y > Z. X, Y and Z are whole numbers of years: X from 0 to 100, Y from 1 to 30 and Z from 1 to 100, the limits the function enforces. "Safe" means that the migration is over at least X years before the quantum computer arrives.
; Source: NIST IR 8547, Section 3
; Expected: unsat for each of the 3 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun years_to_keep () Int)
(declare-fun years_to_migrate () Int)
(declare-fun years_to_quantum () Int)
(declare-fun other_start () Int)
(assert (>= years_to_keep 0))
(assert (<= years_to_keep 100))
(assert (>= years_to_migrate 1))
(assert (<= years_to_migrate 30))
(assert (>= years_to_quantum 1))
(assert (<= years_to_quantum 100))

; Goal 1, negated
(push 1)
(assert (not (<= (+ (- (- years_to_quantum years_to_keep) years_to_migrate) years_to_migrate years_to_keep) years_to_quantum)))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (=> (<= (+ other_start years_to_migrate years_to_keep) years_to_quantum) (<= other_start (- (- years_to_quantum years_to_keep) years_to_migrate)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (= (> (+ years_to_keep years_to_migrate) years_to_quantum) (< (- (- years_to_quantum years_to_keep) years_to_migrate) 0))))
(check-sat)
(pop 1)