Skip to main content

🍃 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.