🏊 Mempool_validation.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Validate.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Module t.
Record record : Set := Build {
predecessor_hash : Block_hash.t;
operation_state : Validate.operation_conflict_state;
operations :
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation;
}.
Definition with_predecessor_hash predecessor_hash (r : record) :=
Build predecessor_hash r.(operation_state) r.(operations).
Definition with_operation_state operation_state (r : record) :=
Build r.(predecessor_hash) operation_state r.(operations).
Definition with_operations operations (r : record) :=
Build r.(predecessor_hash) r.(operation_state) operations.
End t.
Definition t := t.record.
Definition validation_info : Set := Validate.info.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Validate.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Module t.
Record record : Set := Build {
predecessor_hash : Block_hash.t;
operation_state : Validate.operation_conflict_state;
operations :
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation;
}.
Definition with_predecessor_hash predecessor_hash (r : record) :=
Build predecessor_hash r.(operation_state) r.(operations).
Definition with_operation_state operation_state (r : record) :=
Build r.(predecessor_hash) operation_state r.(operations).
Definition with_operations operations (r : record) :=
Build r.(predecessor_hash) r.(operation_state) operations.
End t.
Definition t := t.record.
Definition validation_info : Set := Validate.info.
Records for the constructor parameters
Module ConstructorRecords_add_result.
Module add_result.
Module Replaced.
Record record {removed : Set} : Set := Build {
removed : removed;
}.
Arguments record : clear implicits.
Definition with_removed {t_removed} removed (r : record t_removed) :=
Build t_removed removed.
End Replaced.
Definition Replaced_skeleton := Replaced.record.
End add_result.
End ConstructorRecords_add_result.
Import ConstructorRecords_add_result.
Reserved Notation "'add_result.Replaced".
Inductive add_result : Set :=
| Added : add_result
| Replaced : 'add_result.Replaced → add_result
| Unchanged : add_result
where "'add_result.Replaced" := (add_result.Replaced_skeleton Operation_hash.t).
Module add_result.
Include ConstructorRecords_add_result.add_result.
Definition Replaced := 'add_result.Replaced.
End add_result.
Definition operation_conflict : Set := Validate_errors.operation_conflict.
Inductive add_error : Set :=
| Validation_error : Error_monad.trace Error_monad._error → add_error
| Add_conflict : operation_conflict → add_error.
Inductive merge_error : Set :=
| Incompatible_mempool : merge_error
| Merge_conflict : operation_conflict → merge_error.
Definition encoding : Data_encoding.t t :=
Data_encoding.def "mempool" None None
(Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state;
t.operations := operations
|} := function_parameter in
(predecessor_hash, operation_state, operations))
(fun (function_parameter :
Block_hash.t × Validate.operation_conflict_state ×
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation)
⇒
let '(predecessor_hash, operation_state, operations) :=
function_parameter in
{| t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state; t.operations := operations; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "predecessor_hash" Block_hash.encoding)
(Data_encoding.req None None "operation_state"
Validate.operation_conflict_state_encoding)
(Data_encoding.req None None "operations"
(Operation_hash.Map.(S.INDEXES_MAP.encoding)
(Data_encoding.dynamic_size (Some (Variant.Build "Uint30" unit tt))
Alpha_context.Operation.encoding))))).
Definition init_value
(ctxt : Alpha_context.context) (chain_id : Chain_id.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) (predecessor_hash : Block_hash.t)
(grandparent_round : Alpha_context.Round.t) : validation_info × t :=
let '{|
Validate.validation_state.info := info_value;
Validate.validation_state.operation_state := operation_state
|} :=
Validate.begin_partial_construction ctxt chain_id predecessor_level
predecessor_round grandparent_round in
(info_value,
{| t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state;
t.operations := Operation_hash.Map.(S.INDEXES_MAP.empty); |}).
Inductive keep_or_replace : Set :=
| Keep : keep_or_replace
| Replace : keep_or_replace.
Definition conflict_handler : Set :=
Operation_hash.t × Alpha_context.packed_operation →
Operation_hash.t × Alpha_context.packed_operation → keep_or_replace.
Definition remove_operation (mempool : t) (oph : Operation_hash.t) : t :=
match Operation_hash.Map.(S.INDEXES_MAP.find_opt) oph mempool.(t.operations)
with
| None ⇒ mempool
|
Some {|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} ⇒
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.remove) oph mempool.(t.operations) in
let operation_state :=
Validate.remove_operation mempool.(t.operation_state)
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
t.with_operations operations
(t.with_operation_state operation_state mempool)
end.
Definition add_operation (op_staroptstar : option bool)
: option conflict_handler → Validate.info → t →
Operation_hash.t × Alpha_context.packed_operation →
Pervasives.result (t × add_result) add_error :=
let check_signature :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ true
end in
fun (conflict_handler : option conflict_handler) ⇒
fun (info_value : Validate.info) ⇒
fun (mempool : t) ⇒
fun (function_parameter :
Operation_hash.t × Alpha_context.packed_operation) ⇒
let '(oph, packed_op) := function_parameter in
let '{|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} := packed_op in
let operation :=
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
let validate_result :=
Validate.check_operation (Some check_signature) info_value operation
in
match validate_result with
| Pervasives.Error err ⇒ Pervasives.Error (Validation_error err)
| Pervasives.Ok _ ⇒
match
Validate.check_operation_conflict mempool.(t.operation_state) oph
operation with
| Pervasives.Ok _ ⇒
let operation_state :=
Validate.add_valid_operation mempool.(t.operation_state) oph
operation in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) oph packed_op
mempool.(t.operations) in
let result_value := Added in
Pervasives.Ok
((t.with_operations operations
(t.with_operation_state operation_state mempool)),
result_value)
|
Pervasives.Error
((Validate_errors.Operation_conflict {|
Validate_errors.operation_conflict.Operation_conflict.existing := existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= new_oph
|}) as x_value) ⇒
match conflict_handler with
| Some handler_value ⇒
let new_operation := (new_oph, packed_op) in
let existing_operation :=
match
Operation_hash.Map.(S.INDEXES_MAP.find_opt) existing
mempool.(t.operations) with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Operation_hash.t × Alpha_context.packed_operation)
false
| Some op ⇒ (existing, op)
end in
match handler_value existing_operation new_operation with
| Keep ⇒ Pervasives.Ok (mempool, Unchanged)
| Replace ⇒
let mempool := remove_operation mempool existing in
let operation_state :=
Validate.add_valid_operation mempool.(t.operation_state)
new_oph operation in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) oph packed_op
mempool.(t.operations) in
Pervasives.Ok
((t.with_operations operations
(t.with_operation_state operation_state mempool)),
(Replaced {| add_result.Replaced.removed := existing; |}))
end
| None ⇒ Pervasives.Error (Add_conflict x_value)
end
end
end.
Module Add_replace_or_nothing.
Inductive t : Set :=
| Add_new : t
| Replace : Operation_list_hash.elt → t
| Do_nothing : t.
End Add_replace_or_nothing.
Definition merge
(conflict_handler : option conflict_handler) (existing_mempool : t)
(new_mempool : t) : Pervasives.result t merge_error :=
if
Block_hash.op_ltgt existing_mempool.(t.predecessor_hash)
new_mempool.(t.predecessor_hash)
then
Pervasives.Error Incompatible_mempool
else
let unique_new_operations :=
Operation_hash.Map.(S.INDEXES_MAP.merge)
(fun (function_parameter : Operation_hash.t) ⇒
let '_ := function_parameter in
fun (l_value : option Alpha_context.packed_operation) ⇒
fun (r_value : option Alpha_context.packed_operation) ⇒
match (l_value, r_value) with
| (None, Some r_value) ⇒ Some r_value
| (Some _, None) ⇒ None
| (Some _, Some _) ⇒ None
| (None, None) ⇒ None
end) existing_mempool.(t.operations) new_mempool.(t.operations) in
let unopt_assert {A : Set} (function_parameter : option A) : A :=
match function_parameter with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert _ false
| Some o_value ⇒ o_value
end in
let handle_conflict
(new_operation_content : Alpha_context.packed_operation)
(conflict : Pervasives.result unit Validate_errors.operation_conflict)
: Pervasives.result Add_replace_or_nothing.t merge_error :=
match (conflict, conflict_handler) with
| (Pervasives.Ok _, _) ⇒ Pervasives.Ok Add_replace_or_nothing.Add_new
| (Pervasives.Error conflict, None) ⇒
Pervasives.Error (Merge_conflict conflict)
|
(Pervasives.Error
(Validate_errors.Operation_conflict {|
Validate_errors.operation_conflict.Operation_conflict.existing := existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= new_operation
|}), Some f_value) ⇒
let existing_operation_content :=
unopt_assert
(Operation_hash.Map.(S.INDEXES_MAP.find_opt) existing
existing_mempool.(t.operations)) in
match
f_value (existing, existing_operation_content)
(new_operation, new_operation_content) with
| Keep ⇒ Pervasives.Ok Add_replace_or_nothing.Do_nothing
| Replace ⇒ Pervasives.Ok (Add_replace_or_nothing.Replace existing)
end
end in
Operation_hash.Map.(S.INDEXES_MAP.fold_e)
(fun (roph : Operation_hash.t) ⇒
fun (packed_right_op : Alpha_context.packed_operation) ⇒
fun (mempool_acc : t) ⇒
let '{|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} := packed_right_op in
let right_op :=
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
let? conflict :=
handle_conflict packed_right_op
(Validate.check_operation_conflict
mempool_acc.(t.operation_state) roph right_op) in
match conflict with
| Add_replace_or_nothing.Do_nothing ⇒ return? mempool_acc
| Add_replace_or_nothing.Add_new ⇒
let operation_state :=
Validate.add_valid_operation mempool_acc.(t.operation_state)
roph right_op in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) roph packed_right_op
mempool_acc.(t.operations) in
return?
(t.with_operations operations
(t.with_operation_state operation_state mempool_acc))
| Add_replace_or_nothing.Replace loph ⇒
let mempool_acc := remove_operation mempool_acc loph in
let operation_state :=
Validate.add_valid_operation mempool_acc.(t.operation_state)
roph right_op in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) roph packed_right_op
mempool_acc.(t.operations) in
return?
(t.with_operations operations
(t.with_operation_state operation_state mempool_acc))
end) unique_new_operations existing_mempool.
Definition operations (mempool : t)
: Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation :=
mempool.(t.operations).
Module add_result.
Module Replaced.
Record record {removed : Set} : Set := Build {
removed : removed;
}.
Arguments record : clear implicits.
Definition with_removed {t_removed} removed (r : record t_removed) :=
Build t_removed removed.
End Replaced.
Definition Replaced_skeleton := Replaced.record.
End add_result.
End ConstructorRecords_add_result.
Import ConstructorRecords_add_result.
Reserved Notation "'add_result.Replaced".
Inductive add_result : Set :=
| Added : add_result
| Replaced : 'add_result.Replaced → add_result
| Unchanged : add_result
where "'add_result.Replaced" := (add_result.Replaced_skeleton Operation_hash.t).
Module add_result.
Include ConstructorRecords_add_result.add_result.
Definition Replaced := 'add_result.Replaced.
End add_result.
Definition operation_conflict : Set := Validate_errors.operation_conflict.
Inductive add_error : Set :=
| Validation_error : Error_monad.trace Error_monad._error → add_error
| Add_conflict : operation_conflict → add_error.
Inductive merge_error : Set :=
| Incompatible_mempool : merge_error
| Merge_conflict : operation_conflict → merge_error.
Definition encoding : Data_encoding.t t :=
Data_encoding.def "mempool" None None
(Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state;
t.operations := operations
|} := function_parameter in
(predecessor_hash, operation_state, operations))
(fun (function_parameter :
Block_hash.t × Validate.operation_conflict_state ×
Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation)
⇒
let '(predecessor_hash, operation_state, operations) :=
function_parameter in
{| t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state; t.operations := operations; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "predecessor_hash" Block_hash.encoding)
(Data_encoding.req None None "operation_state"
Validate.operation_conflict_state_encoding)
(Data_encoding.req None None "operations"
(Operation_hash.Map.(S.INDEXES_MAP.encoding)
(Data_encoding.dynamic_size (Some (Variant.Build "Uint30" unit tt))
Alpha_context.Operation.encoding))))).
Definition init_value
(ctxt : Alpha_context.context) (chain_id : Chain_id.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) (predecessor_hash : Block_hash.t)
(grandparent_round : Alpha_context.Round.t) : validation_info × t :=
let '{|
Validate.validation_state.info := info_value;
Validate.validation_state.operation_state := operation_state
|} :=
Validate.begin_partial_construction ctxt chain_id predecessor_level
predecessor_round grandparent_round in
(info_value,
{| t.predecessor_hash := predecessor_hash;
t.operation_state := operation_state;
t.operations := Operation_hash.Map.(S.INDEXES_MAP.empty); |}).
Inductive keep_or_replace : Set :=
| Keep : keep_or_replace
| Replace : keep_or_replace.
Definition conflict_handler : Set :=
Operation_hash.t × Alpha_context.packed_operation →
Operation_hash.t × Alpha_context.packed_operation → keep_or_replace.
Definition remove_operation (mempool : t) (oph : Operation_hash.t) : t :=
match Operation_hash.Map.(S.INDEXES_MAP.find_opt) oph mempool.(t.operations)
with
| None ⇒ mempool
|
Some {|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} ⇒
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.remove) oph mempool.(t.operations) in
let operation_state :=
Validate.remove_operation mempool.(t.operation_state)
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
t.with_operations operations
(t.with_operation_state operation_state mempool)
end.
Definition add_operation (op_staroptstar : option bool)
: option conflict_handler → Validate.info → t →
Operation_hash.t × Alpha_context.packed_operation →
Pervasives.result (t × add_result) add_error :=
let check_signature :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ true
end in
fun (conflict_handler : option conflict_handler) ⇒
fun (info_value : Validate.info) ⇒
fun (mempool : t) ⇒
fun (function_parameter :
Operation_hash.t × Alpha_context.packed_operation) ⇒
let '(oph, packed_op) := function_parameter in
let '{|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} := packed_op in
let operation :=
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
let validate_result :=
Validate.check_operation (Some check_signature) info_value operation
in
match validate_result with
| Pervasives.Error err ⇒ Pervasives.Error (Validation_error err)
| Pervasives.Ok _ ⇒
match
Validate.check_operation_conflict mempool.(t.operation_state) oph
operation with
| Pervasives.Ok _ ⇒
let operation_state :=
Validate.add_valid_operation mempool.(t.operation_state) oph
operation in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) oph packed_op
mempool.(t.operations) in
let result_value := Added in
Pervasives.Ok
((t.with_operations operations
(t.with_operation_state operation_state mempool)),
result_value)
|
Pervasives.Error
((Validate_errors.Operation_conflict {|
Validate_errors.operation_conflict.Operation_conflict.existing := existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= new_oph
|}) as x_value) ⇒
match conflict_handler with
| Some handler_value ⇒
let new_operation := (new_oph, packed_op) in
let existing_operation :=
match
Operation_hash.Map.(S.INDEXES_MAP.find_opt) existing
mempool.(t.operations) with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (Operation_hash.t × Alpha_context.packed_operation)
false
| Some op ⇒ (existing, op)
end in
match handler_value existing_operation new_operation with
| Keep ⇒ Pervasives.Ok (mempool, Unchanged)
| Replace ⇒
let mempool := remove_operation mempool existing in
let operation_state :=
Validate.add_valid_operation mempool.(t.operation_state)
new_oph operation in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) oph packed_op
mempool.(t.operations) in
Pervasives.Ok
((t.with_operations operations
(t.with_operation_state operation_state mempool)),
(Replaced {| add_result.Replaced.removed := existing; |}))
end
| None ⇒ Pervasives.Error (Add_conflict x_value)
end
end
end.
Module Add_replace_or_nothing.
Inductive t : Set :=
| Add_new : t
| Replace : Operation_list_hash.elt → t
| Do_nothing : t.
End Add_replace_or_nothing.
Definition merge
(conflict_handler : option conflict_handler) (existing_mempool : t)
(new_mempool : t) : Pervasives.result t merge_error :=
if
Block_hash.op_ltgt existing_mempool.(t.predecessor_hash)
new_mempool.(t.predecessor_hash)
then
Pervasives.Error Incompatible_mempool
else
let unique_new_operations :=
Operation_hash.Map.(S.INDEXES_MAP.merge)
(fun (function_parameter : Operation_hash.t) ⇒
let '_ := function_parameter in
fun (l_value : option Alpha_context.packed_operation) ⇒
fun (r_value : option Alpha_context.packed_operation) ⇒
match (l_value, r_value) with
| (None, Some r_value) ⇒ Some r_value
| (Some _, None) ⇒ None
| (Some _, Some _) ⇒ None
| (None, None) ⇒ None
end) existing_mempool.(t.operations) new_mempool.(t.operations) in
let unopt_assert {A : Set} (function_parameter : option A) : A :=
match function_parameter with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert _ false
| Some o_value ⇒ o_value
end in
let handle_conflict
(new_operation_content : Alpha_context.packed_operation)
(conflict : Pervasives.result unit Validate_errors.operation_conflict)
: Pervasives.result Add_replace_or_nothing.t merge_error :=
match (conflict, conflict_handler) with
| (Pervasives.Ok _, _) ⇒ Pervasives.Ok Add_replace_or_nothing.Add_new
| (Pervasives.Error conflict, None) ⇒
Pervasives.Error (Merge_conflict conflict)
|
(Pervasives.Error
(Validate_errors.Operation_conflict {|
Validate_errors.operation_conflict.Operation_conflict.existing := existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= new_operation
|}), Some f_value) ⇒
let existing_operation_content :=
unopt_assert
(Operation_hash.Map.(S.INDEXES_MAP.find_opt) existing
existing_mempool.(t.operations)) in
match
f_value (existing, existing_operation_content)
(new_operation, new_operation_content) with
| Keep ⇒ Pervasives.Ok Add_replace_or_nothing.Do_nothing
| Replace ⇒ Pervasives.Ok (Add_replace_or_nothing.Replace existing)
end
end in
Operation_hash.Map.(S.INDEXES_MAP.fold_e)
(fun (roph : Operation_hash.t) ⇒
fun (packed_right_op : Alpha_context.packed_operation) ⇒
fun (mempool_acc : t) ⇒
let '{|
Alpha_context.packed_operation.shell := shell;
Alpha_context.packed_operation.protocol_data :=
Alpha_context.Operation_data protocol_data
|} := packed_right_op in
let right_op :=
{| Alpha_context.operation.shell := shell;
Alpha_context.operation.protocol_data := protocol_data; |} in
let? conflict :=
handle_conflict packed_right_op
(Validate.check_operation_conflict
mempool_acc.(t.operation_state) roph right_op) in
match conflict with
| Add_replace_or_nothing.Do_nothing ⇒ return? mempool_acc
| Add_replace_or_nothing.Add_new ⇒
let operation_state :=
Validate.add_valid_operation mempool_acc.(t.operation_state)
roph right_op in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) roph packed_right_op
mempool_acc.(t.operations) in
return?
(t.with_operations operations
(t.with_operation_state operation_state mempool_acc))
| Add_replace_or_nothing.Replace loph ⇒
let mempool_acc := remove_operation mempool_acc loph in
let operation_state :=
Validate.add_valid_operation mempool_acc.(t.operation_state)
roph right_op in
let operations :=
Operation_hash.Map.(S.INDEXES_MAP.add) roph packed_right_op
mempool_acc.(t.operations) in
return?
(t.with_operations operations
(t.with_operation_state operation_state mempool_acc))
end) unique_new_operations existing_mempool.
Definition operations (mempool : t)
: Operation_hash.Map.(S.INDEXES_MAP.t) Alpha_context.packed_operation :=
mempool.(t.operations).