def take_okb

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

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

62def take_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(n, F.take(n, xs), b) == True{} : Bool}:
63  match n:
64    case 0n:
65      {==}
66    case 1n+ +k:
67      match xs:
68        case Nil{}:
69          e
70        case Con{+x, +xt}:
71          L.and_intro(Nat.is_le(v(x), b), LM.okb(k, F.take(k, xt), b), L.and_left(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e), take_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e)))