Skip to main content

🍃 Bls.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

[of_bytes_opt] applied on [to_bytes].
Axiom of_bytes_opt_to_bytes :
   (x : Bls.t),
  Bls.of_bytes_opt (Bls.to_bytes x) = Some x.

[to_bytes] applied on [of_bytes_opt].
Axiom to_bytes_of_bytes_opt :
   (x : Bls.t) (bytes : Bytes.t),
  Bls.of_bytes_opt bytes = Some x
  Bls.to_bytes x = bytes.

[of_bytes_exn] applied on [to_bytes].
Axiom of_bytes_exn_to_bytes :
   (x : Bls.t),
  Bls.of_bytes_exn (Bls.to_bytes x) = x.

[to_bytes] applied on [of_bytes_exn].
Axiom to_bytes_of_bytes_exn :
   (x : Bls.t) (bytes : Bytes.t),
  Bls.of_bytes_exn bytes = x
  Bls.to_bytes x = bytes.

[of_b58check_exn] applied on [to_b58check].
[to_b58check] applied on [of_b58check_exn].
Axiom to_b58check_of_b58check_exn :
   (x : Bls.t) (st : string),
  Bls.of_b58check_exn st = x
  Bls.to_b58check x = st.

[of_b58check_opt] applied on [to_b58check].
[to_b58check] applied on [of_b58check_opt].
Axiom to_b58check_of_b58check_opt :
   (x : Bls.t) (st : string),
  Bls.of_b58check_opt st = Some x
  Bls.to_b58check x = st.

Module Primitive.
[pairing_check] : add new element at the beginning of the List