Translator simulations 50-59
Write the simulation definitions and proofs for the cases 50-59 in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/status/simulations
Simulations
-
dep_parse_data_aux - partially defined - huge -
dep_parse_view_returning - @kewersonhugo -
dep_typecheck_views -
dep_parse_instr_aux -
dep_parse_toplevel_aux -
dep_parse_returning -
dep_parse_contract_aux -
dep_parse_contract_for_script @dhilst (MR !552 (merged)) -
dep_code_size (MR !542 (merged)) -
dep_parse_code - @kewersonhugo (MR !546 (merged)) -
dep_parse_storage - @kewersonhugo (MR !546 (merged))
Proofs
-
dep_parse_data_aux_eq -
dep_parse_view_returning_eq -
dep_typecheck_views_eq -
dep_parse_instr_aux_eq -
dep_parse_toplevel_aux_eq -
dep_parse_returning_eq -
dep_parse_contract_aux_eq -
dep_parse_contract_for_script_eq -
dep_code_size_eq (MR !542 (merged)) -
dep_parse_code_eq -
dep_parse_storage_eq
Edited by Kewerson Hugo