Skip to main content

Changelog

Gitlab

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

2022-06-27 - 2022-07-01#

Michelson#

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#