def at_view.go

lawful-bytes@0.1.1.0 · PROOF.bend:27

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/proof_core.bend as C

27def at_view.go(-b: D.Bytes, +d: Nat, +i: U32, h: {D.ok(b, d) == True{} : Bool},
28  hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}, m: C.BMirror(b)) ->
29  {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}:
30  (+len, m2) = m
31  (+t, +e) = m2
32  %e : {Some{Pair.snd(D.Bytes, U32, B.at(_, i))} == List.get(&2, U32, D.view(_), U32.to_nat(i)) : Maybe<&2, U32>}
33  +h2 = C.tr(x => {D.ok(x, d) == True{} : Bool}, b, len, t, e, h)
34  C.at_view_t(len, t, d, i, C.ok_full(len, t, d, h2), C.ok_d(len, t, d, h2), C.ok_len(len, t, d, h2),
35    C.tr(x => {Nat.is_lt(U32.to_nat(i), D.size(x)) == True{} : Bool}, b, len, t, e, hi))