🍃 Context.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Base58.
Require TezosOfOCaml.Environment.Structs.V0.Context_hash.
Require TezosOfOCaml.Environment.Structs.V0.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
| None ⇒ false
end.
Definition mem_tree (view : t) (path : key) : bool :=
match find_tree view path with
| Some _ ⇒ true
| None ⇒ false
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.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Base58.
Require TezosOfOCaml.Environment.Structs.V0.Context_hash.
Require TezosOfOCaml.Environment.Structs.V0.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
| None ⇒ false
end.
Definition mem_tree (view : t) (path : key) : bool :=
match find_tree view path with
| Some _ ⇒ true
| None ⇒ false
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
| None ⇒ false
end.
Definition mem_tree (tr : tree) (path : key) : bool :=
match find_tree tr path with
| Some _ ⇒ true
| None ⇒ false
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;
|}.
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
| None ⇒ false
end.
Definition mem_tree (tr : tree) (path : key) : bool :=
match find_tree tr path with
| Some _ ⇒ true
| None ⇒ false
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;
|}.