🍃 Bls.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.Structs.V7.Bls.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.Structs.V7.Bls.
[of_bytes_opt] applied on [to_bytes].
[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.
∀ (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].
[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.
∀ (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.
∀ (x : Bls.t) (st : string),
Bls.of_b58check_exn st = x →
Bls.to_b58check x = st.
[of_b58check_opt] applied on [to_b58check].
Axiom of_b58check_opt_to_b58check :
∀ (x : Bls.t),
Bls.of_b58check_opt (Bls.to_b58check x) = Some x.
∀ (x : Bls.t),
Bls.of_b58check_opt (Bls.to_b58check x) = Some x.
[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.
∀ (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
Axiom pairing_check_cons :
∀ x xs xs',
Primitive.pairing_check xs = Primitive.pairing_check xs' →
Primitive.pairing_check (x::xs) = Primitive.pairing_check (x::xs').
End Primitive.
∀ x xs xs',
Primitive.pairing_check xs = Primitive.pairing_check xs' →
Primitive.pairing_check (x::xs) = Primitive.pairing_check (x::xs').
End Primitive.