LAWS.kex_agree_if: law of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
Lines 301-321 of bend-osdev-crypto@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&start_line=301&end_line=321

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-crypto@0.1.0.0/kex.bend as Kx

# two parties agree from each other's public-key bytes, for every scheme and
# pair of secret keys, when the keys parse (hx, hy), the public keys survive
# their bytes (hfx, hfy) and the scheme's agree law holds for them (h)
law kex_agree_if:
  for ~SK: Data
  for ~PK: Data
  for ~secret: B.Octets -> Result<&2, &2, Cr.CrError, SK>
  for ~public: SK -> PK
  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
  for ~pk_to: PK -> B.Octets
  for ~shared: SK -> PK -> Result<&2, &2, Cr.CrError, B.Octets>
  for +a: B.Octets
  for +b: B.Octets
  for +x: SK
  for +y: SK
  for hx: {secret(a) == Done{x} : Result<&2, &2, Cr.CrError, SK>}
  for hy: {secret(b) == Done{y} : Result<&2, &2, Cr.CrError, SK>}
  for hfx: {pk_of(pk_to(public(x))) == Done{public(x)} : Result<&2, &2, Cr.CrError, PK>}
  for hfy: {pk_of(pk_to(public(y))) == Done{public(y)} : Result<&2, &2, Cr.CrError, PK>}
  for h: {shared(x, public(y)) == shared(y, public(x)) : Result<&2, &2, Cr.CrError, B.Octets>}
  {Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, a, pk_to(public(y))) == Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, b, pk_to(public(x))) : Result<&2, &2, Cr.CrError, B.Octets>}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/crypto.bend&name=CrError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/kex.bend&name=CrKex.agree
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/kex.bend&name=cr.kex.with