law fview_go

lawful-bytes@0.1.1.0 · proof_fast_find.bend:1003

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
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

1003# The answer as a number, split on to <= from (no words: the answer is to = from).
1004law fview_go:
1005  for +b: Bool
1006  for +len: U32
1007  for +t: P.Tree<U32>
1008  for +d: Nat
1009  for +from: U32
1010  for +to: U32
1011  for +c: U32
1012  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
1013  for +hft: {U32.is_le(from, to) == True{} : Bool}
1014  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
1015  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
1016  for +hb: {U32.is_le(to, from) == b : Bool}
1017  {U32.to_nat(U32.min(FG(Bool.pick(Nat, b, 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32))), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}