LAWS.sign_verify_bytes_if: law of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
Lines 281-299 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=281&end_line=299

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/sign.bend as Sg

# Signatures and key agreement (sign.bend, kex.bend): the generic helpers
# keep the interface laws (README.md); the instances (RSA, DH, ECDSA, ECDH,
# SM2, EC-RDSA) and their laws are in bend-osdev-pubkey. A signature
# checked from the public key's bytes is accepted, for every scheme, secret
# key and message, when the scheme's pk_format and accepts laws hold there
# (hf, ha)
law sign_verify_bytes_if:
  for ~SK: Data
  for ~PK: Data
  for ~public: SK -> PK
  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
  for ~pk_to: PK -> B.Octets
  for ~sign: SK -> B.Octets -> B.Octets
  for ~verify: PK -> B.Octets -> B.Octets -> Bool
  for +sk: SK
  for +m: B.Octets
  for hf: {pk_of(pk_to(public(sk))) == Done{public(sk)} : Result<&2, &2, Cr.CrError, PK>}
  for ha: {verify(public(sk), m, sign(sk, m)) == True{} : Bool}
  {Sg.CrSign.verify_bytes(~PK, ~pk_of, ~verify, pk_to(public(sk)), m, sign(sk, m)) == True{} : Bool}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/sign.bend&name=CrSign.verify_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/sign.bend&name=cr.sign.check