🦏 Sc_rollup_wasm.v

Proofs

We split properties described in the module P into individual lemmas.

  Module P.
    Module Valid.
      Import Proto_alpha.Sc_rollup_wasm.V2_0_0.P.

The validity of a PVM implementation, Module P.

      Record t {Tree_t Tree_tree proof : Set}
        {LP : Sc_rollup_wasm.V2_0_0.P (Tree_t := Tree_t)
          (Tree_tree := Tree_tree) (proof := proof)} : Prop := {
          proof_encoding : Data_encoding.Valid.t (fun _ ⇒ True)
            (LP.(proof_encoding));
        }.
      Arguments t {_ _ _}.
    End Valid.
  End P.

We split properties described in the module S into individual lemmas.

  Module S.
    Module Valid.
      Import Proto_alpha.Sc_rollup_wasm.V2_0_0.S.

The validity of a PVM implementation, Module S.

      Record t {state context proof output_proof status : Set}
        {LS : Sc_rollup_wasm.V2_0_0.S (state := state) (context := context)
          (proof := proof) (output_proof := output_proof)
            (status := status) } : Prop := {
          proof_encoding : Data_encoding.Valid.t (fun _ ⇒ True)
            (LS.(proof_encoding));
          output_proof_encoding : Data_encoding.Valid.t (fun _ ⇒ True)
            (LS.(output_proof_encoding));
          get_tick state : Sc_rollup_tick_repr.Valid.t (LS.(get_tick) state);
        }.
      Arguments t {_ _ _}.
    End Valid.
  End S.

  Module Make.
    Import Proto_alpha.Sc_rollup_wasm.V2_0_0.Make.

The encoding [proof_encoding] is valid

    Lemma proof_encoding_is_valid `{FArgs} :
      Data_encoding.Valid.t (fun _ ⇒ True)
        Context.(Sc_rollup_wasm.V2_0_0.P.proof_encoding) →
      Data_encoding.Valid.t (fun _ ⇒ True) proof_encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve proof_encoding_is_valid : Data_encoding_db.

The function [verify_proof] is valid

    Lemma verify_proof_is_valid `{FArgs} input_given proof_value :
      letP ? 'res := verify_proof input_given proof_value in
        True.
    Proof.
      unfold verify_proof.
      step.
      step.
      reflexivity.
      unfold Lwt_result_syntax.tzfail.
      sfirstorder.
    Qed.

The function [produce_proof] is valid

    Lemma produce_proof_is_valid `{FArgs} context_value input_given
      state_value :
      letP ? 'prf := produce_proof context_value input_given state_value in
        True.
    Proof.
      unfold produce_proof.
      step.
      step; try (simpl; apply I).
      sfirstorder.
    Qed.

The function [produce_origination_proof] is valid

    Lemma produce_origination_proof_is_valid `{FArgs} context_value
      boot_sector :
      letP ? 'prf := produce_origination_proof context_value boot_sector in
        True.
    Proof.
      unfold produce_origination_proof.
      step.
      step; try (simpl; apply I).
      unfold Lwt_result_syntax.tzfail.
      unfold Structs.V8.Error_monad.Lwt_result_syntax.tzfail.
      sfirstorder.
    Qed.

    Module Valid.
      (* Validity predicate for the [output_proof] type *)
      Record t `{FArgs} (x : output_proof) : Prop := {
        outbox_level : 0 ≤ x.(output_proof.output_proof_output)
          .(Sc_rollup_PVM_sig.output.outbox_level) ≤ Int32.max_int;
        output_proof : 0 ≤ x.(output_proof.output_proof_output)
          .(Sc_rollup_PVM_sig.output.message_index);
        message : Sc_rollup_outbox_message_repr.Valid.t x.(output_proof
          .output_proof_output).(Sc_rollup_PVM_sig.output.message);
      }.
    End Valid.

The encoding [ouput_proof_encoding] is valid

    Lemma output_proof_encoding_is_valid `{FArgs} :
      Data_encoding.Valid.t (fun _ ⇒ True)
        Context.(Sc_rollup_wasm.V2_0_0.P.proof_encoding) →
      Data_encoding.Valid.t Valid.t output_proof_encoding.
    Proof.
      intro G.
      Data_encoding.Valid.data_encoding_auto.
      intros x H0.
      destruct H0.
      split_conj; try apply I; hauto l: on.
    Qed.
    #[global] Hint Resolve output_proof_encoding_is_valid : Data_encoding_db.
  End Make.

End V2_0_0.