def go_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:113

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as M128

113# the bounded draw after a draw of x is below n > 0
114def go_lt(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: Nat, m: Maybe<&2, Nat>, +x: Nat, +s1: S, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hm: {SR.draw(64n, x, n) == m : Maybe<&2, Nat>}) -> {Nat.is_lt(pfst(S, SR.below_go(~S, ~next, f, n, m, x, s1)), n) == True{} : Bool}:
115  match f m:
116    case 0n Some{k}:
117      draw_lt(x, n, k, hx, hn, hm)
118    case 0n None{}:
119      high_lt(x, n, hx, hn)
120    case 1n+g Some{k}:
121      draw_lt(x, n, k, hx, hn, hm)
122    case 1n+g None{}:
123      go_lt(~S, ~next, g, n, SR.draw(64n, SW.value(SRC.fst64(S, next(s1))), n), SW.value(SRC.fst64(S, next(s1))), SRC.snd64(S, next(s1)), M128.fit64(SRC.fst64(S, next(s1))), hn, {==})