; GraphAtlas proof EN-02
; Statement: The repetition count cutoff never rises when the claimed min-entropy rises.
; About: rctCutoff in src/kernel/entropy.ts, for every pair of claims 0 < H1 <= H2 <= 64.
; Source: NIST SP 800-90B, Section 4.4.1
; Expected: unsat for each of the 1 check below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun alpha_exponent () Int)
(declare-fun entropy_low () Real)
(declare-fun entropy_high () Real)
(assert (>= alpha_exponent 1))
(assert (<= alpha_exponent 64))
(assert (> entropy_low 0.0))
(assert (<= entropy_low entropy_high))
(assert (<= entropy_high 64.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (to_int (- (/ (to_real alpha_exponent) entropy_low)))) (a!2 (to_int (- (/ (to_real alpha_exponent) entropy_high))))) (>= (- a!1) (- a!2)))))
(check-sat)
(pop 1)