🍃 Plonk.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Bls12_381.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.S.

Definition scalar : Set := Bls12_381.Fr.(S.PRIME_FIELD.t).

Module Array.
  Parameter concat : ∀ {a : Set}, list (array a) → array a.

  Parameter length : ∀ {a : Set}, array a → int.

  Parameter to_list : ∀ {a : Set}, array a → list a.
End Array.

Parameter transcript : Set.

Parameter verifier_public_parameters : Set.

Parameter proof : Set.

Parameter verifier_public_parameters_encoding :
  Data_encoding.t verifier_public_parameters.

Parameter proof_encoding : Data_encoding.t proof.

Parameter transcript_encoding : Data_encoding.t transcript.

Parameter scalar_encoding : Data_encoding.t scalar.

Parameter verify :
  verifier_public_parameters × transcript → array scalar → proof → bool.

Parameter verify_multi_circuits :
  verifier_public_parameters × transcript →
  list (string × list (array scalar)) → proof → bool.