; GraphAtlas proof PQ-02
; Statement: A use is at least medium risk under the EU roadmap exactly when it protects confidentiality or takes more than eight years to migrate. It is high risk exactly when it has a high impact and either protects confidentiality for ten years or more or takes more than eight years to migrate.
; About: euRisk in src/kernel/pqc.ts, built from the thresholds in RULES.eu. The statement uses the numbers of the roadmap, 10 and 8, written out in the goals and not read from the code, so a change to the thresholds in the code fails this proof. The years to keep a use secure run from 0 to 100 and the years to migrate from 1 to 30, the limits the plan enforces. Confidentiality is the purpose of key establishment and of encryption.
; Source: EU coordinated implementation roadmap for post-quantum cryptography, version 1.1, Section 5
; 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 confidential () Bool)
(declare-fun high_impact () Bool)
(assert (>= years_to_keep 0))
(assert (<= years_to_keep 100))
(assert (>= years_to_migrate 1))
(assert (<= years_to_migrate 30))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (>= (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!2 (ite a!1 (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!3 (ite (and confidential (>= years_to_keep 10) high_impact) a!2 (ite confidential (ite (>= 1 2) 1 2) 1)))) (let ((a!4 (ite (> years_to_migrate 8) (ite (>= a!3 2) a!3 2) a!3))) (let ((a!5 (ite (and (> years_to_migrate 8) high_impact) (ite (>= a!4 3) a!4 3) a!4))) (and (>= a!5 1) (<= a!5 3)))))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (>= (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!2 (ite a!1 (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!3 (ite (and confidential (>= years_to_keep 10) high_impact) a!2 (ite confidential (ite (>= 1 2) 1 2) 1)))) (let ((a!4 (ite (> years_to_migrate 8) (ite (>= a!3 2) a!3 2) a!3))) (let ((a!5 (>= (ite (and (> years_to_migrate 8) high_impact) (ite (>= a!4 3) a!4 3) a!4) 2))) (= a!5 (or confidential (> years_to_migrate 8))))))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (>= (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!2 (ite a!1 (ite confidential (ite (>= 1 2) 1 2) 1) 3))) (let ((a!3 (ite (and confidential (>= years_to_keep 10) high_impact) a!2 (ite confidential (ite (>= 1 2) 1 2) 1)))) (let ((a!4 (ite (> years_to_migrate 8) (ite (>= a!3 2) a!3 2) a!3))) (let ((a!5 (= (ite (and (> years_to_migrate 8) high_impact) (ite (>= a!4 3) a!4 3) a!4) 3))) (= a!5 (or (and confidential (>= years_to_keep 10) high_impact) (and (> years_to_migrate 8) high_impact))))))))))
(check-sat)
(pop 1)