💾 Storage_generated.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import CoqOfOCaml.Settings.
This file is automatically generated, do not edit it by hand
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context.
(* abreviations to avoid implicits inference errors *)
Notation of_functors_index := Raw_context.of_functors_index.
Notation of_description_index := Raw_context.of_description_index.
Notation of_lazy_storage_kind_id_index :=
Raw_context.of_lazy_storage_kind_id_index.
Module Block_round.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Block_round).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Block_round := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition name := ["block_round"].
End Helpers.
Axiom get : ∀ (ctxt : Raw_context.t),
Storage.Block_round
.(Storage.Simple_single_data_storage.get)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some x ⇒ Pervasives.Ok x
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom update : ∀ (ctxt : Raw_context.t) value,
Storage.Block_round
.(Storage.Simple_single_data_storage.update)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒
return? Helpers.set ctxt (Some value)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
Axiom init_value : ∀ (ctxt : Raw_context.t) value,
Storage.Block_round
.(Storage.Simple_single_data_storage.init_value)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| None ⇒
return? Helpers.set ctxt (Some value)
| Some _ ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
#[global] Hint Rewrite get update init_value : storage_db.
#[global] Opaque Storage.Block_round.
End Block_round.
Module Tenderbake.
Module First_level_of_protocol.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Tenderbake_First_level_of_protocol).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Tenderbake_First_level_of_protocol := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition name := ["first_level_of_protocol"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.mem)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ true
| None ⇒ false
end.
Axiom get : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.get)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some x ⇒ Pervasives.Ok x
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.find)
(Raw_context.to_t ctxt) =
return? Helpers.get ctxt.
Axiom init_value : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.init_value)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| None ⇒
return? Helpers.set ctxt (Some value)
| Some _ ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
Axiom update : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.update)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt (Some value)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
end.
Axiom add : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.add)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt (Some value)
| None ⇒ (Raw_context.to_t ctxt)
end.
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.add_or_remove)
(Raw_context.to_t ctxt) value =
Helpers.set ctxt value.
Axiom remove_existing : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.remove_existing)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt None
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del)
end.
Axiom remove : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.First_level_of_protocol
.(Storage_sigs.Single_data_storage.remove)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt None
| None ⇒ Raw_context.to_t ctxt
end.
#[global] Hint Rewrite mem get find init_value update add
add_or_remove remove_existing remove : storage_db.
#[global] Opaque Storage.Tenderbake.First_level_of_protocol.
End First_level_of_protocol.
Module Endorsement_branch.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Tenderbake_Endorsement_branch).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Tenderbake_Endorsement_branch := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition name := ["endorsement_branch"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.mem)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ true
| None ⇒ false
end.
Axiom get : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.get)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some x ⇒ Pervasives.Ok x
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.find)
(Raw_context.to_t ctxt) =
return? Helpers.get ctxt.
Axiom init_value : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.init_value)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| None ⇒
return? Helpers.set ctxt (Some value)
| Some _ ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
Axiom update : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.update)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt (Some value)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
end.
Axiom add : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.add)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt (Some value)
| None ⇒ (Raw_context.to_t ctxt)
end.
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.add_or_remove)
(Raw_context.to_t ctxt) value =
Helpers.set ctxt value.
Axiom remove_existing : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.remove_existing)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt None
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del)
end.
Axiom remove : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Endorsement_branch
.(Storage_sigs.Single_data_storage.remove)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt None
| None ⇒ Raw_context.to_t ctxt
end.
#[global] Hint Rewrite mem get find init_value update add
add_or_remove remove_existing remove : storage_db.
#[global] Opaque Storage.Tenderbake.Endorsement_branch.
End Endorsement_branch.
Module Grand_parent_branch.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Tenderbake_Grand_parent_branch).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Tenderbake_Grand_parent_branch := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition name := ["grand_parent_branch"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.mem)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ true
| None ⇒ false
end.
Axiom get : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.get)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some x ⇒ Pervasives.Ok x
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.find)
(Raw_context.to_t ctxt) =
return? Helpers.get ctxt.
Axiom init_value : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.init_value)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| None ⇒
return? Helpers.set ctxt (Some value)
| Some _ ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
Axiom update : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.update)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt (Some value)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
end.
Axiom add : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.add)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt (Some value)
| None ⇒ (Raw_context.to_t ctxt)
end.
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) value,
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.add_or_remove)
(Raw_context.to_t ctxt) value =
Helpers.set ctxt value.
Axiom remove_existing : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.remove_existing)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ return? Helpers.set ctxt None
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del)
end.
Axiom remove : ∀ (ctxt : Raw_context.t),
Storage.Tenderbake.Grand_parent_branch
.(Storage_sigs.Single_data_storage.remove)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some _ ⇒ Helpers.set ctxt None
| None ⇒ Raw_context.to_t ctxt
end.
#[global] Hint Rewrite mem get find init_value update add
add_or_remove remove_existing remove : storage_db.
#[global] Opaque Storage.Tenderbake.Grand_parent_branch.
End Grand_parent_branch.
End Tenderbake.
Module Contract.
Module Global_counter.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Global_counter).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Global_counter := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition name := ["global_counter"].
End Helpers.
Axiom get : ∀ (ctxt : Raw_context.t),
Storage.Contract.Global_counter
.(Storage.Simple_single_data_storage.get)
(Raw_context.to_t ctxt) =
match Helpers.get ctxt with
| Some x ⇒ Pervasives.Ok x
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom update : ∀ (ctxt : Raw_context.t) value,
Storage.Contract.Global_counter
.(Storage.Simple_single_data_storage.update)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| Some _ ⇒
return? Helpers.set ctxt (Some value)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
Axiom init_value : ∀ (ctxt : Raw_context.t) value,
Storage.Contract.Global_counter
.(Storage.Simple_single_data_storage.init_value)
(Raw_context.to_t ctxt) value =
match Helpers.get ctxt with
| None ⇒
return? Helpers.set ctxt (Some value)
| Some _ ⇒
Raw_context.storage_error_value
(Raw_context.Existing_key Helpers.name)
end.
#[global] Hint Rewrite get update init_value : storage_db.
#[global] Opaque Storage.Contract.Global_counter.
End Global_counter.
Module Spendable_balance.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Spendable_balance).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Spendable_balance := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["balance"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Spendable_balance
.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Spendable_balance.
End Spendable_balance.
Module Missed_endorsements.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Missed_endorsements).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Missed_endorsements := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["missed_endorsements"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Missed_endorsements
.(Storage_sigs.Indexed_data_storage.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Missed_endorsements.
End Missed_endorsements.
Module Manager.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Manager).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Manager := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["manager"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Manager
.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Manager.
End Manager.
Module Consensus_key.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Consensus_key).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Consensus_key := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["consensus_keys";"active"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Consensus_key
.(Storage_sigs.Indexed_data_storage.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Consensus_key.
End Consensus_key.
Module Pending_consensus_keys.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Pending_consensus_keys).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Pending_consensus_keys := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition Map :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments Map /.
Definition Submap :=
Storage_sigs.Indexed_map.Map
(of_description_index Cycle_repr.Index).
Arguments Submap /.
Definition name := ["consensus_key";"pendings"].
End Helpers.
Axiom mem : ∀ ctxt key subkey,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.Map).(Map.S.find)
key (Helpers.get ctxt) in
match map with
| Some map ⇒
(Helpers.Submap).(Map.S.mem) subkey map
| None ⇒ false
end.
Axiom get : ∀ ctxt subkey key,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt, key)
subkey =
let error := Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get) in
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let value := (Helpers.Submap).(Map.S.find) subkey submap' in
match value with
| Some value' ⇒ return? value'
| None ⇒ error
end
| None ⇒ error
end.
Axiom find : ∀ ctxt subkey key,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt, key)
subkey =
return? (
let× map := (Helpers.Map).(Map.S.find)
key
(Helpers.get ctxt) in
let× value := (Helpers.Submap).(Map.S.find) subkey map in
return× value).
Axiom update : ∀ ctxt subkey key value,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt, key) subkey value =
let error := Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set) in
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
if (Helpers.Submap).(Map.S.mem) subkey submap'
then
let submap'' :=
(Helpers.Submap).(Map.S.add) subkey value submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
return? Helpers.set ctxt map'
else error
| None ⇒ error
end.
Axiom init_value : ∀ ctxt subkey key value,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt, key) subkey value =
let error := Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set) in
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
if (Helpers.Submap).(Map.S.mem) subkey submap'
then error
else
let submap'' :=
(Helpers.Submap).(Map.S.add) subkey value submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
return? Helpers.set ctxt map'
| None ⇒
let submap'' :=
(Helpers.Submap).(Map.S.singleton) subkey value in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
return? Helpers.set ctxt map'
end.
Axiom add : ∀ ctxt key subkey value,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.add)
(Raw_context.to_t ctxt, key) subkey value =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Submap).(Map.S.add) subkey value submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒
let submap'' :=
(Helpers.Submap).(Map.S.singleton) subkey value in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
end.
Axiom add_or_remove : ∀ ctxt key subkey value_opt,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.add_or_remove)
(Raw_context.to_t ctxt, key) subkey value_opt =
match value_opt with
| Some value ⇒
(* add the value *)
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Submap).(Map.S.add) subkey value submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒
let submap'' :=
(Helpers.Submap).(Map.S.singleton) subkey value in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
end
| None ⇒
(* remove the value *)
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Submap).(Map.S.remove) subkey submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒ Raw_context.to_t ctxt
end
end.
Axiom remove_existing : ∀ ctxt key subkey,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.remove_existing)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
if (Helpers.Submap).(Map.S.mem) subkey submap'
then
let submap'' :=
(Helpers.Submap).(Map.S.remove) subkey submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
return? Helpers.set ctxt map'
else
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del)
end.
Axiom remove : ∀ ctxt key subkey,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.remove)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Submap).(Map.S.remove) subkey submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒ Raw_context.to_t ctxt
end.
Axiom clear : ∀ (ctxt : Raw_context.t) key,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.clear)
(Raw_context.to_t ctxt, key) =
let map := (Helpers.get ctxt) in
let empty := (Helpers.Submap).(Map.S.empty) in
let map' := (Helpers.Map).(Map.S.add) key empty map in
return? Helpers.set ctxt map'.
Axiom keys : ∀ ctxt key,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.keys)
(Raw_context.to_t ctxt, key) =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒ return? List.map fst ((Helpers.Submap).(Map.S.bindings)
submap')
| None ⇒ return? []
end.
Axiom bindings : ∀ ctxt key,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.bindings)
(Raw_context.to_t ctxt, key) =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒ return? (Helpers.Submap).(Map.S.bindings) submap'
| None ⇒ return? []
end.
Axiom fold : ∀ {a : Set} ctxt key variant init f,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.fold)
(Raw_context.to_t ctxt, key)
variant
init
f =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let f' k v acc :=
let? acc := acc in
f k v acc in
(Helpers.Submap).(Map.S.fold) f' init (Pervasives.Ok submap')
| None ⇒ return? init
end.
Axiom fold_keys : ∀ {a : Set} ctxt key variant init f,
Storage.Contract.Pending_consensus_keys
.(Storage_sigs.Indexed_data_storage.fold_keys)
(Raw_context.to_t ctxt, key)
variant
init
f =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let f' k acc :=
let? acc := acc in
f k acc in
(Helpers.Submap).(Map.S.fold)
(fun k _ acc ⇒ f' k acc) init (Pervasives.Ok submap')
| None ⇒ return? init
end.
#[global] Hint Rewrite mem get find init_value update add
add_or_remove remove_existing remove @fold @fold_keys keys
bindings clear : storage_db.
#[global] Opaque Storage.Contract.Pending_consensus_keys.
End Pending_consensus_keys.
Module Delegate.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Delegate).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Delegate := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["delegate"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Delegate
.(Storage_sigs.Indexed_data_storage.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Delegate.
End Delegate.
Module Inactive_delegate.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Inactive_delegate).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Inactive_delegate := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_set._Set
(of_description_index Contract_repr.Index).
Arguments S /.
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) elt,
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.mem)
(Raw_context.to_t ctxt) elt =
Helpers.S.(_Set.S.mem) elt (Helpers.get ctxt).
Axiom add : ∀ (ctxt : Raw_context.t) elt,
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.add)
(Raw_context.to_t ctxt) elt =
Helpers.set ctxt (Helpers.S.(_Set.S.add) elt (Helpers.get ctxt)).
Axiom remove : ∀ (ctxt : Raw_context.t) elt,
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.remove)
(Raw_context.to_t ctxt) elt =
Helpers.set ctxt (Helpers.S.(_Set.S.remove) elt
(Helpers.get ctxt)).
Axiom elements : ∀ (ctxt : Raw_context.t),
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.elements)
(Raw_context.to_t ctxt) =
return? Helpers.S.(_Set.S.elements) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant (x : a)
(f : _ → a → M? a),
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.fold)
(Raw_context.to_t ctxt) variant x f =
Helpers.S.(_Set.S.fold)
(fun elt acc ⇒ let? acc := acc in f elt acc) (Helpers.get ctxt)
(Pervasives.Ok x).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Inactive_delegate
.(Storage_sigs.Data_set_storage.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt (Helpers.S.(_Set.S.empty)).
#[global] Hint Rewrite mem add remove elements @fold clear
: storage_db.
#[global] Opaque Storage.Contract.Inactive_delegate.
End Inactive_delegate.
Module Delegate_last_cycle_before_deactivation.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Delegate_last_cycle_before_deactivation).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Delegate_last_cycle_before_deactivation := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["delegate_desactivation"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Delegate_last_cycle_before_deactivation
.(Storage_sigs.Indexed_data_storage.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Delegate_last_cycle_before_deactivation.
End Delegate_last_cycle_before_deactivation.
Module Delegated.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Delegated).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Delegated := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition Map :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments Map /.
Definition Subset :=
Storage_sigs.Indexed_set._Set
(of_description_index Contract_repr.Index).
Arguments Subset /.
Definition name := ["delegated"].
End Helpers.
Axiom mem : ∀ ctxt key subkey,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.mem)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.Map).(Map.S.find)
key (Helpers.get ctxt) in
match map with
| Some map ⇒
(Helpers.Subset).(_Set.S.mem) subkey map
| None ⇒ false
end.
Axiom add : ∀ ctxt key subkey,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.add)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Subset).(_Set.S.add) subkey submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒
let submap'' :=
(Helpers.Subset).(_Set.S.singleton) subkey in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
end.
Axiom remove : ∀ ctxt key subkey,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.remove)
(Raw_context.to_t ctxt, key) subkey =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let submap'' :=
(Helpers.Subset).(_Set.S.remove) subkey submap' in
let map' := (Helpers.Map).(Map.S.add) key submap'' map in
Helpers.set ctxt map'
| None ⇒ Raw_context.to_t ctxt
end.
Axiom elements : ∀ ctxt key,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.elements)
(Raw_context.to_t ctxt, key) =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒ return? (Helpers.Subset).(_Set.S.elements) submap'
| None ⇒ return? []
end.
Axiom fold : ∀ {a : Set} ctxt key variant init f,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.fold)
(Raw_context.to_t ctxt, key)
variant
init
f =
let map := (Helpers.get ctxt) in
let submap := (Helpers.Map).(Map.S.find) key map in
match submap with
| Some submap' ⇒
let f' elm acc :=
let? acc := acc in
f elm acc in
(Helpers.Subset).(_Set.S.fold) f' init
(Pervasives.Ok submap')
| None ⇒ return? init
end.
Axiom clear : ∀ (ctxt : Raw_context.t) key,
Storage.Contract.Delegated
.(Storage_sigs.Data_set_storage.clear)
(Raw_context.to_t ctxt, key) =
let map := (Helpers.get ctxt) in
let empty := (Helpers.Subset).(_Set.S.empty) in
let map' := (Helpers.Map).(Map.S.add) key empty map in
return? Helpers.set ctxt map'.
#[global] Hint Rewrite mem add remove elements @fold clear
: storage_db.
#[global] Opaque Storage.Contract.Delegated.
End Delegated.
Module Counter.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Counter).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Counter := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["counter"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)).
Axiom add : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.add)
(Raw_context.to_t ctxt) k v =
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove)
(Raw_context.to_t ctxt) k v =
match v with
| Some v' ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
(Helpers.get ctxt))
| None ⇒
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.remove)
(Raw_context.to_t ctxt) k =
Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)).
Axiom clear : ∀ (ctxt : Raw_context.t),
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.clear)
(Raw_context.to_t ctxt) =
return? Helpers.set ctxt ((Helpers.S).(Map.S.empty)).
Axiom keys : ∀ (ctxt : Raw_context.t),
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.keys)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
Axiom bindings : ∀ (ctxt : Raw_context.t),
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.bindings)
(Raw_context.to_t ctxt) =
return? (Helpers.S).(Map.S.bindings) (Helpers.get ctxt).
Axiom fold : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → _ → a → M? a),
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.fold)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold) (fun k v acc ⇒ let? acc := acc in f k v acc)
(Helpers.get ctxt) (Pervasives.Ok x).
Axiom fold_keys : ∀ {a : Set} (ctxt : Raw_context.t) variant
(x : a) (f : _ → a → M? a),
Storage.Contract.Counter
.(Storage_sigs.Indexed_data_storage_with_local_context.fold_keys)
(Raw_context.to_t ctxt) variant x f =
(Helpers.S).(Map.S.fold)
(fun k _ acc ⇒ let? acc := acc in f k acc)
(Helpers.get ctxt) (Pervasives.Ok x).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove clear keys bindings
@fold @fold_keys : storage_db.
#[global] Opaque Storage.Contract.Counter.
End Counter.
Module Code.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Code).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Code := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["code"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
(Raw_context.to_t ctxt) k =
return? (Raw_context.to_t ctxt, (Helpers.S).(Map.S.mem) k
(Helpers.get ctxt)).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok (Raw_context.to_t ctxt, v)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Raw_context.to_t ctxt, (Some v))
| None ⇒ return? (Raw_context.to_t ctxt, None)
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
let ctxt := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)) in
return? (ctxt, size)
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? (Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)), size).
Axiom add : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(Raw_context.to_t ctxt) k v =
let storage := (Helpers.get ctxt) in
let bound := (Helpers.S).(Map.S.mem) k storage in
let storage' := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v storage) in
return? (storage', size, bound).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
let storage := Helpers.get ctxt in
let mem := (Helpers.S).(Map.S.mem) k storage in
match v with
| Some v' ⇒
let ctxt' := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
storage) in
return? (ctxt', size, mem)
| None ⇒
let ctxt' := Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
storage) in
return? (ctxt', size, mem)
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? (Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)), size)
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k size,
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.remove)
(Raw_context.to_t ctxt) k =
let storage := Helpers.get ctxt in
let mem := (Helpers.S).(Map.S.mem) k storage in
return? (Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
storage), size, mem).
Axiom keys_unaccounted : ∀ (ctxt : Raw_context.t),
Storage.Contract.Code
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.keys_unaccounted)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove keys_unaccounted
: storage_db.
#[global] Opaque Storage.Contract.Code.
End Code.
Module Storage.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Storage).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Storage := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["storage"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
(Raw_context.to_t ctxt) k =
return? (Raw_context.to_t ctxt, (Helpers.S).(Map.S.mem) k
(Helpers.get ctxt)).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok (Raw_context.to_t ctxt, v)
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Raw_context.to_t ctxt, (Some v))
| None ⇒ return? (Raw_context.to_t ctxt, None)
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
let ctxt := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt)) in
return? (ctxt, size)
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set)
else return? (Helpers.set ctxt ((Helpers.S).(Map.S.add)
k v (Helpers.get ctxt)), size).
Axiom add : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
(Raw_context.to_t ctxt) k v =
let storage := (Helpers.get ctxt) in
let bound := (Helpers.S).(Map.S.mem) k storage in
let storage' := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v storage) in
return? (storage', size, bound).
Axiom add_or_remove : ∀ (ctxt : Raw_context.t) k v size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove)
(Raw_context.to_t ctxt) k v =
let storage := Helpers.get ctxt in
let mem := (Helpers.S).(Map.S.mem) k storage in
match v with
| Some v' ⇒
let ctxt' := Helpers.set ctxt ((Helpers.S).(Map.S.add) k v'
storage) in
return? (ctxt', size, mem)
| None ⇒
let ctxt' := Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
storage) in
return? (ctxt', size, mem)
end.
Axiom remove_existing : ∀ (ctxt : Raw_context.t) k size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.remove_existing)
(Raw_context.to_t ctxt) k =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then return? (Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
(Helpers.get ctxt)), size)
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Del).
Axiom remove : ∀ (ctxt : Raw_context.t) k size,
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.remove)
(Raw_context.to_t ctxt) k =
let storage := Helpers.get ctxt in
let mem := (Helpers.S).(Map.S.mem) k storage in
return? (Helpers.set ctxt ((Helpers.S).(Map.S.remove) k
storage), size, mem).
Axiom keys_unaccounted : ∀ (ctxt : Raw_context.t),
Storage.Contract.Storage
.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage
.keys_unaccounted)
(Raw_context.to_t ctxt) =
return? List.map fst ((Helpers.S).(Map.S.bindings) (Helpers.get ctxt)).
#[global] Hint Rewrite mem get find update init_value add
add_or_remove remove_existing remove keys_unaccounted
: storage_db.
#[global] Opaque Storage.Contract.Storage.
End Storage.
Module Paid_storage_space.
Module Helpers.
Definition get (ctxt : Raw_context.t) :=
ctxt
.(Raw_context.Contract_Paid_storage_space).
Arguments get _ /.
Definition set (ctxt : Raw_context.t) value :=
let ctxt' := ctxt <| Raw_context.Contract_Paid_storage_space := value |> in
(Raw_context.to_t ctxt').
Arguments set _ _ /.
Definition S :=
Storage_sigs.Indexed_map.Map
(of_description_index Contract_repr.Index).
Arguments S /.
Definition name := ["paid_bytes"].
End Helpers.
Axiom mem : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Paid_storage_space
.(Storage_sigs.Indexed_data_storage.mem)
(Raw_context.to_t ctxt) k =
(Helpers.S).(Map.S.mem) k
(Helpers.get ctxt).
Axiom get : ∀ (ctxt : Raw_context.t) k,
Storage.Contract.Paid_storage_space
.(Storage_sigs.Indexed_data_storage.get)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ Pervasives.Ok v
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context.Get)
end.
Axiom find : ∀(ctxt : Raw_context.t) k,
Storage.Contract.Paid_storage_space
.(Storage_sigs.Indexed_data_storage.find)
(Raw_context.to_t ctxt) k =
let x := (Helpers.S).(Map.S.find) k (Helpers.get ctxt) in
match x with
| Some v ⇒ return? (Some v)
| None ⇒ return? None
end.
Axiom update : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Paid_storage_space
.(Storage_sigs.Indexed_data_storage.update)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then
return? Helpers.set ctxt ((Helpers.S).(Map.S.add) k v
(Helpers.get ctxt))
else Raw_context.storage_error_value
(Raw_context.Missing_key Helpers.name Raw_context._Set).
Axiom init_value : ∀ (ctxt : Raw_context.t) k v,
Storage.Contract.Paid_storage_space
.(Storage_sigs.Indexed_data_storage.init_value)
(Raw_context.to_t ctxt) k v =
if (Helpers.S).(Map.S.mem) k (Helpers.get ctxt)
then Raw_context.storage_error_value
(Raw_context.Missing_key