; GraphAtlas proof SM-03
; Statement: In a bucket, the parts that rest on the factors add up to K^2 + S x C, where K^2 is the quantity under the root of the bucket margin, S is the clipped sum of the weighted sensitivities and C is what the other buckets put in the cross term. It holds when the sum is inside the clip, above it or below it, or when K is zero, and for any number of factors, because each step of the sum keeps the invariant.
; About: evaluate and evaluateBucket in src/kernel/simm.ts. The part of the margin that rests on a factor is ws x (u + C x d) times a factor that is the same for the whole bucket, where d is 1 inside the clip, plus or minus u over K outside it, and 0 when K is zero. The proof states the invariant of the loop over the factors for each case, with A the sum of ws x u so far and B the sum of ws, and the solver checks that one more factor keeps it. When the loop ends A is K^2, because K is the root of it, and B decides the case. No table is in the proof, because u can be anything, which is what the positive definite correlation matrix is certified for separately.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraphs 7(c) and 8(c)
; Expected: unsat for each of the 8 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun weighted_sensitivity () Real)
(declare-fun weights_so_far () Real)
(declare-fun cross () Real)
(declare-fun weighted_row () Real)
(declare-fun products_so_far () Real)
(declare-fun shares_so_far () Real)
(declare-fun k () Real)
(declare-fun k_inverse () Real)

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (and (>= k 0.0) (= shares_so_far (+ products_so_far (* cross weights_so_far))))) (a!2 (+ shares_so_far (* weighted_sensitivity (+ weighted_row (* cross 1.0)))))) (let ((a!3 (= a!2 (+ products_so_far (* weighted_sensitivity weighted_row) (* cross (+ weights_so_far weighted_sensitivity)))))) (=> a!1 a!3)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (and (> k 0.0) (= (* k k_inverse) (to_real 1)) (= shares_so_far (+ products_so_far (* cross products_so_far k_inverse))))) (a!2 (+ shares_so_far (* weighted_sensitivity (+ weighted_row (* cross weighted_row k_inverse))))) (a!3 (+ (+ products_so_far (* weighted_sensitivity weighted_row)) (* cross (+ products_so_far (* weighted_sensitivity weighted_row)) k_inverse)))) (=> a!1 (= a!2 a!3)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (and (> k 0.0) (= (* k k_inverse) (to_real 1)) (= shares_so_far (- products_so_far (* cross products_so_far k_inverse))))) (a!2 (+ weighted_row (* cross (- (* weighted_row k_inverse))))) (a!3 (- (+ products_so_far (* weighted_sensitivity weighted_row)) (* cross (+ products_so_far (* weighted_sensitivity weighted_row)) k_inverse)))) (=> a!1 (= (+ shares_so_far (* weighted_sensitivity a!2)) a!3)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (+ shares_so_far (* weighted_sensitivity (+ weighted_row (* cross 0.0)))))) (=> (and (= k (to_real 0)) (= shares_so_far products_so_far)) (= a!1 (+ products_so_far (* weighted_sensitivity weighted_row)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (and (>= k 0.0) (>= weights_so_far (- k)) (<= weights_so_far k) (= products_so_far (* k k)) (= shares_so_far (+ products_so_far (* cross weights_so_far)))))) (=> a!1 (= shares_so_far (+ (* k k) (* cross weights_so_far)))))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (and (> k 0.0) (= (* k k_inverse) (to_real 1)) (> weights_so_far k) (= products_so_far (* k k)) (= shares_so_far (+ products_so_far (* cross products_so_far k_inverse)))))) (=> a!1 (= shares_so_far (+ (* k k) (* cross k)))))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (and (> k 0.0) (= (* k k_inverse) (to_real 1)) (< weights_so_far (- k)) (= products_so_far (* k k)) (= shares_so_far (- products_so_far (* cross products_so_far k_inverse))))) (a!2 (= shares_so_far (+ (* k k) (* cross (- k)))))) (=> a!1 a!2))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (=> (and (= k (to_real 0)) (= products_so_far (* k k)) (= shares_so_far products_so_far)) (= shares_so_far (+ (* k k) (* cross 0.0))))))
(check-sat)
(pop 1)