def le_app

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:57

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

57def le_app(xs: List<&2, U32>, +ys: List<&2, U32>) -> {le_val(List.append(&2, U32, xs, ys)) == Nat.add(le_val(xs), pw8(List.length(&2, U32, xs), le_val(ys))) : Nat}:
58  match xs:
59    case Nil{}:
60      {==}
61    case +x <> +t:
62      %Equal.sym(Nat, le_val(List.append(&2, U32, t, ys)), Nat.add(le_val(t), pw8(List.length(&2, U32, t), le_val(ys))), le_app(t, ys)) : {Nat.add(B.byte(x), C.shift(8n, _)) == Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))) : Nat}
63      %Equal.sym(Nat, C.shift(8n, Nat.add(le_val(t), pw8(List.length(&2, U32, t), le_val(ys)))), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))), WW.shift_add(8n, le_val(t), pw8(List.length(&2, U32, t), le_val(ys)))) : {Nat.add(B.byte(x), _) == Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))) : Nat}
64      %Equal.sym(Nat, Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))), Nat.add(B.byte(x), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))), NA.add_assoc(B.byte(x), C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))) : {Nat.add(B.byte(x), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))) == _ : Nat}
65      {==}