Changelog

Gitlab

We list here, week by week, the important properties we have verified.

2022-06-27 - 2022-07-01

Michelson

• MR 524: start work on dep_parse_instr_aux address Issue 215

2022-06-21 - 2022-06-25

Michelson

• MR 612: Simulation dep_parse_view_returning closes Issue 216
• MR 562: Add partial proof for dep_extract_lazy_storage_updates related to Issue 141
• MR 609: add simulation for dep_parse_view_name, dep_parse_contract and dep_parse_returning. In Script_ir_translator.v related to Issue 138
• MR 600 Add simulation definition for dep_well_formed_entrypoints in Script_ir_translator.v related to Issue 214
• MR 604 Add simulation definition for dep_record_trace_eval and proof it's equality in [Gas_monad.v]

coq-of-ocaml

• MR 603 Related to Issue 211, translate files that were in the black-list before, namely:
  • Sc_rollups.v
  • Sc_rollup_arith.v
  • Sc_rollup_game.v
  • Tx_rollup_l2_apply.v
  • Tx_rollup_l2_batch.v
  • Tx_rollup_l2_context.v
  • Tx_rollup_l2_verifier.v

2022-06-13 - 2022-06-17

Michelson

• MR 594 Add simulation definition for dep_diff_of_big_map in Script_ir_translator.v related to Issue 140
• MR 592 Add simulation proof for dep_big_map_get_and_update in Script_ir_translator.v related to Issue 140
• MR 548: More cases for the simulation of the Michelson interpreter in Script_interpreter.v, related to the Issue 117
• MR 587 correct termination and definitions for cases map, big_map and set for simulation of parse_data_aux in Script_ir_translator.v related to Issue 138
• MR 586 Add simulation proof for dep_big_map_update in Script_ir_translator.v related to Issue 140
• MR 589 Proof of dep_extract_lazy_storage_diff_eq, related to Issue 141
• MR 582 Proof of dep_merge_branches_eq, related to Issue 135
• MR 583 Add simulation proof for dep_big_map_update_by_hash in Script_ir_translator.v related to Issue 140
• MR 570 Add the proof dep_collect_lazy_storage_eq related to Issue 141.
• MR 581 Add proof for dep_parse_toplevel_aux related to Issue 138
• MR 573 Add simulation big_map_get related to Issue 140
• MR 577 Encodings, Liquidity_baking_repr.v closes Issue 100.
• MR 576 Verify dep_comparable_ty_eq_eq in Script_ir_translator.v

2022-06-06 - 2022-06-10

Michelson

• MR 560 Encodings, closes Issue 101, closes Issue 102, Closes Issue 103.
• MR 572: add proof for dep_stack_eq_eq, related to Issue 135
• MR 564: add simulation of merge_branches, related to Issue 135
• MR 515 Verify the simulations in Script_set.v closing the Issue 161
• MR 571 Add proofs for simulations : dep_parse_contract_aux_eq, dep_parse_contract_for_script_eq dep_typecheck_views Issue 138.
• MR 566 Add simulation of dep_parse_contract_aux related to Issue 138.
• MR 569 Add proofs for simulations : dep_parse_instr_eq Issue 141.
• MR 568 Added proofs in String.v
• MR 563 Add simulation of dep_big_map_get_by_hash related to Issue 140
• MR 561 Add proofs for simulations : dep_parse_toplevel_eq, dep_parse_contract_eq, dep_parse_data_eq Issue 141.
• MR 559 Encodings Issue 96 Issue 97.
• MR 552 Add simulation of dep_parse_contract_for_script related to Issue 138.
• MR 549 Finish the proof of dep_fold_lazy_storage_eq related to Issue 141.
• MR 546 related to Issue 136: Add simulations definition and proof for dep_parse_storage and dep_parse_code.
• MR 531 related to Issue 136: Add simulations dep_find_entrypoint and dep_find_entrypoint_for_type.
• MR 553 Add simulation of dep_parse_view_returning, dep_typecheck_views, dep_parse_returning, dep_parse_toplevel_aux related to Issue 138.

Tests

• MR 554: verify the domain of the generators in Test_tez_repr.v
• MR 526: add a translation to Coq and a few proofs for the property-based tests in Test_tez_repr.v

Others

• MR 558: add blog post about property based tests in Coq

2022-05-30 - 2022-06-03

Michelson

• MR 547 related to Issue 139: dep_typecheck_code_inner_eq proof in Script_ir_translator.v.
• MR 542: simulations for code_size in Script_ir_translator.v
• MR 545: simulations for empty_big_map and big_map_mem in Script_ir_translator.v
• MR 544 related to Issue 139: dep_parse_script_eq proof in Script_ir_translator.v.
• MR 532: Partial proof script of dep_fold_lazy_storage_eq.
• MR 537: simulations of smart consturctions in Script_typed_ir.v
• MR 535: state all the simulation lemmas (without proofs) in Script_ir_translator.v
• MR 534: state a few more simulation lemmas (without proofs) in Script_ir_translator.v
• MR 513 related to Issue 141: Add simulations definitions dep_extract_lazy_storage_diff
• MR 533 related to Issue 137: Add simulation proof dep_make_comb_set_proof_argument_eq
• MR 469 related to Issue 136: Add simulations definition and proof for dep_check_packable and axioms for dep_parse_storage_ty_eq.

