🐆 Tx_rollup_l2_verifier.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_verifier.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_message_repr.

The function [verify_proof_model] is valid.

Lemma verify_proof_model_is_valid message_size proof_size :
  Saturation_repr.Valid.t (
    Tx_rollup_l2_verifier.verify_proof_model message_size proof_size
  ).
Proof.
  apply Saturation_repr.add_is_valid.
Qed.

The function [consume_verify_proof_cost] is valid.

Lemma consume_verify_proof_cost_is_valid ctxt message_size proof_size
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? ctxt :=
    Tx_rollup_l2_verifier.consume_verify_proof_cost
      ctxt message_size proof_size in
  Raw_context.Valid.t ctxt.
Proof.
  unfold Tx_rollup_l2_verifier.consume_verify_proof_cost.
  apply Raw_context.consume_gas_is_valid; trivial.
  apply verify_proof_model_is_valid.
Qed.

The function [hash_message_result] is valid.

Lemma hash_message_result_is_valid
  ctxt after withdraw :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,_) :=
    Tx_rollup_l2_verifier.hash_message_result ctxt after withdraw in
  Raw_context.Valid.t ctxt.
Proof.
  apply Tx_rollup_hash_builder.message_result_is_valid.
Qed.
(*
Definition after_hash_when_proof_failed
  (ctxt : Alpha_context.context) (before : Context_hash.t)
  : M? (Alpha_context.context * Alpha_context.Tx_rollup_message_result_hash.t) :=
  hash_message_result ctxt before
*)

The function [after_has_when_proof_failed] is valid.

Lemma after_hash_when_proof_failed_is_valid
  ctxt before :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,_) :=
    Tx_rollup_l2_verifier.after_hash_when_proof_failed ctxt before in
  Raw_context.Valid.t ctxt.
Proof.
  apply hash_message_result_is_valid.
Qed.

The function [compute_proof_after_hash] is valid.

Lemma compute_proof_after_hash_is_valid
  max_proof_size s_z ctxt parameters agreed proof message :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,_) :=
    Tx_rollup_l2_verifier.compute_proof_after_hash
      max_proof_size
      s_z
      ctxt
      parameters
      agreed
      proof
      message
    in
  Raw_context.Valid.t ctxt.
Proof.
  (* TODO: [compute_proof_after_hash] is an axiom *)
Admitted.

The function [verify_proof] is valid. Perhaps a pre-condition on [max_proof_size] could be added.

Lemma verify_proof_is_valid ctxt parameters message proof_value agreed
  rejected max_proof_size s_z :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Tx_rollup_l2_verifier.verify_proof ctxt parameters message
    proof_value agreed rejected max_proof_size s_z in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  Error.split_error_with compute_proof_after_hash_is_valid.
  Tactics.destruct_pairs.
  now destruct Alpha_context.Tx_rollup_message_result_hash.op_ltgt.
Qed.