Skip to main content

Changelog

Gitlab

We list here, week by week, the important properties we have verified. You can click on the various links to get more details. If you have a request for a feature of the protocol you want to get verified, you can open an issue on coq-tezos-of-ocaml/-/issues or contact us ✍️.

2022-12-12 - 2022-12-16

Sc_rollups

2022-12-12 - 2022-12-16

Others

Mi-Cho-Coq Compatibility

Verify Rollups

  • MR 1006: Verify Rollup related files, in particular Sc_rollup_inbox_message_repr.v (wip) and Sc_rollup_inbox_message_repr.v (wip). Addresses Issue 743 and Issue 734.

2022-12-05 - 2022-12-09

Others

  • MR 1000: Verify Sc_rollup_refutation.v, part 3. Part of Issue #713
  • MR 995: Begin work on verifying Raw_context.v, part of Issue #556
  • MR 994: Unblacklisting the dependencies of [Apply.v].
  • MR 983: update current version of proto_alpha. Fix proofs.

Mi-Cho-Coq Compatibility

2022-11-28 - 2022-12-02

Others

Michelson

  • Adding the lastest cases for the value validity predicate (Map_value and Big_map_value) (closes Issue #697: define kinstr and values)
  • Adding some changes related to Issue #700: Update the remaining proofs files Script_....v.
  • MR 986: Compatibility of parse_ty and unparse_ty functions in Script_ir_translator.v (related to Issue #701: Verify the validity of some functions in Script_ir_translator.v)

2022-11-21 - 2022-11-25

Michelson

Others

  • MR 979: Unblacklist some files (related to the simulations removal).
  • MR 981: New comparability and validity predicates for [Script_typed_ir] and projection onto [Ty.t].

2022-11-14 - 2022-11-18

Michelson

Others

2022-11-07 - 2022-11-11

Internal Errors

Others

  • MR 965: Draft for verification of Mempool_validation, addresses Issue 705.
  • MR 948: Simulations and Proofs : initial upgrade for the new version of protocol.
  • MR 955: Initial fix the definition of [dep_step_eq]. Addresses Issue 691.
  • MR 954: Fix the definition of [dep_step]. Changing [ty_to_dep_Set Ty.Operation] to return [With_family.operation] instead of [Script_typed_ir.operation]. Addresses Issue 691.
  • MR 950: Initial attempt to implement LamRec. Simplify definition of dep_make_transaction_to_tx_rollup. Chaning types in some definitions. Addresses Issue 691.
  • MR 946: bodies for the definitions for the Simulations/Script_interpreter_defs.v except LamRec cases (2 such cases are missing). Addresses Issue 691.
  • MR 963: verify Ticket_receipt_repr.v. Closes Issue 707.
  • MR 962: unblacklist Apply.v for the new version of the protocol.

Michelson

2022-10-31 - 2022-11-04

Internal Errors

Others

  • MR 941: Proto_alpha/Simulatins/Script_interpreter_defs.v axiomatization for the most of original definitions.
  • MR 945: /Environment/V7/Proofs/List.v auxiliary lemma [filter_preserves_prop]. Related to Issue 639

2022-10-24 - 2022-10-28

Internal Errors

  • MR 907: Verify Baking.v, closes Issue 473
  • MR 904: closes Issue 490
  • MR 910: Verify Validation, part 1 Issue 674
  • MR 902: closes Issue 682
  • MR 892: addresses Issue 430
  • MR 901: verify the internal errors for Ticket_costs.v and Ticket_scanner.v
  • MR 908: verify the internal errors for Ticket_balance_key.v and Ticket_hash_builder.v
  • MR 909: verify the internal errors for Ticket_token_map.v
  • MR 906: Specify Script_map.v
  • MR 903: Admitted Definitions in Token.v Issue 639
  • MR 912: Begin verification of Tx_rollup_ticket.v
  • MR 913: Verification of the Ticket_operations_diff.v file
  • MR 920: finishing the verification of ticket files for internal errors
  • MR 914: Begin verification of Script_ir_unparser for the absence of internal errors. Addresses the Issue 601.
  • MR 919: Begin verification of Sc_rollup_inbox_repr for the absence of internal errors. Addresses the Issue 576.
  • MR 921: Specification of Sc_rollup_commitment_storage.v, Verify Sc_rollup_inbox_storage.v, Verify Sc_rollup_outbox_storage.v, Verify Sc_rollup_refutation_storage.v, and Verify Sc_rollup_stake_storage.v
  • MR 922: Specification of Dal_slot_storage.v, Delegate_activation_storage.v, Delegate_slashed_deposits_storage.v, Delegate_storage.v, Init_storage.v, and Liquidity_baking_storage.v
  • MR 918: Verify parse_ticket

Michelson

  • MR 902: Support proofs in Proto_alpha : [Simulations/Script_big_map][Proofs/Script_big_map]

2022-10-17 - 2022-10-21

Internal Errors

  • MR 893: Verify Amendment, addresses Issue 688
  • MR 898: addresses Issue 473, Issue 618
  • MR 877: Verify Apply.ex_ticket_size
  • MR 879: Verification of Level_repr.v (adresses issue 532)
  • MR 881: Progress towards the verification of Apply.apply_transaction_to_tx_rollup
  • MR 884: Finish the verification of Apply.apply_transaction_to_tx_rollup
  • MR 886: Verify Script_string.v
  • MR 894: Verify Baking.v
  • MR 896: Specify Voting_period_storage.v, Vote_storage.v and Zk_rollup_storage.v
  • MR 897: Specify Constants_storage.v, Fees_storage.v, Global_constants_storage.v, Level_storage.v, Nonce_storage.v, Tx_rollup_reveal_storage.v and Tx_rollup_storage.v
  • MR 865: Show the absence of internal errors for Seed_storage.for_cycle . Closes Issue 425
  • MR 899: Specify Bootstrap_storage.v, Commitment_storage.v, Contract_delegate_storage.v, Contract_manager_storage.v, Contract_storage.v, Delegate_missed_endorsements_storage.v and Frozen_deposits_storage.v
  • MR 900: Specify Sc_rollup_storage.v, Ticket_storage.v, Tx_rollup_commitment_storage.v and Tx_rollup_inbox_storage.v

Michelson

Miscellaneous

  • MR 866: Add convenient record update syntax
  • MR 888: Disable the compilation of the protocol J in our CI

Blog

  • MR 886: Add post about the verification of internal errors

2022-10-10 - 2022-10-14

Internal Errors

  • MR 859: closes Issue 418 Issue 419 Issue 420, related to Issue 416
  • MR 856: have a validity predicate for the simulation of Raw_context.t
  • MR 863: Add a few more definitions to the error monad in the environment
  • MR 864: Use the notation letP? to also check that there are no internal errors
  • MR 867: Progress towards the verification of Main.finalize_block
  • MR 868: Verification of Validate.finalize_block
  • MR 873: Add axioms about internal errors in Apply.v
  • MR 869: Verification of Apply.finalize_block
  • MR 857: Creating dedicated folder for proofs of internal error absense
  • MR 852: Beginning proofs that Main.v is free of internal errors

Translation

  • MR 854: translating more axiomatized definitions from proto_alpha to Coq

Storage

  • MR 846: Add tool to generate the storage specification, part 2.
  • MR 855: Add tool to generate the storage specification, part 3.

Michelson

Porting simulations to Proto_alpha

  • MR 861: Define the simulation with the new form of [typed_contract] and ensures retrocompatibility with K. Addresses the Issue 394

Others

  • MR 872: Move generated simulation code from Context.v to Context_generated.v
  • MR 874: Add a new layer to the context simulation

2022-10-03 - 2022-10-07

Michelson

  • MR 837: filling gaps in migration from Proto_K to Proto_alpha, addresses the Issue 392
  • MR 842: solves get_total_voting_power_free_is_backward_compatible from Proto_J_K/Proofs. Addresses the Issue 372
  • MR 824: Addresses the Issue 388

Translation

  • MR 844: translating last OCaml files of proto_alpha to Coq
  • MR 845: use int notations on the translation of proto_alpha

Internal Errors

  • MR 850: removing more asserts from proto_alpha
  • MR 847: Add statements that Main.v is free of internal errors (Issue 390)

Others

Environment

Storage

  • MR 835: Add tool to generate the storage specification, part 1.

2022-09-26 - 2022-09-30

Michelson

  • MR 833: solves get_voting_power_is_backward_compatible and get_total_voting_power from Proto_J_K/Proofs. Addresses the Issue 372

2022-09-19 - 2022-09-23

Michelson

  • MR 814: Verify ISapling_verify_update_deprecated simulation
  • MR 813: Verify IMap_get_and_update and IMap_size simulation

Translation

  • MR 838: Use monadic notations in the translation for the monadic notations used in the protocol with the local let open
  • MR 818: Migrate the environment proofs to V7
  • MR 821: Migrate the simulations, from Proto K to Proto alpha, part 1
  • MR 832: Port migrations of the simulations, from Proto_J_K to Proto_K_alpha (Issue 395) and part 1 of porting migrations from Proto_J_K to Proto_K_alpha (Issue 392)
  • MR 819: Fix proofs in Proto alpha, part 1
  • MR 826: Synchronize the translation of the protocol to the current status of our fork branch
  • MR 828: Fix repr proofs in Proto alpha, part 1. Adresses the Issue 386.
  • MR 822: Fix repr proofs in Proto alpha, part 2. Adresses the Issue 386.

Storage

  • MR 830: Add some experiments for the formalization of the storage system

Others

  • MR 827 : Verify the new repr files in Proto_alpha, closes the Issue 387
  • MR 823: Fix links going back to the OCaml code
  • MR 817: Port migrate function to proto K -> alpha. Related to the the Issue 392

2022-09-12 - 2022-09-16

Michelson

  • MR 816: Verify IPairing_check_bls12_381. Addresses the Issue 372
  • MR 790: Verify big_map cases in Script_interpreter. Closes the Issue 249
  • MR 801: Verify IPack. Addresses the Issue 368
  • MR 804: Completed some admitted lemmas in the instruction backward compatability proofs
  • MR 807: Verify IMap_iter simulation
  • MR 809: Verify ISet_iter simulation
  • MR 811: Verify IMap_get and IMap_update simulation
  • MR 796: Verify IComb, IUncomb, IComb_get, IComb_set, IDup_n` for Proto J and Proto K. Closes the Issue 267

Translation

  • MR 802: Beginning of translation of the current proto_alpha version of the protocol
  • MR 808: More translate files for proto_alpha
  • MR 815: Copy proofs from Proto K and blacklist failing files

Others

  • MR 806: Fix carbonated map proofs
  • MR 812: Move the folders Proto_alpha to Proto_J and Proto_A to Proto_alpha

2022-09-05 - 2022-09-09

Michelson

  • MR 799: Verify ICreate_contract. Closes the Issue 259
  • MR 794: Verify boolean arithmetic instructions. Closes the Issue 254
  • MR 791: Verify arithmetic instructions, Part 1: IIs_nat, IAbs_int, IAdd_nat, IMul_nat. Related to the Issue 253
  • MR 793: Verify division instructions: IEdiv_teznat, IEdiv_tez, IEdiv_int, IEdiv_nat. Related to the Issue 252; also update the definitions for the division instructions
  • MR 750 : Backward compatibility proofs for some (2/14) instructions, closes Issue 363

Translation

  • MR 800: Remove remaining axioms for the translation of the interpreter of protocol K.

2022-08-29 - 2022-09-02

Michelson

  • MR 783 : Verify IMap_map. Closes the Issue 248
  • MR 772 : Backward compatibility proofs for some (11/14). Related to the Issue 372
  • MR 778 : Backward compatibility proofs for some (8/14). Related to the Issue 369
  • MR 771 : Backward compatibility proofs for some (9/14) Part 3. Related to the Issue 370
  • MR 773 : Backward compatibility proofs for some (10/14) instructions with auxiliary lemmas of backward compatibility of auxiliary functions, closes Issue 371
  • MR 776 : Backward compatibility proofs for some (12/14) Part 1. Related to the Issue 373
  • MR 777 : Backward compatibility proofs for some (13/14). Closes to the Issue 374
  • MR 755 : Backward compatibility proofs for some (14/14) Part 1. Related to the Issue 375
  • MR 774 : Backward compatibility proofs for some (14/14) Part 2. Related to the Issue 375
  • MR 789 : Backward compatibility proofs for some (12/14) Closes Issue 373
  • MR 784 : Backward compatibility proofs for some (6/14) instructions and some definitions of migration functions, closes Issue 367
  • MR 792 : Backward compatibility proofs for some remaining instructions.

Translation

  • MR 786: Remove some axioms from the Coq translation of the protocol K.
  • MR 768: Update the Coq translation to the latest versions of proto J and K, fixing Issue 212
  • MR 780: Fix more proofs copied from proto J to proto K

2022-08-22 - 2022-08-26

Michelson

  • MR 764 : Backward compatibility proofs for some (5/14) instructions and some definitions of migration functions, closes Issue 366
  • MR 767 : Backward compatibility proofs for some (9/14) Part 1. Related to the Issue 370
  • MR 769 : Backward compatibility proofs for some (9/14) Part 2. Related to the Issue 370

Repr files

  • MR 763 : Verify Sc_rollup_game_repr.v for Proto_K.

2022-08-15 - 2022-08-19

Michelson

  • MR 756: More fixes in Script_ir_tranlator for Proto K.
  • MR 746: Simple proofs fixes in Script_ir_translator for Proto K.
  • MR 731: Backward compatibility proofs for some instructions
  • MR 743: Backward compatibility proofs for more instructions, fixing Issue 364
  • MR 738: Finish Sc_rollup_inbox_rerp proofs, closes Issue 330
  • MR 760: Add migration for the errors, closes Issue 379
  • MR 758: Backward compatibility proofs for some instructions, closes Issue 365

2022-08-08 - 2022-08-12

Michelson

2022-08-01 - 2022-08-05

Michelson

  • MR 721 : Port Script_interpreter and its dependencies to Proto_K, part 1. Relates to the Issue 289
  • MR 716 : Port Proots/Script_map, closes Issue 291
  • MR 718 : Finish the prof of Proofs/Script_typed_ir.v to Proto K, Part 2. Closes Issue 295
  • MR 717 : Port Proofs/Script_typed_ir.v to Proto K, Part 1. Related to Issue 295
  • MR 708: port the simulations of Script_ir_translator.v to proto K closing Issue 280
  • MR 710: port the simulations of Script_typed_interpreter.v to proto K closing Issue 279
  • MR 711: add admitted statement for the backward-compatibility of the Michelson interpreter in Script_interpreter.v
  • MR 712: Port Proofs/Script_family.v to Proto_K
  • MR 714: Port Proofs/Script_comparable.v to Proto_K, closes Issue 286 and Issue 294
  • MR 720 : Port Proofs/Script_tc_context.v to Proto_K, closes Issue 293
  • MR 722, MR 724 : Port Proofs/Script_set.v to Proto_K and prove dep_update_is_valid, closes Issue 292

Repr Files

Environment files

2022-07-25 - 2022-07-29

Michelson

  • MR 698: finish the definition of dep_parse_data_aux
  • MR 703: Add proof for IConcat_string
  • MR 696: Verification of KMap_exit_body instruction, also some progres with ISet_iter, IMap_iter and IMap_empty
  • MR 695: port Script_set.v and Script_map.v simulations to Proto_K
  • MR 709 : Finish the proof of diff_of_big_map, closes 220 Verify simulation for diff_of_big_map
  • MR 703 : More instruction proofs IEmpty_map, ISlice_string, IConcat_bytes, ISlice_bytes, IMul_teznat and IMul_nattez
  • MR 698 : finish the definition of dep_parse_data_aux
  • MR 704 : closes 302 Verify Constants_parametric_repr.v
  • MR 703 : Add proof for IConcat_string
  • MR 696 : Verification of KMap_exit_body instruction, also some progres with ISet_iter, IMap_iter and IMap_empty
  • MR 695 : port Script_set.v and Script_map.v simulations to Proto_K

Repr Files

2022-07-18 - 2022-07-22

Michelson

  • MR 692: finish definition of parse_data_aux_fuel1 (one case commented to compile it), also closes : 356, 357
  • MR 693: Finish the verification of IVoting_power, ITotal_voting_power, ITicket, IRead_ticket, ISplit_ticket, IJoin_tickets, KList_enter_body, KMap_enter_body.
  • MR 688: Verification of I_PACK and progress in the verification of I_UNPACK, related issues : 262 273
  • MR 687: closes Issue 276, Issue 284, Issue 285
  • MR 685: adds Proto_K/Simulation/Gas_comparable_input_size.v, closes Issue 273
  • MR 684: adds Proto_K/Simulation/Script_family.v, closes Issue 277

Translation

2022-07-11 - 2022-07-15

Michelson

  • MR 679: Proof for I_CONTRACT and I_LEVEL, related to the issues 256 and 261.
  • MR 682: parse_instr I_COMPARE, I_CAST, I_RENAME, I_CONTRACT, I_VIEW, I_TRANSFER_TOKENS, I_SET_DELEGATE, I_CREATE_ACCOUNT (fail), I_IMPLICIT_ACCOUNT, I_CREATE_CONTRACT, I_NOW, I_AMOUNT, I_CHAIN_ID, I_BALANCE, I_LEVEL, I_VOTING_POWER, I_TOTAL_VOTING_POWER, I_SOURCE, I_SENDER, I_SELF, I_DROP, I_PAIRING_CHECK, I_TICKET, I_READ_TICKET, I_SPLIT_TICKET, I_JOIN_TICKETS
  • MR 681: parse_instr I_SAPLING_VERIFY_UPDATE, I_IF, I_LAMBDA, I_EXEC, I_APPLY, I_DIP (1), I_DIP (n)
  • MR 680: parse_instr I_UPDATE bool set, I_CONS non-empty, I_ITER (cons body []), I_MEM (vk map rest), I_GET (vk map rest), I_UPDATE (vk opt map rest), I_GET_AND_UPDATE (vk opt map rest), I_EMPTY_BIG_MAP, I_MEM (big_map), I_GET (big_map), I_UPDATE (big_map), I_GET_AND_UPDATE (big_map)
  • MR 673: I_AMOUTN and I_BALANCE proof (related to the issue 264
  • MR 536: Verify more cases in the simulation proof for the interpreter in Script_interpreter.v
  • MR 658: I_ADD (one)
  • MR 661 : I_SUB (legacy mutez), I_SUB_MUTEZ, I_SUB int (int and int), I_SUB int (int and nat), I_SUB int (nat and int), I_SUB int (nat and nat)
  • MR 659: I_ITER
  • MR 665: I_AND (bool), I_AND (nat nat), I_AND (int nat)
  • MR 667 : I_OR (bool), I_OR_NAT (nat)
  • MR 662 : Definitions for I_MUL in parse_instr
  • MR 664: I_ITER, I_MAP
  • MR 669 : I_NOT (bool), I_NOT (int), I_NOT (nat), I_XOR (bool), I_XOR (nat)
  • MR 670 : I_ADD (int nat), I_ADD (nat nat), I_ABS (nat int), I_NEG (int), I_NEG (Nat), I_NEG (Bls12_381_g1), I_NEG (Bls12_381_g2), I_NEG (Bls12_381_fr)
  • MR 671 : Case EDIV_nat (nat nat), Case EDIV_nat (nat int), Case EDIV_int (int nat), Case EDIV_int (int int), Case EDIV_teznat (mutez nat), Case EDIV_tez (mutez mutez), Case IInt_bls12_381_fr (int of bls12_381_fr), Case I_int_nat (int of nat), Case I_ISNAT (int)
  • MR 672: I_LOOP, I_LOOP_LEFT
  • MR 675 : case I_GE, case I_LE, case I_GT, case I_LT, case I_NEQ, case I_EQ, case I_LSR, case LSL, case I_SIZE map
  • MR 677 : I_MUL (nat tez)

Tests

  • MR 646 : Translation of Test_gas_properties

Translation

  • MR 674 : Complete translation of Proto_K/Script_interpreter.v and some other files
  • MR 657 : Fixes in some of the proofs for Proto_K

2022-07-04 - 2022-07-08

Michelson

  • MR 654: I_IF_CONS, I_SIZE, I_BLAKE2B, I_SHA256, I_SHA512, I_KECCAK, I_SHA3, I_ADD (one), I_ADD (two), I_ADD (three), I_MAP
  • MR 655: Update the proof of verification for the comparison function on Michelson values in Script_comparable.v fixing Issue 243
dep_parse_instr_aux, Issue 215
  • MR 649: I_CONCAT, I_CONCAT, I_SLICE, I_UPDATE
  • MR 635: I_CDR, I_DUP (witness), I_SELF_ADDRESS, I_HASH_KEY, I_CHECK_SIGNATURE

Repr files

Translation

  • MR 660 : Compile Script_ir_translator.v for the protocol K
  • MR 650: Compile Alpha_context.v for the protocol K
  • MR 648: Add more files compiling in Coq from the protocol version K
  • MR 641: Add more files compiling in Coq from the protocol version K
  • MR 634: show separated folders on the website for the various environment/protocol versions, closes Issue 213
  • MR 636: Add definition for the Option library in Option.v
  • MR 638: Add definition for the Result library in Result.v
  • MR 643: Add definition for the Either library in Either.v
  • MR 644: Verify definition for the Either library in Either.v
  • MR 647: Add definition for the Result library in Result.v

2022-06-27 - 2022-07-01

Michelson

  • MR 627: dep_well_formed_entrypoints_eq
dep_parse_instr_aux, Issue 215
  • MR 524: start work on dep_parse_instr_aux
  • MR 619: I_DUP (1)
  • MR 620: I_DUP (n), I_ADDRESS
  • MR 621: 2 cases for I_DIG, 3 cases for I_DUG, I_PUSH, I_NONE, I_PAIR (cons n_value []) (defined with axiom), I_GET, I_LEFT, I_RIGHT, I_NIL, I_EMPTY_SET, I_EMPTY_MAP, I_SAPLING_EMPTY_STATE, 3 Micheline.Seq cases
  • MR 626: more cases defined for parse_instr_aux_fuel1
  • MR 629: I_MAP
  • MR 630: I_PAIR (n), I_IF_NONE, I_UNIT, I_SWAP, I_UNPAIR, I_ADD (mutez)
  • MR 632: I_UNPAIR, I_CAR
  • MR 633: I_IF_LEFT
  • MR 640: I_FAILWITH, I_NEVER, I_ADD (timestamp, int), I_ADD (int, timestamp), I_SUB (timestamp, int), I_SUB (timestamp, timestamp), I_CONCAT (str, str), I_CONCAT (list str), I_SLICE

Translation

2022-06-21 - 2022-06-25

Michelson

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

2022-06-06 - 2022-06-10

Michelson

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

Others

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

2022-05-23 - 2022-05-27

Michelson

2022-05-16 - 2022-05-22

Others

Skip-lists

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

Map

2022-05-09 - 2022-05-15

Data_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

Data_encoding

Skip-list

Reports

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: add a script to generate the list of dependent simulations to write, mainly for the translator of Michelson for now

Compare

Data_encoding

Others

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

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

Others

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.