def fast_append_ok.go

lawful-bytes@0.1.1.0 · PROOF.bend:525

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-bytes@0.1.1.0/proof_fast_append.bend as FX

525def fast_append_ok.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
526  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}:
527  (+l_dst, m2_dst) = m_dst
528  (+t_dst, +e_dst) = m2_dst
529  (+l_src, m2_src) = m_src
530  (+t_src, +e_src) = m2_src
531  %e_dst : {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(_, src, s, n)), d) == True{} : Bool}
532  %e_src : {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(l_dst, t_dst), _, s, n)), d) == True{} : Bool}
533  +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
534  +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
535  FX.fast_append_ok_t(l_dst, t_dst, l_src, t_src, d, s, n, hd_t, hc_t)