🦏 Sc_rollup_operations.v

Proofs

The [validate_ty] is valid

Lemma validate_ty_is_valid {ret : Set} ty_value k_value :
  (letP ? _ := k_value tt in True) →
  letP ? _ := @Sc_rollup_operations.validate_ty ret ty_value k_value in
  True.
Proof.
  revert ty_value.
  revert k_value.
  fix IH 2.
  intros k_value ty_value H.
  unfold Sc_rollup_operations.validate_ty.
  destruct ty_value; trivial; try reflexivity.
  1,2,6 : (do 2 apply IH; trivial).
  1 - 4 : apply IH; trivial.
Qed.

The [validate_parameters_ty] is valid

Lemma validate_parameters_ty_is_valid ctxt parameters_ty :
  Raw_context.Valid.t ctxt →
  Saturation_repr.Valid.t
    (Sc_rollup_costs.is_valid_parameters_ty_cost
       (Script_typed_ir.Type_size.to_int
          (Script_typed_ir.ty_size parameters_ty))) →
  letP ? ctxt := Sc_rollup_operations.validate_parameters_ty
    ctxt parameters_ty in
  Raw_context.Valid.t ctxt.
Proof.
  intros H H0.
  unfold Sc_rollup_operations.validate_parameters_ty.
  eapply Error.split_letP. {
    apply Alpha_context.Gas.consume_is_valid.
    apply H.
    apply H0.
  }
  intros x H1.
  unfold Result_syntax.op_letplus.
  eapply Error.split_letP. {
   now apply validate_ty_is_valid.
  }
  intro x0.
  simpl.
  scongruence.
Qed.

The [validate_untyped_parameters_ty] is valid

Lemma validate_untyped_parameters_ty_is_valid {entrypoints : Set}
  ctxt parameters_ty :
  Raw_context.Valid.t ctxt →
  letP ? ctxt := Sc_rollup_operations.validate_untyped_parameters_ty
    ctxt parameters_ty in
  Raw_context.Valid.t ctxt.
Proof.
  intros H.
  unfold Sc_rollup_operations.validate_untyped_parameters_ty.
  eapply Error.split_letP. {
    now apply Script_ir_translator.parse_parameter_ty_and_entrypoints_is_valid.
  }
  intros x H1.
  destruct x eqn:D_X.
  destruct e eqn:D_E.
  apply validate_parameters_ty_is_valid.
  apply H1.
  destruct e0 eqn:D_E0.
  pose proof Script_typed_ir.ty.Valid.saturation_ty_size.
  apply H0.
Qed.

The [origination_proof_of_string] is valid

Lemma origination_proof_of_string_is_valid origination_proof kind_value :
  letP ? res := Sc_rollup_operations.origination_proof_of_string
    origination_proof kind_value in
  True.
Proof.
  unfold Sc_rollup_operations.origination_proof_of_string.
  step; hauto l: on.
Qed.

The [check_origination_proof] is valid

Lemma check_origination_proof_is_valid kind_value boot_sector origination_proof :
  letP ? res := Sc_rollup_operations.check_origination_proof
    kind_value boot_sector origination_proof in
  True.
Proof.
  unfold Sc_rollup_operations.check_origination_proof.
  simpl.
  step.
  unfold fail_when.
  step. {
    simpl.
    hauto lq: on.
  }
  {
    simpl.
    hauto l: on.
  }
Qed.

The [originate_is_valid] is valid

Lemma originate_is_valid {entrypoints : Set} ctxt kind_value boot_sector
  origination_proof parameters_ty :
  Raw_context.Valid.t ctxt →
  letP ? '( _ ,ctxt ) := Sc_rollup_operations.originate ctxt kind_value
    boot_sector origination_proof parameters_ty in
  Raw_context.Valid.t ctxt.
