law nv

lawful-fields@0.1.1.0 · proof_num.bend:492

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B
import lawful-fields@0.1.1.0/defs.bend as F
import lawful-fields@0.1.1.0/fields.bend as C
import lawful-bytes@0.1.1.0/proof_core.bend as K
import lawful-arrays@0.1.0.0/proof_tree.bend as P

492law nv:
493  for +n: Nat
494  for +len: U32
495  for +t: P.Tree<U32>
496  for +d: Nat
497  for +j: U32
498  for +ok: Bool
499  for +acc: U32
500  for +m: Maybe<&2, Nat>
501  for +M: Nat
502  for +q: Nat
503  for +hm: {Nat.pow(2n, 32n) == M : Nat}
504  for +hcq: {U32.to_nat(429496729) == q : Nat}
505  for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
506  for +h: {D.ok(K.BT(len, t), d) == True{} : Bool}
507  for +hjn: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool}
508  for +hi: Inv(ok, acc, m, M)
509  {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num.go(n, B.at(K.BT(len, t), j), j, acc, ok))) == F.decb.of(F.dec.go(D.slice(D.view(K.BT(len, t)), U32.to_nat(j), n), m), M) : Maybe<&2, Nat>}