; GraphAtlas proof RS-08
; Statement: The expected real rate is rounded to a whole number of five basis points, upwards when it is below the rounded rate of the year before and downwards otherwise. The rounded rate is less than five basis points from the unrounded one, a rate that is already a whole number of five basis points stays as it is, and a higher unrounded rate never gives a lower rounded one.
; About: roundRealRate in src/kernel/curve.ts. A rate is a whole number of millionths, so five basis points is 500 of them. The rate of the year before is itself a whole number of five basis points. Rounding up gives the least multiple of five basis points that is not below the rate, and rounding down gives the greatest that is not above it.
; Source: EIOPA-BoS-26-198, technical documentation of May 2026, Annex C, paragraph C.3.6
; Expected: unsat for each of the 6 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun unrounded_real_rate () Int)
(declare-fun a_higher_unrounded_real_rate () Int)
(declare-fun previous_rounded_rate () Int)
(declare-fun steps_up () Int)
(declare-fun steps_down () Int)
(declare-fun steps_up_of_the_higher () Int)
(declare-fun steps_down_of_the_higher () Int)
(assert (>= a_higher_unrounded_real_rate unrounded_real_rate))
(assert (= (mod previous_rounded_rate 500) 0))
(assert (<= unrounded_real_rate (* steps_up 500)))
(assert (> unrounded_real_rate (* (- steps_up 1) 500)))
(assert (>= unrounded_real_rate (* steps_down 500)))
(assert (< unrounded_real_rate (* (+ steps_down 1) 500)))
(assert (<= a_higher_unrounded_real_rate (* steps_up_of_the_higher 500)))
(assert (> a_higher_unrounded_real_rate (* (- steps_up_of_the_higher 1) 500)))
(assert (>= a_higher_unrounded_real_rate (* steps_down_of_the_higher 500)))
(assert (< a_higher_unrounded_real_rate (* (+ steps_down_of_the_higher 1) 500)))

; Goal 1, negated
(push 1)
(assert (not (= (mod (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)) 500) 0)))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (- (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)) unrounded_real_rate))) (< (ite (>= a!1 0) a!1 (- a!1)) 500))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (=> (< unrounded_real_rate previous_rounded_rate) (>= (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)) unrounded_real_rate))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (=> (>= unrounded_real_rate previous_rounded_rate) (<= (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)) unrounded_real_rate))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (=> (= (mod unrounded_real_rate 500) 0) (= (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)) unrounded_real_rate))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (>= (ite (< a_higher_unrounded_real_rate previous_rounded_rate) (* steps_up_of_the_higher 500) (* steps_down_of_the_higher 500)) (ite (< unrounded_real_rate previous_rounded_rate) (* steps_up 500) (* steps_down 500)))))
(check-sat)
(pop 1)