; GraphAtlas proof EN-01
; Statement: The repetition count cutoff is the smallest integer C for which H times (C - 1) reaches the false positive exponent.
; About: rctCutoff in src/kernel/entropy.ts, which computes 1 + ceil(a / H) exactly for the binary value of H, for every H in (0, 64] and every integer exponent a from 1 to 64. SP 800-90B chooses the rule so that a run of C equal samples from a source with min-entropy H has probability at most 1/2^a. The proof is about the integer rule, not about that probability argument.
; Source: NIST SP 800-90B, Section 4.4.1
; Expected: unsat for each of the 2 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun alpha_exponent () Int)
(declare-fun min_entropy () Real)
(declare-fun other_candidate () Int)
(assert (>= alpha_exponent 1))
(assert (<= alpha_exponent 64))
(assert (> min_entropy 0.0))
(assert (<= min_entropy 64.0))
(assert (>= other_candidate 0))

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

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