def below_go

bend-collections-laws-crypto@1.0.0.0 · spec/math/random/rand.bend:92

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/src/math/u64.bend as W
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/source.bend as SRC

92# the bounded draw once a draw of x (with verdict m) has left state s: m if
93# accepted, else (while fuel lasts) the next draw; with no fuel left, the
94# last candidate floor(x n / 2^64). The verdict is matched before the
95# recursion, so a draw that is not yet decided keeps the rest unexpanded.
96def below_go(~S: Data, ~next: S -> W.U64 & S, fuel: Nat, +n: Nat, m: Maybe<&2, Nat>, +x: Nat, +s: S) -> Nat & S:
97  match fuel m:
98    case 0n Some{k}:
99      (k, s)
100    case 0n None{}:
101      (C.high(64n, Nat.mul(x, n)), s)
102    case 1n+f Some{k}:
103      (k, s)
104    case 1n+f None{}:
105      below_go(~S, ~next, f, n, draw(64n, SW.value(SRC.fst64(S, next(s))), n), SW.value(SRC.fst64(S, next(s))), SRC.snd64(S, next(s)))