def scal_okb

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

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/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

216def scal_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.okb(n, ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.okb(n, F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:
217  match n ys:
218    case 0n Nil{}:
219      {==}
220    case 0n Con{y, yt}:
221      Empty.absurd({LM.okb(0n, F.scal(x, Con{y, yt}), Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))
222    case 1n+m Nil{}:
223      Empty.absurd({LM.okb(1n+m, Nil{}, Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))
224    case 1n+ +m Con{+y, +yt}:
225      +hyh = LM.okb_head(m, y, yt, b, hy)
226      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)
227      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))
228      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.okb(m, F.scal(x, yt), Nat.mul(a, b)), hd, scal_okb(one, h1, m, x, yt, a, b, hx, LM.okb_tail(m, y, yt, b, hy), hab))