Skip to main content

💾 Storage_description.v

Proofs

See code, See simulations, Gitlab , OCaml

Our dependent veresion of [unpack] is equivalent to the original one.
Fixpoint dep_unpack_eq {a b c : Set}
  (v : Storage_description.dep_args a b c) (x : c) {struct v} :
  Storage_description.dep_unpack v x =
  Storage_description.unpack (Storage_description.to_args v) x.
Proof.
  destruct v; simpl.
  { now rewrite cast_eval. }
  { match goal with
    | _ : Storage_description.dep_args _ ?a ?inter_key,
      _ : Storage_description.dep_args ?inter_key ?b _
      |- context[cast_exists (Es := ?Es) ?T ?x] ⇒
      match Es with
      | [Set ** Set ** Set]
        rewrite (cast_exists_eval_3 (T := T)
          (E1 := inter_key) (E2 := b) (E3 := a))
      end
    end; rewrite cast_eval.
    now repeat (rewrite dep_unpack_eq; destruct Storage_description.unpack).
  }
Qed.

Our dependent veresion of [_pack] is equivalent to the original one.
Fixpoint dep_pack_eq {a b c : Set}
  (v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
  Storage_description.dep_pack v x y =
  Storage_description._pack (Storage_description.to_args v) x y.
Proof.
  destruct v; simpl.
  { now rewrite cast_eval. }
  { match goal with
    | _ : Storage_description.dep_args _ ?a ?inter_key,
      _ : Storage_description.dep_args ?inter_key ?b _
      |- context[cast_exists (Es := ?Es) ?T ?x] ⇒
      match Es with
      | [Set ** Set ** Set]
        rewrite (cast_exists_eval_3 (T := T)
          (E1 := inter_key) (E2 := b) (E3 := a))
      end
    end; rewrite cast_eval.
    destruct y.
    now repeat rewrite dep_pack_eq.
  }
Qed.

[dep_unpack] is the inverse of [dep_pack].
Fixpoint dep_unpack_dep_pack {a b c : Set}
  (v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
  Storage_description.dep_unpack v (Storage_description.dep_pack v x y) =
  (x, y).
Proof.
  destruct v; simpl; try reflexivity.
  Tactics.destruct_pairs.
  now repeat rewrite dep_unpack_dep_pack.
Qed.

[dep_pack] is the inverse of [dep_unpack].
Fixpoint dep_pack_dep_unpack {a b c : Set}
  (v : Storage_description.dep_args a b c) (z : c) {struct v} :
  (let '(x, y) := Storage_description.dep_unpack v z in
  Storage_description.dep_pack v x y) =
  z.
Proof.
  destruct v; Tactics.destruct_pairs; simpl; try reflexivity.
  repeat match goal with
  | |- context[Storage_description.dep_unpack ?v ?z] ⇒
    pose proof (dep_pack_dep_unpack _ _ _ v z);
    destruct (Storage_description.dep_unpack v z)
  end.
  congruence.
Qed.

Module INDEX.
  Definition to_Path {t : Set} (I : Storage_description.INDEX (t := t))
    : Path_encoding.S (t := t) := {|
      Path_encoding.S.to_path := I.(Storage_description.INDEX.to_path);
      Path_encoding.S.of_path := I.(Storage_description.INDEX.of_path);
      Path_encoding.S.path_length := I.(Storage_description.INDEX.path_length);
    |}.

  Module Valid.
    Record t {t : Set} (domain : t Prop)
      (I : Storage_description.INDEX (t := t)) : Prop := {
      Path_is_valid : Path_encoding.S.Valid.t (to_Path I);
      rpc_arg : RPC_arg.Valid.t domain I.(Storage_description.INDEX.rpc_arg);
      encoding_is_valid :
        Data_encoding.Valid.t domain I.(Storage_description.INDEX.encoding);
      compare_is_valid :
        Compare.Valid.t (fun _True) id
          I.(Storage_description.INDEX.compare);
    }.
  End Valid.
End INDEX.

Module Query.
Validity predicate for a query.
  Module Valid.
    Import Storage_description.query.

    Record t (q : Storage_description.query) : Prop := {
      depth : Pervasives.Int.Valid.non_negative q.(depth);
    }.
  End Valid.
End Query.

The query [depth_query] is valid.
Lemma depth_query_is_valid :
  RPC_query.Valid.t Query.Valid.t Storage_description.depth_query.
Proof.
  RPC_query.valid_auto.
Qed.