Skip to main content

🍃 Context.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.Map.

#[local] Open Scope list.

Module Key.
  Definition Compare : Compare.S (t := Context.key) :=
    Compare.List {| Compare.COMPARABLE.compare := String.compare |}.

  Definition compare : Context.key Context.key int :=
    Compare.(Compare.S.compare).

  Axiom compare_is_valid : Compare.Valid.t (fun _True) id compare.

  Definition eqb : Context.key Context.key bool :=
    Compare.(Compare.S.op_eq).

  (* @TODO verify *)
  Axiom eqb_implies_eq : path1 path2,
    eqb path1 path2 = true
    path1 = path2.

  Axiom eqb_refl : path,
    eqb path path = true.

  Definition lt (path1 path2 : Context.key) : Prop :=
    Compare.(Compare.S.op_lt) path1 path2 = true.
End Key.

Relate the [find] and [flatten_view] primitives.
Axiom flatten_view_find_In :
   (view : Context.t) (root path : key) (depth : int),
  List.length path = depth
  ( v, Context.find view (op_at root path) = Some v)
   t, In (path, t) (Context.flatten_view (Some (Eq depth)) view root).

The ordering relation over [flatten_view].
Definition flatten_view_lt (x1 x2 : Context.key × Context.tree) : Prop :=
  Key.lt (fst x1) (fst x2).

The [flatten_view] is sorted.
Axiom flatten_view_is_sorted : view root depth,
  Sorted.Sorted flatten_view_lt (Context.flatten_view depth view root).

Axiom flatten_view_forall_find : view root depth,
  List.Forall
    (fun '(path, tree)
      (Context.Tree.to_value tree =
      Context.find view (root ++ path))
      ( sub_path,
      Context.Tree.find tree sub_path =
      Context.find view (root ++ path ++ sub_path))
    )
    (Context.flatten_view (Some (Context.Eq depth)) view root).

Definition find_value_in_flatten_view
  (path : Context.key) (elements : list (Context.key × Context.tree)) :
  option Context.value :=
  List.find_map
    (fun '(current_path, current_tree)
      if Key.eqb path current_path then
        Context.Tree.to_value current_tree
      else
        None
    )
    elements.

Axiom find_value_flatten_view_eq : view root path,
  let depth := Some (Context.Eq (List.length path)) in
  Context.find view (root ++ path) =
  find_value_in_flatten_view path (Context.flatten_view depth view root).

Definition find_tree_value_in_flatten_view
  (path1 path2 : Context.key) (elements : list (Context.key × Context.tree)) :
  option Context.value :=
  List.find_map
    (fun '(current_path, current_tree)
      if Key.eqb path1 current_path then
        Context.Tree.find current_tree path2
      else
        None
    )
    elements.

Axiom find_tree_value_flatten_view_eq : view root path1 path2,
  let depth := Some (Context.Eq (List.length path1)) in
  Context.find view (root ++ path1 ++ path2) =
  find_tree_value_in_flatten_view path1 path2
    (Context.flatten_view depth view root).

Fixpoint filter_trees {a} (f : a Kind.t) (xs : list a) : list a :=
  match xs with
  | [][]
  | x::ys
    match f x with
    | Kind.Treefilter_trees f ys
    | Kind.Valuex :: filter_trees f ys
    end
  end.

Lemma remove_kind_match : {a b : Set}
  (f : a Kind.t) (g : a b b) (xs : list a) y,
  fold_right
    (fun x acc
      match f x with
      | Kind.Treeacc
      | Kind.Valueg x acc
      end) xs y =
      fold_right g (filter_trees f xs) y.
  induction xs; intros.
  - reflexivity.
  - simpl; destruct (f a0).
    + apply IHxs.
    + simpl; rewrite IHxs; reflexivity.
Qed.

Lemma opt_map_filter_tree : {a b : Set}
  (f : a Kind.t) (h : a option b),
  ( x, f x = Kind.Tree h x = None) xs,
  List.filter_map h (filter_trees f xs) = List.filter_map h xs.
  induction xs; intros.
  - reflexivity.
  - simpl.
    + destruct (f a0) eqn:F.
      × rewrite (H a0 F); assumption.
      × simpl.
        destruct (h a0).
        ** congruence.
        ** exact IHxs.
Qed.

Reading a value that we just added returns this value.
Axiom find_add_same : (ctxt : Context.t) (k : key) (v : value),
  Context.find (Context.add ctxt k v) k = Some v.

Reading a value at a different address is like reading the context before the insertion.
Axiom find_add_different : (ctxt : Context.t) (k1 k2 : key) (v : value),
  k1 k2
  Context.find (Context.add ctxt k1 v) k2 = Context.find ctxt k2.

Rewrite either [find_add_same] or [find_add_different] depending on which one fits better.
Ltac rewrite_find_add :=
  match goal with
  | |- context[Context.find (Context.add _ ?k _) ?k] ⇒
    rewrite Context.find_add_same
  | |- context[Context.find (Context.add _ ?k1 _) ?k2] ⇒
    rewrite Context.find_add_different by now cbv
  end.

Proof encoding


Module PROOF_ENCODING.
  Module Valid.
    Import Environment.V7.Context.PROOF_ENCODING.

    Record t (x : Context.PROOF_ENCODING) : Prop := {
      tree_proof_encoding :
        Data_encoding.Valid.t (fun _True) x.(tree_proof_encoding);
      stream_proof_encoding :
        Data_encoding.Valid.t (fun _True) x.(stream_proof_encoding);
    }.
  End Valid.
End PROOF_ENCODING.

Module Proof_encoding.
  Module V1.
    Axiom Tree32_is_valid :
      PROOF_ENCODING.Valid.t Context.Proof_encoding.V1.Tree32.

    Axiom Tree2_is_valid :
      PROOF_ENCODING.Valid.t Context.Proof_encoding.V1.Tree2.
  End V1.

  Module V2.
    Axiom Tree32_is_valid :
      PROOF_ENCODING.Valid.t Context.Proof_encoding.V2.Tree32.

    Axiom Tree2_is_valid :
      PROOF_ENCODING.Valid.t Context.Proof_encoding.V2.Tree2.
  End V2.
End Proof_encoding.

Module Cache.
We assume that the sync of the cache is the identity.