def drop_okb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/bytes.bend:73

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

73def drop_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(m, F.drop(n, xs), b) == True{} : Bool}:
74  match n:
75    case 0n:
76      e
77    case 1n+ +k:
78      match xs:
79        case Nil{}:
80          Empty.absurd({LM.okb(m, Nil{}, b) == True{} : Bool}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
81        case Con{+x, +xt}:
82          drop_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e))