Others

• MR 543: add blog post about the proof plan for backward compatibility

2022-05-23 - 2022-05-27

Michelson

• MR 520 related to Issue 170: validity predicate is done
• MR 509 related to Issue 162: verifying all the simulations in Script_map
• MR 507 related to Issue 162: beginning of the verification of the simulations in Script_map
• MR 493 related to Isse 141: Add simulations definitions dep_fold_lazy_storage and dep_collect_lazy_storage
• MR 519 related to Isse 141: Add simulations definitions dep_unparse_data and dep_unparse_code.

2022-05-16 - 2022-05-22

Others

• MR 495, closes Issue 164: adds links to the simulations.

Skip-lists

• MR 488 in Proofs/Skip-list-repr.v: verify the Skip-list.

Michelson

• MR 494 in Proofs/Script_ir_translator.v and others, addresses Issue 139: amonth others add the following simulation definitions:
  • dep_unparse_contract
  • fuel_to_stack_depth
  • dep_parse_storage_ty
  • dep_typecheck_views
  • dep_parse_returning
  • dep_parse_contract_aux
  • dep_parse_toplevel_aux
  • dep_comb_witness2
  • dep_unparse_data_aux_fuel
  • dep_unparse_code_aux_fuel
  • dep_unparse_items_fuel
  • dep_unparse_data_aux
  • dep_unparse_code_aux
  • dep_unparse_items
  • dep_parse_and_unparse_script_unaccounted
  • dep_pack_data_with_mode
  • dep_hash_data
  • dep_pack_data
  • dep_is_comparable
  • dep_pair_t
  • dep_pair_key
  • dep_pair_3_key
  • dep_option_t And the following proofs :
  • stack_depth_to_fuel_to_stack_depth
  • dep_comb_witness2_eq
  • dep_unparse_data_aux_fuel_eq
  • dep_unparse_code_aux_fuel_eq
  • dep_unparse_items_fuel_eq
  • dep_unparse_data_aux_eq
  • dep_unparse_code_aux_eq
  • dep_unparse_items_eq
  • dep_pack_data_with_mode_eq
  • dep_hash_data_eq
  • dep_check_eq_eq
  • dep_is_comparable_eq
  • dep_pair_t_eq
  • dep_pair_key_eq
  • dep_pair_3_key_eq
  • dep_option_t_eq
  • dep_list_operation_t_eq
• MR 489 in Proofs/Script_ir_translator.v: verify the following simulations:
  • dep_parse_comparable_ty
  • dep_parse_big_map_value_ty
  • dep_parse_packable_ty
  • dep_parse_passable_ty
  • dep_parse_any_ty
  • dep_parse_ty
  • dep_parse_parameter_ty_and_entrypoints
  • dep_get_single_sapling_state
  • dep_script_size
  • dep_typecheck_code
• MR 492 in Proofs/Script_ir_translator.v: add proof for dep_comb_witness1_eq and dep_parse_comparable_data_eq. Addresses Issue 137.
• MR 463 in Script_ir_translator.v: add simulations, and proofs for
• dep_comparable_ty_of_ty_eq
• dep_pack_comparable_data_eq
• dep_hash_comparable_data_eq

Data_encoding

• MR 467 in Lazy_storag_diff.v: add proof for diff_encoding while axiomating item_encoding because of the use of GADTs.

Map

• MR 482 in Map.v: verify various properties of list-based Map implementation.
• MR 490 in Carbonated_map.v: verify various properties of the carbonated maps.

2022-05-09 - 2022-05-15

Data_encoding

• MR 478 in Apply.v: adds proof for denunciation_kind_encoding.

Tests

• MR 485in Test_bitset.v: verify the property-based tests of test_bitset.ml

2022-05-2 - 2022-05-08

Michelson

• MR 471 in Script_ir_translator.v: add simulations, and proofs for dep_stack_eq_eq, dep_has_lazy_storage_value_eq.
• MR 465 in Script_ir_translator.v: add simulations, and proofs for dep_check_dupable_comparable_ty_eq, dep_check_dupable_ty_eq, dep_default_ty_eq_error_eq, dep_comparable_ty_eq_eq, dep_ty_eq_eq.
• MR 436 in Script_typed_ir.v: have two different implementations for the Set of values in the OCaml and dependent version of the Michelson interpreter. Use that to define the simulation of the IExec instruction.

Compare

• MR 474, in Proofs/Script_comparable.v, one more (small) proof for validity of comparison functions.
• MR 468, many files affected: validity of compare functions. The most part of needed work on issue 79.
• MR 464 in Environment/Proofs/Compare.v: create automated tactic for solve validity of compare functions. Resolves issue 72.
• MR 462 in Script_comparable.v: Add equality proof for compare_comparable_eq