Proof.
  intro H.
  unfold Sc_rollup_operations.originate.
  eapply Error.split_letP.
  {
    eapply Error.split_letP. {
      now apply Alpha_context.Script.force_decode_in_context_is_valid.
    }
    intros x H0.
    destruct x.
    now apply (validate_untyped_parameters_ty_is_valid
     (entrypoints:=entrypoints)).
  }
  intros x H0.
  eapply Error.split_letP. {
    apply origination_proof_of_string_is_valid.
  }
  intros x0 H1.
  eapply Error.split_letP. {
    apply check_origination_proof_is_valid.
  }
  intros x1 H2.
  eapply Error.split_letP. {
    apply Sc_rollup_commitment_repr.V1.genesis_commitment_is_valid.
  }
  intros x2 H3.
  unfold Lwt_result_syntax.op_letplus.
  eapply Error.split_letP. {
    now apply Sc_rollup_storage.originate_is_valid.
  }
  intros x3 H4.
  hauto lq: on.
Qed.

[validate_and_decode_output_proof] is valid. Note that [validate_and_decode_output_proof] is currently an axiom, (opaque). The [validate_and_decode_output_proof] is valid

Lemma validate_and_decode_output_proof_is_valid ctxt commit rollup string :
  Raw_context.Valid.t ctxt →
  letP ? '(_,ctxt ) := Sc_rollup_operations.validate_and_decode_output_proof
    ctxt commit rollup string in Raw_context.Valid.t ctxt.
Proof.
Admitted.

The [validate_outbox_level] is valid

Lemma validate_outbox_level_is_valid ctxt outbox_level lcc_level :
  letP ? res := Sc_rollup_operations.validate_outbox_level
    ctxt outbox_level lcc_level in True.
Proof.
  unfold Sc_rollup_operations.validate_outbox_level.
  unfold fail_unless.
  step. {
    simpl; apply I.
  }
  {
    unfold tzfail.
    hauto lq: on.
  }
Qed.

The function [execute_outbox_message_aux] is valid. Note that this function seems to be used only in the definition of function [execute_outbox_message], and that, only with [validate_and_decode_output_proof] as second parameter. Thus, the lemma can perhaps be altogether be ignored, whereas [execute_outbox_message_is_valid] should be proved on its own.

Lemma execute_outbox_message_aux_is_valid ctxt
  validate_and_decode_output_proof
  rollup cemented_commitment source (output_proof : string)
  (H : ∀ ctxt commit rollup string, Raw_context.Valid.t ctxt →
  letP ? '(_,ctxt ) := validate_and_decode_output_proof
    ctxt commit rollup string in Raw_context.Valid.t ctxt ) :
  Raw_context.Valid.t ctxt →
  letP ? '(_,ctxt ) := Sc_rollup_operations.execute_outbox_message_aux
  ctxt validate_and_decode_output_proof
  rollup cemented_commitment source output_proof in Raw_context.Valid.t ctxt.
Proof.
  unfold Sc_rollup_operations.execute_outbox_message_aux.
  intro H0.
  eapply Error.split_letP. {
    now apply Sc_rollup_commitment_storage
      .last_cemented_commitment_hash_with_level_is_valid.
  }
  intros x H1.
  step.
  step.
  unfold fail_unless.
  step. {
    simpl.
    eapply Error.split_letP. {
      apply H.
      apply H1.
    }
    {
      intros x0 H2.
      step.
      eapply Error.split_letP. {
        apply validate_outbox_level_is_valid.
      }
      { intros x1 H3.
        eapply Error.split_letP. {
          apply Sc_rollup_management_protocol
          .outbox_message_of_outbox_message_repr_is_valid.
        }
        intros x2 H4.
        step.
        step.
        eapply Error.split_letP.

@TODO Define and prove fold_left_map_e_is_valid in Environment/V8/List.v

        admit.
        admit.
      }
    }
  }
  {
    hauto lq: on.
  }
Admitted.

The function [execute_outbox_message] is valid.

Lemma execute_outbox_message_is_valid ctxt rollup cemented_commitment
    source output_proof : Raw_context.Valid.t ctxt →
    letP ? '(_,ctxt ) := @Sc_rollup_operations.execute_outbox_message ctxt
    rollup cemented_commitment source output_proof in Raw_context.Valid.t ctxt.
Proof.
  intros H. unfold Sc_rollup_operations.execute_outbox_message.
  apply execute_outbox_message_aux_is_valid.
  intros.
  apply Sc_rollup_operations.validate_and_decode_output_proof_is_valid.
  trivial.
  trivial.
Qed.