Skip to main content

🍃 Context.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Base58.
Require Proto_alpha.Environment.Context_hash.
Require Proto_alpha.Environment.Map.

Inductive depth : Set :=
| Ge : int depth
| Lt : int depth
| Eq : int depth
| Le : int depth
| Gt : int depth.

Parameter config : Set.

Parameter equal_config : config config bool.

Module VIEW.
  Record signature {t key value tree : Set} : Set := {
    t := t;
    key := key;
    value := value;
    tree := tree;
    mem : t key bool;
    mem_tree : t key bool;
    find : t key option value;
    find_tree : t key option tree;
    list_value :
      t option int option int key list (string × tree);
    length : t key int;
    add : t key value t;
    add_tree : t key tree t;
    remove : t key t;
    fold :
       {a : Set},
      option depth t key Variant.t a (key tree a a)
      a;
    config_value : t config;
  }.
End VIEW.
Definition VIEW := @VIEW.signature.
Arguments VIEW {_ _ _ _}.

Module Kind.
  Inductive t : Set :=
  | Tree : t
  | Value : t.
End Kind.

Module TREE.
  Record signature {t tree key value : Set} : Set := {
    t := t;
    tree := tree;
    key := key;
    value := value;
    mem : tree key bool;
    mem_tree : tree key bool;
    find : tree key option value;
    find_tree : tree key option tree;
    list_value :
      tree option int option int key list (string × tree);
    length : tree key int;
    add : tree key value tree;
    add_tree : tree key tree tree;
    remove : tree key tree;
    fold :
       {a : Set},
      option depth tree key Variant.t a
      (key tree a a) a;
    config_value : tree config;
    empty : t tree;
    is_empty : tree bool;
    kind_value : tree Kind.t;
    to_value : tree option value;
    of_value : t value tree;
    hash_value : tree Context_hash.t;
    equal : tree tree bool;
    clear : option int tree unit;
  }.
End TREE.
Definition TREE := @TREE.signature.
Arguments TREE {_ _ _ _}.

Module Proof.
  Definition step : Set := string.

  Definition value : Set := bytes.

  Definition index : Set := int.

  Definition hash : Set := Context_hash.t.

  Module inode.
    Record record {a : Set} : Set := Build {
      length : int;
      proofs : list (index × a) }.
    Arguments record : clear implicits.
    Definition with_length {t_a} length (r : record t_a) :=
      Build t_a length r.(proofs).
    Definition with_proofs {t_a} proofs (r : record t_a) :=
      Build t_a r.(length) proofs.
  End inode.
  Definition inode := inode.record.

  Module inode_extender.
    Record record {a : Set} : Set := Build {
      length : int;
      segment : list index;
      proof : a }.
    Arguments record : clear implicits.
    Definition with_length {t_a} length (r : record t_a) :=
      Build t_a length r.(segment) r.(proof).
    Definition with_segment {t_a} segment (r : record t_a) :=
      Build t_a r.(length) segment r.(proof).
    Definition with_proof {t_a} proof (r : record t_a) :=
      Build t_a r.(length) r.(segment) proof.
  End inode_extender.
  Definition inode_extender := inode_extender.record.

  Inductive tree : Set :=
  | Value : value tree
  | Blinded_value : hash tree
  | Node : list (step × tree) tree
  | Blinded_node : hash tree
  | Inode : inode inode_tree tree
  | Extender : inode_extender inode_tree tree
  
  with inode_tree : Set :=
  | Blinded_inode : hash inode_tree
  | Inode_values : list (step × tree) inode_tree
  | Inode_tree : inode inode_tree inode_tree
  | Inode_extender : inode_extender inode_tree inode_tree.

  Inductive kinded_hash : Set :=
  | KNode : hash kinded_hash
  | KValue : hash kinded_hash.

  Module Stream.
    Inductive elt : Set :=
    | Value : value elt
    | Node : list (step × kinded_hash) elt
    | Inode : inode hash elt
    | Inode_extender : inode_extender hash elt.

    Definition t : Set := Seq.t elt.
  End Stream.

  Definition stream : Set := Stream.t.

  Module t.
    Record record {a : Set} : Set := Build {
      version : int;
      before : kinded_hash;
      after : kinded_hash;
      state : a }.
    Arguments record : clear implicits.
    Definition with_version {t_a} version (r : record t_a) :=
      Build t_a version r.(before) r.(after) r.(state).
    Definition with_before {t_a} before (r : record t_a) :=
      Build t_a r.(version) before r.(after) r.(state).
    Definition with_after {t_a} after (r : record t_a) :=
      Build t_a r.(version) r.(before) after r.(state).
    Definition with_state {t_a} state (r : record t_a) :=
      Build t_a r.(version) r.(before) r.(after) state.
  End t.
  Definition t := t.record.
