law fast_find2_t

lawful-bytes@0.1.1.0 · proof_fast_find2.bend:677

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-bytes@0.1.1.0/fast.bend as FA
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P

677law fast_find2_t:
678  for +len: U32
679  for +t: P.Tree<U32>
680  for +d: Nat
681  for +from: U32
682  for +to: U32
683  for +c1: U32
684  for +c2: U32
685  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
686  for +hft: {U32.is_le(from, to) == True{} : Bool}
687  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
688  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
689  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
690  {FA.find2(C.BT(len, t), from, to, c1, c2) == B.find2(C.BT(len, t), from, to, c1, c2) : D.Bytes & U32}