Verify Script_typed_ir.v
Verify the validity, and hence the absence of internal errors, for the file https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/script_typed_ir/ . You can first make a merge request to axiomatize all the expected properties. If you need validity properties in other files, you can axiomatize them. An example of validity proofs is in https://formal-land.gitlab.io/coq-tezos-of-ocaml/docs/proto_alpha/proofs/apply/
-
of_int -
compound1 -
compound2 -
pair_t -
pair_3_t -
comparable_pair_t -
comparable_pair_3_t -
union_t -
comparable_union_t -
lambda_t -
option_t -
comparable_option_t -
list_t -
set_t -
map_t -
big_map_t -
contract_t -
ticket_t
Edited by Evan Marzion