law av

lawful-bytes@0.1.1.0 · proof_fast_append.bend:897

import Base
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/defs.bend as A
import lawful-arrays@0.1.0.0/proof_tree.bend as P

897# After the words written so far (o bytes, o <= np), the bytes in use agree
898# with v1 then src from qn; the k words left finish the np bytes.
899law av:
900  for +k: Nat
901  for +b: Bool
902  for +ts: P.Tree<U32>
903  for +e: Nat
904  for +td: P.Tree<U32>
905  for +d: Nat
906  for +p: U32
907  for +lo: U32
908  for +si: U32
909  for +di: U32
910  for +sh: Nat
911  for +l1: Nat
912  for +qn: Nat
913  for +r: Nat
914  for +o: Nat
915  for +np: Nat
916  for +v1: List<&2, U32>
917  for +hbq: {Nat.is_le(Nat.add(o, 4n), np) == b : Bool}
918  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
919  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
920  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
921  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
922  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
923  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
924  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
925  for +hlo: {lo == C.WD(ts, si) : U32}
926  for +hsh: {sh == Nat.mul(8n, r) : Nat}
927  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
928  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
929  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
930  for +hon: {Nat.is_le(o, np) == True{} : Bool}
931  for +hc1: {Nat.is_le(np, Nat.add(o, Nat.mul(k, 4n))) == True{} : Bool}
932  for +hc2: {Nat.is_lt(Nat.add(o, Nat.mul(k, 4n)), Nat.add(np, 4n)) == True{} : Bool}
933  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
934  {List.take(&2, U32, US(AWT(k, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>}