def eq_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/eqf.bend:82

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
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/nat.bend as N
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/math/natural/arith.bend as NR
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/fieldops.bend as FO
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as CN
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

82def eq_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {F.eq(a, b) == Nat.is_eq(Nat.mod(FS.value(a), 1n+pp), Nat.mod(FS.value(b), 1n+pp)) : Bool}:
83  +P = {1n+pp : Nat}
84  +A = Nat.mod(FS.value(a), P)
85  +B = Nat.mod(FS.value(b), P)
86  +d = F.sub(a, b)
87  +e1 = CN.is_zero_val(one, h1, pp, hP, d, FO.sub_okb(one, h1, a, b, ha, hb))
88  +e2 = FO.sub_mod(one, h1, pp, hP, a, b, ha, hb)
89  +e3 = G.c_subm(pp, FS.value(a), A, B, G.c_sym(pp, A, FS.value(a), G.c_mod(pp, FS.value(a))), N.lt_le(B, P, NR.dm_lt(pp, FS.value(b))))
90  +e4 = Equal.trans(Nat, Nat.mod(FS.value(d), P), Nat.mod(Nat.sub(Nat.add(FS.value(a), P), B), P), Nat.mod(pw(pp, A, B), P), e2, e3)
91  +e5 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), Nat.mod(FS.value(d), P), Nat.mod(pw(pp, A, B), P), e4)
92  Equal.trans(Bool, F.eq(a, b), Nat.is_eq(Nat.mod(FS.value(d), P), 0n), Nat.is_eq(A, B), e1, Equal.trans(Bool, Nat.is_eq(Nat.mod(FS.value(d), P), 0n), Nat.is_eq(Nat.mod(pw(pp, A, B), P), 0n), Nat.is_eq(A, B), e5, eq_bool(pp, A, B, NR.dm_lt(pp, FS.value(a)), NR.dm_lt(pp, FS.value(b)), Nat.is_eq(A, B), {==})))