Data_encoding

• MR 451 in Storage.v

Skip-list

• MR 472 in Skip_list_repr.v: verification of the equal function

Reports

• MR 470 in [Reports/exceptions.md](Storage.v

2022-04-25 - 2022-05-01

Michelson

• MR 452 in Script_ir_translator.v: add simulations of close_descr, kinfo_of_descr and compose_descr
• MR 450: in Status/Simulations add a list of dependent simulations to write, mainly for the translator of Michelson for now

Compare

• MR 448]: in scripts/list_compare_functions.rb add a generated Markdown file to list the verified compare functions

Data_encoding

• MR 460 in Tx_rollup_l2_context_sig resolves issue 111: signature_encoding
• MR 459 in Script_typed_ir resolves issue 108: Encodings in Script_typed_ir
• MR 444 in Tx_rollup_commitment_repr
• MR 430 in Data_encoding: Specify Compact encoding

Others

• MR 454: Errors and Assertions report
• MR 438: Skip-list-repr validity. Back_pointer and back_pointers lemmas proved
• MR 447: in Proofs/Tx_rollup_commitment_repr.v, simple proofs of [*.compare_is_valid] lemmas. Resolves issue 77
• MR 433: in Proofs/Receipt_repr.v, proof for compare_balance_is_valid which resolves issue 74
• MR 442; add specification for Tx_rollup_l2_qty.v
• MR 434: Add encoding proof to Tx_rollup_state_repr.v which resolves issue 113
• MR 429: Verify the Commitment encoding in Sc_rollup_repr.v.
• MR 441: Partially remove the warnings from the proofs which resolves issue 113. The cases left is describred in issue 133
• MR 445: Proof encodings for Sc_rollup_tick_repr.v issue 107
• MR 456: Proof encodings for Alpha_context.v issue 92

2022-04-18 - 2022-04-24

Michelson

• MR 431 in Script_interpreter.v: Beginning of proof for cases with loops in the equality of our interpreter with dependent types
• MR 422 in Micho_to_dep.v: Begin proof of seq_instr_compose
• MR 424 in Script_interpreter.v: Add more definitions for dep_step
• MR 417 in Script_ir_translator.v: dep_unparse_comparable_data and proof that it equals to unparse_comparable_data

Others

• MR 435: Skip-list-repr validity. 4 lemmas proved. 6 lemmas defined.
• MR 432: Fallback_Array definitions
• MR 416: upgrade Coq from version 8.13 to 8.14
• MR 427 in Destination_repr.v: Verify that the compare function is valid
• MR 425 in Bitset.v: Prove add_is_valid and mem_add_eq

2022-04-11 - 2022-04-17

Michelson

• MR 409 in Script_interpreter.v: 80% of the cases (the simplest ones) for the equality of our dependently typed interpreter
• MR 408 in Script_interpreter.v: beginning of equality proof between the OCaml Michelson interpreter with GADTs and our dependently typed version

Tests

• MR 407 in the Tests folder: add a generated version of https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/pbt/test_sc_rollup_tick_repr.ml and factorize the test definitions

Others

• MR 418 in Bitset.v: add specification of bitsets
• MR 410 in Bond_id_repr.v: verify the specification of this file
• MR 406 in Lazy_storage_kind.v: verify the encodings
• MR 423: Adds script to display the encoding lemmas in src/Proto_alpha/encoding.md

2022-04-04 - 2022-04-10

• MR 405 in Simulations/Script_ir_translator.v about 6 percent (about 330 of 4946 lines) of dep_parse_data_aux is defined, Proofs/Script_ir_translator.v a couple of small proofs of aux lemmas.
• MR 401 in Script_ir_translator.v dep_parse_comparable_data dep_comparable_comb_witness1 are defined (no proofs yet)
• MR 395 in Carbonated_map.v: specification of the carbonated maps (but no proofs)
• MR 394 in Script_ir_translator.v: Proved that comparable_ty_of_ty and ty_of_comparable_ty are compatible (2 reciprocal Fixpoints created and proved), ty and comparable_ty are the same type (one of corresponding properties proved):
  • Fixpoint ty_of_comparable_ty_comparable_ty_of_ty
  • Fixpoint comparable_ty_of_ty_ty_of_comparable_ty
  • Lemma ty_of_comparable_ty_eq
• MR 393 in Skip_list_repr.v: add a specification of skip lists (the verification itself is a todo)
• MR 383 in Script_ir_translator.v: fix the proof parse_ty_aux_dep_parse_ty_aux_eq due to a Michelson update in OCaml
• MR 386 in Saturation_repr_generated.v: add a beginning of translation of the property-based tests using coq-of-ocaml
• MR 369 in Script_ir_translator.v: fix the following Coq proofs, due to a Michelson update in OCaml:
  • dep_ty_of_comparable_ty_eq
  • dep_unparse_comparable_ty_eq
  • dep_unparse_ty_eq
• MR 397 in Micho_to_dep.v: Begin correctness proofs for micho-coq's instructions and instruction sequences. Define function to sequence two kinstr's.