End Proof.

Parameter t : Set.

Definition key : Set := list string.

Definition value : Set := bytes.

Parameter tree : Set.

Parameter find : t key option value.

Parameter find_tree : t key option tree.

Definition mem (view : t) (path : key) : bool :=
  match find view path with
  | Some _true
  | Nonefalse
  end.

Definition mem_tree (view : t) (path : key) : bool :=
  match find_tree view path with
  | Some _true
  | Nonefalse
  end.

Parameter list_value :
  t option int option int key list (string × tree).

Parameter length : t key int.

Parameter update : t key option value t.

Parameter update_tree : t key option tree t.

Definition add (view : t) (path : key) (v : value) : t :=
  update view path (Some v).

Definition add_tree (view : t) (path : key) (v : tree) : t :=
  update_tree view path (Some v).

Definition remove (view : t) (path : key) : t :=
  update view path None.

The list of elements seen by a sorted fold operation.
Parameter flatten_view : option depth t key list (key × tree).

Definition fold_sorted {a : Set} (d : option depth) (view : t) (path : key)
  (acc : a) (f : key tree a a) : a :=
  List.fold_right
    (fun p acc'f (fst p) (snd p) acc')
    (flatten_view d view path)
    acc.

Parameter fold_undefined : {a : Set},
  option depth t key a (key tree a a) a.

Definition fold {a : Set} (d : option depth) (view : t) (path : key)
  (order : Variant.t) (acc : a) (f : key tree a a) : a :=
  match order with
  | Variant.Build order _ _
    if String.eqb order "Sorted" then
      fold_sorted d view path acc f
    else
      fold_undefined d view path acc f
  end.

Parameter config_value : t config.

Module Tree.
  Parameter find : tree key option value.

  Parameter find_tree : tree key option tree.

  Definition mem (tr : tree) (path : key) : bool :=
    match find tr path with
    | Some _true
    | Nonefalse
    end.

  Definition mem_tree (tr : tree) (path : key) : bool :=
    match find_tree tr path with
    | Some _true
    | Nonefalse
    end.

  Parameter list_value :
    tree option int option int key list (string × tree).

  Parameter length : tree key int.

  Parameter update : tree key option value tree.

  Parameter update_tree : tree key option tree tree.

  Definition add (tr : tree) (path : key) (v : value) : tree :=
    update tr path (Some v).

  Definition add_tree (tr : tree) (path : key) (v : tree) : tree :=
    update_tree tr path (Some v).

  Definition remove (tr : tree) (path : key) : tree :=
    update tr path None.

  Parameter fold : {a : Set},
    option depth tree key Variant.t a (key tree a a)
    a.

  Parameter config_value : tree config.

  Parameter empty : t tree.

  Parameter is_empty : tree bool.

  Parameter kind_value : tree Kind.t.

  Parameter to_value : tree option value.

  Parameter of_value : t value tree.

  Parameter hash_value : tree Context_hash.t.

  Parameter equal : tree tree bool.

  Parameter clear : option int tree unit.

  Definition module :
    TREE (t := t) (tree := tree) (key := key) (value := value) :=
      {|
        TREE.mem := mem;
        TREE.mem_tree := mem_tree;
        TREE.find := find;
        TREE.find_tree := find_tree;
        TREE.list_value := list_value;
        TREE.length := length;
        TREE.add := add;
        TREE.add_tree := add_tree;
        TREE.remove := remove;
        TREE.fold _ := fold;
        TREE.config_value := config_value;
        TREE.empty := empty;
        TREE.is_empty := is_empty;
        TREE.kind_value := kind_value;
        TREE.to_value := to_value;
        TREE.of_value := of_value;
        TREE.hash_value := hash_value;
        TREE.equal := equal;
        TREE.clear := clear;
      |}.
