def conv_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/mulw.bend:71

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/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL

71def conv_ge(+m: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +b: Nat, +hx: {LM.okb(1n+m, xs, b) == True{} : Bool}, +hy: {PL.len_ge(n, ys) == True{} : Bool}) -> {PL.len_ge(n, F.conv(xs, ys)) == True{} : Bool}:
72  match xs:
73    case Nil{}:
74      Empty.absurd({PL.len_ge(n, Nil{}) == True{} : Bool}, L.false_true(hx))
75    case Con{+x, +xt}:
76      PL.conv_len_ge(n, x, xt, ys, hy)