def kex_shared

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/proof.bend:203

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/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/kex.bend as SK
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kex.bend as K

203def kex_shared(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +pk: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}, +hp: {FS.tight(pk) == True{} : Bool}) -> SK.Kex.shared(one, h1, sk, pk, hs, hp):
204  e = x25519_checked(one, h1, sk, pk)
205  %Equal.sym(Maybe<&2, List<&2, U32>>, X.x25519(sk, pk), Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(sk), FS.tight(pk)), Some{S.x25519(one, sk, pk)}, None{}), e) : {K.shared_of(_) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
206  %Equal.sym(Bool, FS.tight(sk), True{}, hs) : {K.shared_of(Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(_, FS.tight(pk)), Some{S.x25519(one, sk, pk)}, None{})) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
207  %Equal.sym(Bool, FS.tight(pk), True{}, hp) : {K.shared_of(Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(True{}, _), Some{S.x25519(one, sk, pk)}, None{})) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
208  shared_by(one, h1, S.x25519(one, sk, pk), spec_tight(one, sk, pk))