🌱 Seed_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.

Assumming [Constants_storage.preserved_cycles = 5] and current level cycles between 0 and 5, [init_value] success implies [for_cycle] success for the first [Constants_storage.preserved_cycles]

Lemma init_for_cycle_is_ok (absolute_key : Context.key)
  (ctxt : Raw_context.t) (seed: Seed_repr.seed) :
  let preserved_cycles := 5 in
  (∀ (ctxt : Raw_context.t),
     Constants_storage.preserved_cycles ctxt = preserved_cycles) →
  letP? ctxt' := Seed_storage.init_value None ctxt in
  let current_level := Level_storage.current ctxt' in
  let current_cycle := current_level.(Level_repr.t.cycle) in
  0 ≤ current_cycle ≤ preserved_cycles →
  Pervasives.is_ok (Seed_storage.for_cycle ctxt' current_cycle).
Proof.
  intros.
  unfold Seed_storage.init_value.
  rewrite H. simpl.
  unfold Int32.of_int,
   Cycle_repr.of_int32_exn, "+i"; simpl.
  repeat rewrite Int32.normalize_identity; try easy.
  repeat rewrite Pervasives.normalize_identity; try easy.
  do 7 (
    rewrite (Storage.Eq.Seeds.For_cycle.eq absolute_key).(
      Storage_sigs.For_cycle.Eq.init_value); simpl;
    unfold Storage_sigs.For_cycle.Op.init_value;
    destruct Storage_sigs.For_cycle.Op.mem; try easy; simpl).
  rewrite Int32.normalize_identity; [|easy].
  set (ctxt' := Storage.Eq.Seeds.For_cycle.apply _ _).
  intros.
  unfold Seed_storage.for_cycle.
  set (current_cycle' :=
         (Level_storage.current ctxt').(Level_repr.t.cycle)).
  rewrite H; simpl.
  unfold Cycle_repr.op_lteq, "+i",
    Cycle_repr.add, Cycle_repr.root_value,
    Cycle_repr.op_eq, Cycle_repr.sub, "-i32", "+i32", Int32.of_int.
  rewrite Pervasives.normalize_identity; try lia.
  repeat rewrite Int32.normalize_identity; try lia; simpl.
  assert (Hcurrent_cycle_dec :
           current_cycle' = 0 ∨ current_cycle' = 1 ∨
           current_cycle' = 2 ∨ current_cycle' = 3 ∨
           current_cycle' = 4 ∨ current_cycle' = 5 ∨
           current_cycle' = 6) by lia.
  subst preserved_cycles.
  destruct Hcurrent_cycle_dec
    as [H' | [H' | [H' | [H' | [H' | [H' | H']]]]]];
    rewrite H'; simpl;
    rewrite (Storage.Eq.Seeds.For_cycle.eq absolute_key).(
      Storage_sigs.For_cycle.Eq.get); simpl;
    subst ctxt';
    Storage.auto_parse_apply;
    repeat rewrite Pervasives.normalize_identity; try easy;
    repeat rewrite Int32.normalize_identity; try easy;
    Storage_sigs.For_cycle.Op.Unfold.all;
    repeat (rewrite Map.find_add_compare_int; simpl);
    try easy.
    all: apply Storage.generic_Path_encoding_Valid.
Qed.