Changelog
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
- MR 1010: Begin work on verifying
Sc_rollup_operations.v
, part of Issue #739 and of Issue #737 - MR 1004: Begin work on verifying
Sc_rollup_wasm.v
, part of Issue #749 - MR 1011: Verify
Sc_rollup_commitment_storage.v
, closes Issue 727
2022-12-12 - 2022-12-16
Others
- MR 1003: Update the storage specification to the last protocol update. Closes Issue 724
- MR 1002: Verify
Sc_rollup_refutation.v
, part 4. Part of Issue #713
Mi-Cho-Coq Compatibility
Verify Rollups
- MR 1006: Verify Rollup related files, in particular
Sc_rollup_inbox_message_repr.v
(wip) andSc_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
- MR 999: Create intermediate AST for Mi-Cho-Coq verification, closes Issue #715
2022-11-28 - 2022-12-02
Others
- MR 996: Verify
Sc_rollup_refutation.v
, part 2. Part of the Issue #713 - MR 995: Verify
Sc_rollup_refutation.v
, part 1. Part of the Issue #713 - MR 976: Verify Level_storage.v, part 1. Part of the Issue #713
- MR 987: Verify Level_storage.v, part 2. Part of the Issue #713
- MR 989: Cleanup of Proofs/Map.v
- MR 990: Verify Zk_rollup_ticket_repr.v, closes Issue #709
- MR 984: Verify [Ticket_scanner.v].
- MR 988: Verify Constants_storage.v. Part of Issue #713
- MR 991: Verify Zk_rollup_parameters.v, closes Issue #708
Michelson
- MR 993: more definitions for Issue #700: Update Proofs/Script_....v
- MR 980:
- Adding the lastest cases for the
value
validity predicate (Map_value
andBig_map_value
) (closes Issue #697: definekinstr
andvalues
) - Adding some changes related to Issue #700: Update the remaining proofs files Script_....v.
- MR 986: Compatibility of
parse_ty
andunparse_ty
functions in Script_ir_translator.v (related to Issue #701: Verify the validity of some functions inScript_ir_translator.v
)
2022-11-21 - 2022-11-25
Michelson
- MR 975: Closes Issue #698: Specify Script_typed_ir.continuation.
- MR 971: Related to Issue #697: define kinstr and values.
- MR 974: Closes Issue #699: Update [Proofs/Script_ir_translator.v]
- MR 977: Related to Issue #700: Updating Proofs/Script_...v.
- MR 985: Related to Issue #697: Inductive type_contract defined + several cases in
values
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
- MR 968: specify Script_typed_ir.ty Issue #696: specify
script_typed_ir.ty
. - MR 964: Use the upstream version of Mi-Cho-Coq (branch
dev
) instead of a vendored one - MR 961: Closes Issue #695: simplify Script_family.v.
- MR 960: Closes Issue #694: remove all the simulations.
Others
- MR 972: Make the context simulation record flat. Issue 711
- MR 973: Make the context simulation record flat, part 2. Issue 711
- MR 982: Make the context simulation record flat, part 3. Issue 711
2022-11-07 - 2022-11-11
Internal Errors
- MR 944: Verify Validate, part 4 Issue 674
- MR 949: Verify Validate, part 5 Issue 674
- MR 951: Verify
Tx_rollup_gas.v
, addresses Issue 643 - MR 952: Verify
Script_typed_ir.v
Pt. 1 (Issue 611 - MR 953: Progress on
Apply.v
. Adresses Issue 430. - MR 957: Verify
Script_typed_ir.v
Pt. 2 (Issue 611 - MR 958: Refactor
Operation_repr
predicates - MR 967: Verify
Ticket_amount.v
. Adresses Issue 706
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
exceptLamRec
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
- MR 936: Lemma [apply_manager_operation] is proved, addresses Issue 430: verify Apply.v.
- MR 938: small proof for Constants_storage.v, addresses Internal_errors task.
- MR 928: Verify Validate, part 3 Issue 674
- MR 929: More cases in
Apply.v
, addresses Issue 430: verify Apply.v. - MR 925: New cases in
Apply.v
, addresses Issue 430: verify Apply.v. - MR 924: Verify
Sc_rollup_inbox_repr.v
, related to Issue 576 - MR 923: Verify
Dal_apply.v
,Sc_rollup_PVM_sem.v
,Origination_nonce.v
,Tx_rollup_l2_context_sig.v
- MR 927: Verify
Sc_rollup_inbox_repr.v
, closes Issue 576 - MR 911: Verify Validate, part 2 Issue 674
- MR 926: Verify
Tx_rollup_l2_storage_sig.v
,Tx_rollup_l2_context_sig.v
,Tx_rollup_l2_context.v
- MR 930: Progress towards the verification of
Main.v
- MR 935: End of verification of
Main.v
- MR 931 and MR 937: Verify
Tx_rollup_ticket.v
, closes Issue 617 - MR 940: Verify
Tx_rollup_l2_verifier.v
, closes Issue 656
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
andTicket_scanner.v
- MR 908: verify the internal errors for
Ticket_balance_key.v
andTicket_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
, andVerify 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
, andLiquidity_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
andZk_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
andTx_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
andFrozen_deposits_storage.v
- MR 900: Specify
Sc_rollup_storage.v
,Ticket_storage.v
,Tx_rollup_commitment_storage.v
andTx_rollup_inbox_storage.v
Michelson
- MR 878: fixing proofs in
Proto_alpha
, addresses the Issue 388 - MR 889: fixing proofs in
Proto_alpha
, addresses the Issue 388
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
toProto_alpha
, addresses the Issue 392 - MR 842: solves
get_total_voting_power_free_is_backward_compatible
fromProto_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 ofproto_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
- MR 715: closes 309 Verify Entrypoint_repr.v, closes 296 Verify Block_header_repr.v, adding several proofs for Proto_alpha (and for Proto_K).
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
andget_total_voting_power
fromProto_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
andIMap_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
andIMap_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
toProto_J
andProto_A
toProto_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
- MR 745: Add
dep_unparse_ty_entrypoints_uncarbonated_eq
proof inScript_ir_translator.v
of Proto K. - MR 742: Add dep_unparse_comparable_ty_uncarbonated_eq proof in Script_typed_ir
- MR 739: Add comments and fix the import order.
- MR 735: Verify
Sc_rollup_proof_repr
for Proto K, closes Issue 332 - MR 736: Verify Sc_rollup_outbox_message_repr.v for Proto K, closes Issue 331
- MR 723: Fix or remove commented lemmas in Script_ir_translator.v part of Issue 289 and add a status page Proto K simulations
- MR 729: Fix Script_interpreter proofs in Proto_K, part 2. Relates to the Issue 289
- MR 725: Migrate the continuations in Script_typed_ir.v closing Issue 360
- MR 726: Statement of the backward compatibility lemma for
dep_next
inScript_interpreter.v
closing Issue 361 - MR 728: Migration of the instructions in Script_typed_ir.v closing Issue 359
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
toProto_K
- MR 714: Port
Proofs/Script_comparable.v
toProto_K
, closes Issue 286 and Issue 294 - MR 720 : Port
Proofs/Script_tc_context.v
toProto_K
, closes Issue 293 - MR 722, MR 724 : Port
Proofs/Script_set.v
toProto_K
and provedep_update_is_valid
, closes Issue 292
Repr Files
- MR 705: closes 303 Verify Constants_repr.v, 304 Verify Contract_repr.v, 307 Verify Dal_slot_repr.v
- MR 707: Verifies Dal_endorsement_repr.v, closes Issue 306
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 withISet_iter
,IMap_iter
andIMap_empty
- MR 695: port
Script_set.v
andScript_map.v
simulations toProto_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
andIMul_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 withISet_iter
,IMap_iter
andIMap_empty
- MR 695 : port
Script_set.v
andScript_map.v
simulations toProto_K
Repr Files
- MR 704: closes 302 Verify Constants_parametric_repr.v
- MR 699: Verifies Time_repr.v, closes Issue 340
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
- MR 686: completes the translation of Script_ir_translator.v
- MR 689: completes the translation of axiomatized functions in Michelson related files for the protocol K
- MR 694: Completes most definitions in List.v
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
andI_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
- MR 645: Verify the encodings in Constants_parametric_previous_repr.v and Ratio_repr.v
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
- 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
anddep_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
andset
for simulation ofparse_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
anddep_parse_code
. - MR 531 related to Issue 136: Add simulations
dep_find_entrypoint
anddep_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
andbig_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 fordep_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
anddep_collect_lazy_storage
- MR 519 related to Isse 141: Add simulations definitions
dep_unparse_data
anddep_unparse_code
.
2022-05-16 - 2022-05-22
Others
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
anddep_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 axiomatingitem_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
Tests
- MR 485in
Test_bitset.v
: verify the property-based tests oftest_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 theIExec
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 forcompare_comparable_eq
Data_encoding
- MR 451 in
Storage.v
Skip-list
- MR 472 in Skip_list_repr.v: verification of the
equal
function
Reports
2022-04-25 - 2022-05-01
Michelson
- MR 452 in Script_ir_translator.v: add simulations of
close_descr
,kinfo_of_descr
andcompose_descr
- MR 450: add a script to generate the 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 ofseq_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 tounparse_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
andmem_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
andty_of_comparable_ty
are compatible (2 reciprocal Fixpoints created and proved),ty
andcomparable_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 usingcoq-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 twokinstr
's.