🇿 Zk_rollup_apply.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_apply.

The function [assert_feature_enabled] is valid.

Lemma assert_feature_enabled_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? _ := Zk_rollup_apply.assert_feature_enabled ctxt in
  True.
Proof.
  intro H; Raw_context.Valid.destruct_rewrite H.
  unfold Zk_rollup_apply.assert_feature_enabled, error_unless.
  destruct (Alpha_context.Constants.zk_rollup_enable);
    [scongruence | hauto lq: on].
Qed.

The function [originate] is valid.

Lemma originate_is_valid {A : Set}
  ctxt_before_op ctxt public_parameters circuits_info init_state nb_ops :
  Raw_context.Valid.t ctxt →
  Raw_context.Valid.t ctxt_before_op →
  Zk_rollup_account_repr.static.Valid.t {|
    Alpha_context.Zk_rollup.Account.static.public_parameters :=
      public_parameters;
    Alpha_context.Zk_rollup.Account.static.state_length :=
      Array.length init_state;
    Alpha_context.Zk_rollup.Account.static.circuits_info :=
      circuits_info;
    Alpha_context.Zk_rollup.Account.static.nb_ops :=
      nb_ops
  |} →
  letP? '(ctxt, _, _) := @Zk_rollup_apply.originate A ctxt_before_op ctxt
    public_parameters circuits_info init_state nb_ops in
  Raw_context.Valid.t ctxt.
Proof.
  intros; unfold Zk_rollup_apply.originate.
  eapply Error.split_letP. {
    apply assert_feature_enabled_is_valid; trivial.
  }
  intros. destruct (_ <i _); simpl; try reflexivity.
  unfold Lwt_result_syntax.op_letplus.
  eapply Error.split_letP. {
    apply Zk_rollup_storage.originate_is_valid; scongruence.
  }
  hauto lq: on.
Qed.

The function [publish] is valid

Lemma publish_is_valid {A : Set} ctxt_before_op ctxt zk_rollup l2_ops :
  Raw_context.Valid.t ctxt_before_op →
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, succ_manager_op_res , l) :=
    @Zk_rollup_apply.publish A ctxt_before_op ctxt zk_rollup l2_ops
  in Raw_context.Valid.t ctxt.
Proof.

@TODO finish proof.

  intros H_bef_op H.
  unfold Zk_rollup_apply.publish.
  eapply Error.split_letP ; [
    apply Zk_rollup_apply.assert_feature_enabled_is_valid ; assumption |].
  intros _ _.
  eapply Error.split_letP with (fun _ ⇒ True). {
    destruct error_unless eqn:eq_error_unless ; [constructor |].
    rewrite <- eq_error_unless.
    destruct (for_all) ; constructor.
  }
  intros _ _.
Admitted.