def conv_len_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:306

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

306# len(conv(xs, ys)) <= j + k when len(xs) <= j and len(ys) <= k
307def conv_len_le(+j: Nat, +k: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ex: {len_le(j, xs) == True{} : Bool}, +ey: {len_le(k, ys) == True{} : Bool}) -> {len_le(Nat.add(j, k), F.conv(xs, ys)) == True{} : Bool}:
308  match j xs:
309    case 0n Nil{}:
310      len_le_nil(k)
311    case 0n Con{x, xt}:
312      Empty.absurd({len_le(k, F.conv(Con{x, xt}, ys)) == True{} : Bool}, L.false_true(ex))
313    case 1n+m Nil{}:
314      {==}
315    case 1n+ +m Con{+x, +xt}:
316      +hs0 = len_le_mono(k, 1n+m, F.scal(x, ys), scal_len_le(k, x, ys, ey))
317      +hs = L.subst(Nat, z => {len_le(z, F.scal(x, ys)) == True{} : Bool}, Nat.add(k, 1n+m), Nat.add(1n+m, k), NA.add_comm(k, 1n+m), hs0)
318      +hz = conv_len_le(m, k, xt, ys, ex, ey)
319      addl_len_le(Nat.add(1n+m, k), F.scal(x, ys), Con{0, F.conv(xt, ys)}, hs, hz)