End Tree.
Definition Tree := Tree.module.

Definition verifier (proof result : Set) : Set :=
  proof (tree tree × result)
  Pervasives.result (tree × result) Variant.t.

Definition tree_proof : Set := Proof.t Proof.tree.

Parameter tree_proof_encoding : Data_encoding.t tree_proof.

Parameter verify_tree_proof : {a : Set}, verifier tree_proof a.

Definition stream_proof : Set := Proof.t Proof.stream.

Parameter stream_proof_encoding : Data_encoding.t stream_proof.

Parameter verify_stream_proof : {a : Set}, verifier stream_proof a.

Module PROOF_ENCODING.
  Record signature : Set := {
    tree_proof_encoding : Data_encoding.t tree_proof;
    stream_proof_encoding : Data_encoding.t stream_proof;
  }.
End PROOF_ENCODING.
Definition PROOF_ENCODING := PROOF_ENCODING.signature.

Module Proof_encoding.
  Module V1.
    Parameter Tree32 : PROOF_ENCODING.

    Parameter Tree2 : PROOF_ENCODING.
  End V1.

  Module V2.
    Parameter Tree32 : PROOF_ENCODING.

    Parameter Tree2 : PROOF_ENCODING.
  End V2.
End Proof_encoding.

Parameter complete : t string list string.

Parameter get_hash_version : t Context_hash.Version.t.

Parameter set_hash_version :
  t Context_hash.Version.t Error_monad.shell_tzresult t.

Parameter cache_key : Set.

Definition cache_value := extensible_type.

Module CACHE.
  Record signature {t size index identifier key value : Set} : Set := {
    t := t;
    size := size;
    index := index;
    identifier := identifier;
    key := key;
    value := value;
    key_of_identifier : index identifier key;
    identifier_of_key : key identifier;
    pp : Format.formatter t unit;
    find : t key option value;
    set_cache_layout : t list size t;
    update : t key option (value × size) t;
    sync : t Bytes.t t;
    clear : t t;
    list_keys : t index option (list (key × size));
    key_rank : t key option int;
    future_cache_expectation : t int t;
    cache_size : t index option size;
    cache_size_limit : t index option size;
  }.
End CACHE.
Definition CACHE := @CACHE.signature.
Arguments CACHE {_ _ _ _ _ _}.

Parameter Cache :
  CACHE (t := t) (size := int) (index := int) (identifier := string)
    (key := cache_key) (value := cache_value).

Definition Included_VIEW_t : Set := t.

Definition Included_VIEW_tree : Set := tree.

Definition Included_VIEW :
  VIEW (t := Included_VIEW_t) (key := list string) (value := bytes)
    (tree := Included_VIEW_tree) :=
  {|
    VIEW.mem := mem;
    VIEW.mem_tree := mem_tree;
    VIEW.find := find;
    VIEW.find_tree := find_tree;
    VIEW.list_value := list_value;
    VIEW.length := length;
    VIEW.add := add;
    VIEW.add_tree := add_tree;
    VIEW.remove := remove;
    VIEW.fold _ := fold;
    VIEW.config_value := config_value;
  |}.