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-09-19 - 2022-09-23

Michelson

  • MR 814: Verify ISapling_verify_update_deprecated simulation

Translation

  • 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.

Others

  • 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

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

2022-06-13 - 2022-06-17

Michelson

2022-06-06 - 2022-06-10

Michelson

Tests

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

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

Compare

Data_encoding

Others

2022-04-18 - 2022-04-24

Michelson

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