; GraphAtlas proof SM-06
; Statement: The clipped sum of a bucket is never beyond K and has the sign of the sum. It is the sum inside the clip and K with the sign of the sum outside it. It rises with the sum, and a book with every sign changed has the clipped sum with its sign changed, so that the margin does not depend on which side of the market the book is on.
; About: evaluateBucket in src/kernel/simm.ts, where S is the larger of minus K and the smaller of the sum of the weighted sensitivities and K. The quantity under the root is the same for a book and for its mirror image, because each K^2 is a form of the weighted sensitivities, which does not change with their sign, and each product of two clipped sums does not either, so the margin of a book and of its mirror image are the same.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraphs 7(c) and 8(c)
; Expected: unsat for each of the 7 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun k () Real)
(declare-fun sum () Real)
(declare-fun other_sum () Real)

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (=> (>= k 0.0) (and (>= a!1 (- k)) (<= a!1 k))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (=> (>= k 0.0) (>= (* a!1 sum) 0.0)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (=> (and (>= k 0.0) (>= sum (- k)) (<= sum k)) (= a!1 sum)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (=> (and (>= k 0.0) (> sum k)) (= a!1 k)))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (=> (and (>= k 0.0) (< sum (- k))) (= a!1 (- k))))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k))) (a!2 (ite (>= (- k) (ite (<= other_sum k) other_sum k)) (- k) (ite (<= other_sum k) other_sum k)))) (=> (and (>= k 0.0) (<= sum other_sum)) (<= a!1 a!2)))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (>= (- k) (ite (<= (- sum) k) (- sum) k))) (a!3 (ite (>= (- k) (ite (<= sum k) sum k)) (- k) (ite (<= sum k) sum k)))) (let ((a!2 (ite a!1 (- k) (ite (<= (- sum) k) (- sum) k)))) (=> (>= k 0.0) (= a!2 (- a!3)))))))
(check-sat)
(pop 1)