def value_vn

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/uint64n.bend:321

import Base
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/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/spec/math/random.bend as SRM

321def value_vn(~S: Data, ~next: S -> WU.U64 & S, +s: S, +n: WU.U64, +vn: Nat, +hv: {SW.value(n) == vn : Nat}) -> {SRM.val_pair(S, R.uint64n(~S, ~next, s, n)) == SR.below(~S, ~next, 127n, SW.value(n), s) : Nat & S}:
322  match vn:
323    case 0n:
324      +hz = Equal.trans(Bool, X.is_zero(n), Nat.is_eq(SW.value(n), 0n), True{}, WA.is_zero_value(n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(n), 0n, hv))
325      %Equal.sym(WU.U64, n, Z(), zero_word(n, hz)) : {SRM.val_pair(S, R.uint64n(~S, ~next, s, _)) == SR.below(~S, ~next, 127n, SW.value(_), s) : Nat & S}
326      zero_pair(S, next(s))
327    case 1n+m:
328      +hz = Equal.trans(Bool, X.is_zero(n), Nat.is_eq(SW.value(n), 0n), False{}, WA.is_zero_value(n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(n), 1n+m, hv))
329      %Equal.sym(Bool, R.is_pow2(n), Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), pow2_value(n, m, hv)) : {SRM.val_pair(S, R.uint64n_pick(~S, ~next, s, n, _)) == SR.below(~S, ~next, 127n, SW.value(n), s) : Nat & S}
330      %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {SRM.val_pair(S, R.uint64n_pick(~S, ~next, s, n, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n))) == SR.below(~S, ~next, 127n, _, s) : Nat & S}
331      value_nz(~S, ~next, 1n, {==}, s, n, m, hv, hz, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), {==})