Uint64n.value_vn: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 321-331 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&start_line=321&end_line=331

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

def 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}:
  match vn:
    case 0n:
      +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))
      %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}
      zero_pair(S, next(s))
    case 1n+m:
      +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))
      %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}
      %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}
      value_nz(~S, ~next, 1n, {==}, s, n, m, hv, hz, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), {==})

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=Z
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=pow2_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=value_nz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=zero_pair
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=zero_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=is_zero_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend&name=and_bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend&name=below
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random.bend&name=val_pair
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend&name=is_pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend&name=uint64n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend&name=uint64n_pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=is_zero