🌱 Seed_storage.v

Proofs

Access the [Storage.Cycle.Seed] substore in the simulated context [sim_ctxt]

#[local] Definition substore (sim_ctxt : Raw_context.t)
  : Storage_sigs.Indexed_data_storage.t
      (Raw_context.of_description_index Cycle_repr.Index)
      Seed_repr.seed :=
  sim_ctxt
    .(Raw_context.Cycle_Seed).
Arguments substore _ /.

Tactic to solve [Cycle_repr.add] cases

#[local] Ltac solve_cycle_repr_add :=
  apply Cycle_repr.add_is_valid;
    destruct_by_type (Raw_context.Valid.simulation _);
    destruct_by_type (Raw_context.config.Valid.simulation _);
    destruct_by_type (Constants_parametric_repr.Valid.t _);
    unfold Constants_storage.preserved_cycles in *; cbn in *; lia.

(* @TODO *)

[purge_nonces_and_get_unrevealed] is valid as long its inputs are valid

Lemma purge_nonces_and_get_unrevealed_is_valid
  (ctxt : Proto_alpha.Raw_context.t) (cycle : Cycle_repr.t) :
  Raw_context.Valid.t ctxt →
  Cycle_repr.Valid.t cycle →
  letP ? '(ctxt , _) :=
    Seed_storage.purge_nonces_and_get_unrevealed ctxt cycle in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_valid_ctxt H_valid_cycle.
  unfold Seed_storage.purge_nonces_and_get_unrevealed.
  cbn.
  eapply Error.split_letP.
  { apply Level_storage.levels_with_commitments_in_cycle_is_valid;
      [hauto l:on|assumption].
  }
  { intros.
    (* @TODO verify the fold_left here *) admit.
  }
Admitted.

(* @TODO *)

[compute_randao] is valid if the key [current_cycle + preserved_cycles + 1] exists in the substore

Lemma compute_randao_is_valid (ctxt : Proto_alpha.Raw_context.t) :
  Raw_context.Valid.on
    (fun sim_ctxt ⇒
      letP ? cycle :=
        Cycle_repr.add
          sim_ctxt
            .(Raw_context.config)
            .(Raw_context_aux.config.level)
            .(Level_repr.t.cycle)
           (Constants_storage.preserved_cycles ctxt +i 1) in
        Raw_context.Indexed_data_storage.key_exists
          cycle (substore sim_ctxt))
    ctxt →
  letP ? ctxt := Seed_storage.compute_randao ctxt in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_valid_ctxt.
  Raw_context.Valid.destruct_rewrite H_valid_ctxt.
  unfold Seed_storage.compute_randao. cbn.
  (* Cannot use split_letP here becasue I need this
     the equality generated by this destrut *)
  eapply Error.split_letP; cbn; [solve_cycle_repr_add|].
  intros.
  do 3 (step; [|hauto l:on]).
  eapply Error.split_letP; cbn.
  { apply Level_storage.levels_with_commitments_in_cycle_is_valid;
      [hauto l:on|].
    apply Cycle_repr.pred_is_valid in Heqo; [easy|].
    destruct H_sim_ctxt, config, level, cycle. lia.
  }
  { intros. eapply Error.split_letP; cbn.
    { with_strategy transparent [Storage.Seed.For_cycle]
      unfold Storage.Seed.For_cycle, Storage.Seed.For_cycle.module,
      Storage.Seed.For_cycle.get; cbn.
Admitted.

(* @TODO *)

[get_seed_computation_status] is valid

Lemma get_seed_computation_status_is_valid
  (ctxt : Proto_alpha.Raw_context.t) :
  Raw_context.Valid.t ctxt →
  letP ? _ := Seed_storage.get_seed_computation_status ctxt in
  True.
Proof.
Admitted.

(* @TODO *)

[check_vdf_is_valid] is valid

Lemma check_vdf_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  (vdf_solution : Seed_repr.vdf_solution) :
  Raw_context.Valid.t ctxt →
  letP ? _ := Seed_storage.check_vdf ctxt vdf_solution in
  True.
Proof.
Admitted.

(* @TODO *)

[update_seed] is valid if the context contains a seed for the last preserved cycle and a seed status

Lemma update_seed_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  (vdf_solution : Seed_repr.vdf_solution) :
  Raw_context.Valid.t ctxt →
  letP ? ctxt := Seed_storage.update_seed ctxt vdf_solution in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

[raw_for_cycle] is valid if there is a seed for this cycle in the substore

Lemma raw_for_cycle_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  (cycle : Cycle_repr.t) :
  Raw_context.Valid.on
    (fun sim_ctxt ⇒
       Raw_context.Indexed_data_storage.key_exists
         cycle
         (substore sim_ctxt))
    ctxt →
  letP ? _ :=
    Seed_storage.raw_for_cycle ctxt cycle in
  True.
Proof.
  intros H_valid_ctxt.
  Raw_context.Valid.destruct_rewrite H_valid_ctxt.
  unfold Seed_storage.raw_for_cycle.
  with_strategy transparent [Storage.Seed.For_cycle]
    unfold Storage.Seed.For_cycle, Storage.Seed.For_cycle.module,
    Storage.Seed.For_cycle.get; cbn.
  rewrite_db storage_db.
  Raw_context.Valid.destruct_rewrite H_valid_ctxt.
  cbn in ×.
  apply Map.mem_find_not_eq_none in H_sim_ctxt_domain.
  now step.
Qed.

[for_cycle ctxt cycle] has no internal errors if The [ctxt] context is valid. The [cycle] cycle is valid. There is a seed [seed] for the cycle [cycle] in the substore

Lemma for_cycle_is_valid (ctxt : Raw_context.t) (cycle : Cycle_repr.t) :
  Raw_context.Valid.on
    (fun sim_ctxt ⇒
      Raw_context.Indexed_data_storage.key_exists
        cycle
        (substore sim_ctxt))
    (Raw_context.to_t ctxt) →
  Cycle_repr.Valid.t cycle →
  letP ? _ := Seed_storage.for_cycle (Raw_context.to_t ctxt) cycle in
  True.
Proof.
  intros H_valid_ctxt H_valid_cycle.
  Raw_context.Valid.destruct_rewrite H_valid_ctxt.
  unfold Seed_storage.for_cycle; cbn.
  eapply Error.split_letP;
    [step; solve_cycle_repr_add|].
  intros.
  eapply Error.split_letP.
  { eapply Error.split_letP.
    { apply Cycle_repr.sub_is_valid.
      destruct H_sim_ctxt, config, constants.
      unfold Constants_storage.max_slashing_period. cbn. lia.
    }
    { intros. step; cbn; eauto.
      cbv. split; discriminate.
    }
  }
  { intros.
    eapply Error.split_letP; cbn.
    { unfold error_unless. step.
      { simpl. instantiate (1 := fun _ ⇒ True). reflexivity.
      }
      { easy. }
    }
    { intros.
      now apply Storage.Seed.For_cycle.get_is_valid.
    }
  }
Qed.