Skip to main content

Proto k simulations

Gitlab

Script_interpreter.v

Proofs

92%

  1. IDrop 🟢
  2. IDup 🟢
  3. ISwap 🟢
  4. IConst 🟢
  5. ICons_pair 🟢
  6. ICar 🟢
  7. ICdr 🟢
  8. IUnpair 🟢
  9. ICons_some 🟢
  10. ICons_none 🟢
  11. IIf_none 🟢
  12. IOpt_map 🟢
  13. ICons_left 🟢
  14. ICons_right 🟢
  15. IIf_left 🟢
  16. ICons_list 🟢
  17. INil 🟢
  18. IIf_cons 🟢
  19. IList_map 🟢
  20. IList_iter 🟢
  21. IList_size 🟢
  22. IEmpty_set 🟢
  23. ISet_iter 🟢
  24. ISet_mem 🟢
  25. ISet_update 🟢
  26. ISet_size 🟢
  27. IEmpty_map 🟢
  28. IMap_map 🟢
  29. IMap_iter 🟢
  30. IMap_mem 🟢
  31. IMap_get 🟢
  32. IMap_update 🟢
  33. IMap_get_and_update 🔴
  34. IMap_size 🔴
  35. IEmpty_big_map 🟢
  36. IBig_map_mem 🟢
  37. IBig_map_get 🟢
  38. IBig_map_update 🟢
  39. IBig_map_get_and_update 🔴
  40. IConcat_string 🟢
  41. IConcat_string_pair 🟢
  42. ISlice_string 🟢
  43. IString_size 🟢
  44. IConcat_bytes 🟢
  45. IConcat_bytes_pair 🟢
  46. ISlice_bytes 🟢
  47. IBytes_size 🟢
  48. IAdd_seconds_to_timestamp 🟢
  49. IAdd_timestamp_to_seconds 🟢
  50. ISub_timestamp_seconds 🟢
  51. IDiff_timestamps 🟢
  52. IAdd_tez 🟢
  53. ISub_tez 🟢
  54. ISub_tez_legacy 🟢
  55. IMul_teznat 🟢
  56. IMul_nattez 🟢
  57. IEdiv_teznat 🟢
  58. IEdiv_tez 🟢
  59. IOr 🟢
  60. IAnd 🟢
  61. IXor 🟢
  62. INot 🟢
  63. IIs_nat 🟢
  64. INeg 🟢
  65. IAbs_int 🟢
  66. IInt_nat 🟢
  67. IAdd_int 🟢
  68. IAdd_nat 🟢
  69. ISub_int 🟢
  70. IMul_int 🟢
  71. IMul_nat 🟢
  72. IEdiv_int 🟢
  73. IEdiv_nat 🟢
  74. ILsl_nat 🟢
  75. ILsr_nat 🟢
  76. IOr_nat 🟢
  77. IAnd_nat 🟢
  78. IAnd_int_nat 🟢
  79. IXor_nat 🟢
  80. INot_int 🟢
  81. IIf 🟢
  82. ILoop 🟢
  83. ILoop_left 🟢
  84. IDip 🟢
  85. IExec 🟢
  86. IApply 🟢
  87. ILambda 🟢
  88. IFailwith 🟢
  89. ICompare 🟢
  90. IEq 🟢
  91. INeq 🟢
  92. ILt 🟢
  93. IGt 🟢
  94. ILe 🟢
  95. IGe 🟢
  96. IAddress 🟢
  97. IContract 🟢
  98. IView 🔴
  99. ITransfer_tokens 🔴
  100. IImplicit_account 🟢
  101. ICreate_contract 🟢
  102. ISet_delegate 🟢
  103. INow 🟢
  104. IMin_block_time 🔴
  105. IBalance 🟢
  106. ILevel 🟢
  107. ICheck_signature 🟢
  108. IHash_key 🟢
  109. IPack 🟢
  110. IUnpack 🟢
  111. IBlake2b 🟢
  112. ISha256 🟢
  113. ISha512 🟢
  114. ISource 🟢
  115. ISender 🟢
  116. ISelf 🟢
  117. ISelf_address 🟢
  118. IAmount 🟢
  119. ISapling_empty_state 🟢
  120. ISapling_verify_update 🟢
  121. ISapling_verify_update_deprecated 🟢
  122. IDig 🔴
  123. IDug 🔴
  124. IDipn 🔴
  125. IDropn 🔴
  126. IChainId 🟢
  127. INever 🟢
  128. IVoting_power 🟢
  129. ITotal_voting_power 🟢
  130. IKeccak 🟢
  131. ISha3 🟢
  132. IAdd_bls12_381_g1 🟢
  133. IAdd_bls12_381_g2 🟢
  134. IAdd_bls12_381_fr 🟢
  135. IMul_bls12_381_g1 🟢
  136. IMul_bls12_381_g2 🟢
  137. IMul_bls12_381_fr 🟢
  138. IMul_bls12_381_z_fr 🟢
  139. IMul_bls12_381_fr_z 🟢
  140. IInt_bls12_381_fr 🟢
  141. INeg_bls12_381_g1 🟢
  142. INeg_bls12_381_g2 🟢
  143. INeg_bls12_381_fr 🟢
  144. IPairing_check_bls12_381 🟢
  145. IComb 🔴
  146. IUncomb 🔴
  147. IComb_get 🟢
  148. IComb_set 🟢
  149. IDup_n 🟢
  150. ITicket 🟢
  151. IRead_ticket 🟢
  152. ISplit_ticket 🟢
  153. IJoin_tickets 🟢
  154. IOpen_chest 🟢
  155. IHalt 🟢
  156. KNil 🟢
  157. KCons 🟢
  158. KReturn 🟢
  159. KMap_head 🟢
  160. KUndip 🟢
  161. KLoop_in 🟢
  162. KLoop_in_left 🟢
  163. KIter 🟢
  164. KList_enter_body 🟢
  165. KList_exit_body 🟢
  166. KMap_enter_body 🟢
  167. KMap_exit_body 🟢
  168. KView_exit 🟢

Script_ir_translator.v

Simulations

We also check that the simulations are in the right order.

56%

  1. dep_close_descr 🟢
  2. dep_compose_descr 🟢
  3. dep_tc_context 🟢
  4. dep_type_logger 🔴
  5. dep_location 🔴
  6. dep_kind_equal 🔴
  7. dep_kind_value 🔴
  8. dep_unexpected 🔴
  9. dep_check_kind 🔴
  10. dep_unparse_memo_size 🔴
  11. dep_unparse_ty_and_entrypoints_uncarbonated 🔴
  12. dep_unparse_comparable_ty_uncarbonated 🟢
  13. dep_unparse_ty_uncarbonated 🟢
  14. dep_unparse_ty 🟢
  15. dep_unparse_parameter_ty 🟢
  16. dep_serialize_ty_for_error 🟢
  17. dep_check_comparable 🟢
  18. dep_unparse_stack_uncarbonated 🟢
  19. dep_serialize_stack_for_error 🟢
  20. dep_unparse_unit 🔴
  21. dep_unparse_int 🔴
  22. dep_unparse_nat 🔴
  23. dep_unparse_string 🔴
  24. dep_unparse_bytes 🔴
  25. dep_unparse_bool 🔴
  26. dep_unparse_timestamp 🔴
  27. dep_unparse_address 🔴
  28. dep_unparse_tx_rollup_l2_address 🔴
  29. dep_unparse_contract 🟢
  30. dep_unparse_signature 🔴
  31. dep_unparse_mutez 🔴
  32. dep_unparse_key 🔴
  33. dep_unparse_key_hash 🔴
  34. dep_unparse_operation 🔴
  35. dep_unparse_chain_id 🔴
  36. dep_unparse_bls12_381_g1 🔴
  37. dep_unparse_bls12_381_g2 🔴
  38. dep_unparse_bls12_381_fr 🔴
  39. dep_unparse_with_data_encoding 🔴
  40. dep_unparse_pair 🔴
  41. dep_unparse_union 🔴
  42. dep_unparse_option 🔴
  43. dep_comb_witness2 🟢
  44. dep_unparse_comparable_data 🟢
  45. dep_pack_node 🔴
  46. dep_pack_comparable_data 🟢
  47. dep_hash_bytes 🔴
  48. dep_hash_comparable_data 🟢
  49. dep_check_dupable_comparable_ty 🟢
  50. dep_check_dupable_ty 🟢
  51. dep_type_metadata_eq 🟢
  52. dep_default_ty_eq_error 🟢
  53. dep_memo_size_eq 🔴
  54. dep_ty_eq 🟢
  55. dep_stack_eq 🟢
  56. dep_merge_branches 🟢
  57. dep_parse_memo_size 🔴
  58. dep_their 🔴
  59. dep_parse_ty_aux 🟢
  60. dep_parse_comparable_ty_aux 🟢
  61. dep_parse_big_map_ty 🟢
  62. dep_parse_passable_ty_aux_with_ret 🟢
  63. dep_parse_any_ty_aux 🟢
  64. dep_parse_big_map_value_ty_aux 🟢
  65. dep_parse_packable_ty_aux 🟢
  66. dep_parse_view_input_ty 🟢
  67. dep_parse_view_output_ty 🟢
  68. dep_parse_normal_storage_ty 🟢
  69. dep_parse_storage_ty 🟢
  70. dep_check_packable 🟢
  71. dep_typed_view_map 🟢
  72. dep_make_dug_proof_argument 🟢
  73. dep_make_comb_get_proof_argument 🟢
  74. dep_make_comb_set_proof_argument 🟢
  75. dep_find_entrypoint 🟢
  76. dep_find_entrypoint_for_type 🟢
  77. dep_well_formed_entrypoints 🟢
  78. dep_parse_parameter_ty_and_entrypoints_aux 🟢
  79. dep_parse_passable_ty_aux 🟢
  80. dep_parse_uint 🔴
  81. dep_parse_uint10 🔴
  82. dep_parse_uint11 🔴
  83. dep_opened_ticket_type 🟢
  84. dep_parse_unit 🔴
  85. dep_parse_bool 🔴
  86. dep_parse_string 🔴
  87. dep_parse_bytes 🔴
  88. dep_parse_int 🔴
  89. dep_parse_nat 🔴
  90. dep_parse_mutez 🔴
  91. dep_parse_timestamp 🔴
  92. dep_parse_key 🔴
  93. dep_parse_key_hash 🔴
  94. dep_parse_signature 🔴
  95. dep_parse_chain_id 🔴
  96. dep_parse_address 🔴
  97. dep_parse_tx_rollup_l2_address 🔴
  98. dep_parse_never 🔴
  99. dep_parse_pair 🔴
  100. dep_parse_union 🔴
  101. dep_parse_option 🔴
  102. dep_comb_witness1 🟢
  103. dep_parse_view_name 🟢
  104. dep_parse_toplevel_aux 🟢
  105. dep_parse_data_aux 🟢
  106. dep_parse_view 🟢
  107. dep_parse_instr_aux 🟢
  108. dep_loc_value 🔴
  109. dep_parse_views 🔴
  110. dep_parse_returning 🔴
  111. dep_parse_contract 🟢
  112. dep_parse_contract_data_aux 🔴
  113. dep_parse_contract_for_script 🟢
  114. dep_view_size 🔴
  115. dep_code_size 🟢
  116. dep_parse_code 🟢
  117. dep_parse_storage 🟢
  118. dep_parse_script 🟢
  119. dep_typecheck_code_aux 🟢
  120. dep_list_entrypoints_uncarbonated 🟢
  121. dep_unparse_data_aux 🟢
  122. dep_unparse_code_aux 🟢
  123. dep_unparse_items 🟢
  124. dep_parse_and_unparse_script_unaccounted 🟢
  125. dep_pack_data_with_mode 🟢
  126. dep_hash_data 🟢
  127. dep_pack_data 🟢
  128. dep_lazy_storage_ids 🔴
  129. dep_no_lazy_storage_id 🔴
  130. dep_diff_of_big_map 🟢
  131. dep_diff_of_sapling_state 🔴
  132. dep_has_lazy_storage_value 🟢
  133. dep_extract_lazy_storage_updates 🟢
  134. dep_fold_lazy_storage 🟢
  135. dep_collect_lazy_storage 🟢
  136. dep_extract_lazy_storage_diff 🟢
  137. dep_list_of_big_map_ids 🔴
  138. dep_parse_data 🟢
  139. dep_parse_comparable_data 🔴
  140. dep_parse_instr 🟢
  141. dep_unparse_data 🟢
  142. dep_unparse_code 🟢
  143. dep_parse_contract_data 🔴
  144. dep_parse_toplevel 🟢
  145. dep_parse_comparable_ty 🟢
  146. dep_parse_big_map_value_ty 🟢
  147. dep_parse_packable_ty 🟢
  148. dep_parse_passable_ty 🟢
  149. dep_parse_any_ty 🟢
  150. dep_parse_ty 🟢
  151. dep_parse_parameter_ty_and_entrypoints 🟢
  152. dep_get_single_sapling_state 🟢
  153. dep_script_size 🟢
  154. dep_typecheck_code 🟢

Proofs

We also check that the proofs are in the right order.

37%

  1. dep_close_descr_eq 🟢
  2. dep_compose_descr_eq 🟢
  3. dep_tc_context_eq 🔴
  4. dep_type_logger_eq 🔴
  5. dep_location_eq 🔴
  6. dep_kind_equal_eq 🔴
  7. dep_kind_value_eq 🔴
  8. dep_unexpected_eq 🔴
  9. dep_check_kind_eq 🔴
  10. dep_unparse_memo_size_eq 🔴
  11. dep_unparse_ty_and_entrypoints_uncarbonated_eq 🔴
  12. dep_unparse_comparable_ty_uncarbonated_eq 🟢
  13. dep_unparse_ty_uncarbonated_eq 🟢
  14. dep_unparse_ty_eq 🟢
  15. dep_unparse_parameter_ty_eq 🟢
  16. dep_serialize_ty_for_error_eq 🟢
  17. dep_check_comparable_eq 🔴
  18. dep_unparse_stack_uncarbonated_eq 🟢
  19. dep_serialize_stack_for_error_eq 🟢
  20. dep_unparse_unit_eq 🔴
  21. dep_unparse_int_eq 🔴
  22. dep_unparse_nat_eq 🔴
  23. dep_unparse_string_eq 🔴
  24. dep_unparse_bytes_eq 🔴
  25. dep_unparse_bool_eq 🔴
  26. dep_unparse_timestamp_eq 🔴
  27. dep_unparse_address_eq 🔴
  28. dep_unparse_tx_rollup_l2_address_eq 🔴
  29. dep_unparse_contract_eq 🟢
  30. dep_unparse_signature_eq 🔴
  31. dep_unparse_mutez_eq 🔴
  32. dep_unparse_key_eq 🔴
  33. dep_unparse_key_hash_eq 🔴
  34. dep_unparse_operation_eq 🔴
  35. dep_unparse_chain_id_eq 🔴
  36. dep_unparse_bls12_381_g1_eq 🔴
  37. dep_unparse_bls12_381_g2_eq 🔴
  38. dep_unparse_bls12_381_fr_eq 🔴
  39. dep_unparse_with_data_encoding_eq 🔴
  40. dep_unparse_pair_eq 🔴
  41. dep_unparse_union_eq 🔴
  42. dep_unparse_option_eq 🔴
  43. dep_comb_witness2_eq 🟢
  44. dep_unparse_comparable_data_eq 🟢
  45. dep_pack_node_eq 🔴
  46. dep_pack_comparable_data_eq 🟢
  47. dep_hash_bytes_eq 🔴
  48. dep_hash_comparable_data_eq 🟢
  49. dep_check_dupable_comparable_ty_eq 🟢
  50. dep_check_dupable_ty_eq 🟢
  51. dep_type_metadata_eq_eq 🟢
  52. dep_default_ty_eq_error_eq 🟢
  53. dep_memo_size_eq_eq 🔴
  54. dep_ty_eq_eq 🟢
  55. dep_stack_eq_eq 🟢
  56. dep_merge_branches_eq 🟢
  57. dep_parse_memo_size_eq 🔴
  58. dep_their_eq 🔴
  59. dep_parse_ty_aux_eq 🟢
  60. dep_parse_comparable_ty_aux_eq 🔴
  61. dep_parse_big_map_ty_eq 🟢
  62. dep_parse_passable_ty_aux_with_ret_eq 🟢
  63. dep_parse_any_ty_aux_eq 🟢
  64. dep_parse_big_map_value_ty_aux_eq 🟢
  65. dep_parse_packable_ty_aux_eq 🟢
  66. dep_parse_view_input_ty_eq 🟢
  67. dep_parse_view_output_ty_eq 🟢
  68. dep_parse_normal_storage_ty_eq 🟢
  69. dep_parse_storage_ty_eq 🟢
  70. dep_check_packable_eq 🟢
  71. dep_typed_view_map_eq 🔴
  72. dep_make_dug_proof_argument_eq 🟢
  73. dep_make_comb_get_proof_argument_eq 🟢
  74. dep_make_comb_set_proof_argument_eq 🟢
  75. dep_find_entrypoint_eq 🟢
  76. dep_find_entrypoint_for_type_eq 🟢
  77. dep_well_formed_entrypoints_eq 🟢
  78. dep_parse_parameter_ty_and_entrypoints_aux_eq 🟢
  79. dep_parse_passable_ty_aux_eq 🟢
  80. dep_parse_uint_eq 🔴
  81. dep_parse_uint10_eq 🔴
  82. dep_parse_uint11_eq 🔴
  83. dep_opened_ticket_type_eq 🟢
  84. dep_parse_unit_eq 🔴
  85. dep_parse_bool_eq 🔴
  86. dep_parse_string_eq 🔴
  87. dep_parse_bytes_eq 🔴
  88. dep_parse_int_eq 🔴
  89. dep_parse_nat_eq 🔴
  90. dep_parse_mutez_eq 🔴
  91. dep_parse_timestamp_eq 🔴
  92. dep_parse_key_eq 🔴
  93. dep_parse_key_hash_eq 🔴
  94. dep_parse_signature_eq 🔴
  95. dep_parse_chain_id_eq 🔴
  96. dep_parse_address_eq 🔴
  97. dep_parse_tx_rollup_l2_address_eq 🔴
  98. dep_parse_never_eq 🔴
  99. dep_parse_pair_eq 🔴
  100. dep_parse_union_eq 🔴
  101. dep_parse_option_eq 🔴
  102. dep_comb_witness1_eq 🟢
  103. dep_parse_view_name_eq 🟢
  104. dep_parse_toplevel_aux_eq 🟢
  105. dep_parse_data_aux_eq 🔴
  106. dep_parse_view_eq 🔴
  107. dep_parse_instr_aux_eq 🟢
  108. dep_loc_value_eq 🔴
  109. dep_parse_views_eq 🔴
  110. dep_parse_returning_eq 🟢
  111. dep_parse_contract_eq 🟢
  112. dep_parse_contract_data_aux_eq 🔴
  113. dep_parse_contract_for_script_eq 🔴
  114. dep_view_size_eq 🔴
  115. dep_code_size_eq 🔴
  116. dep_parse_code_eq 🔴
  117. dep_parse_storage_eq 🔴
  118. dep_parse_script_eq 🔴
  119. dep_typecheck_code_aux_eq 🔴
  120. dep_list_entrypoints_uncarbonated_eq 🔴
  121. dep_unparse_data_aux_eq 🔴
  122. dep_unparse_code_aux_eq 🔴
  123. dep_unparse_items_eq 🔴
  124. dep_parse_and_unparse_script_unaccounted_eq 🔴
  125. dep_pack_data_with_mode_eq 🔴
  126. dep_hash_data_eq 🔴
  127. dep_pack_data_eq 🔴
  128. dep_lazy_storage_ids_eq 🔴
  129. dep_no_lazy_storage_id_eq 🔴
  130. dep_diff_of_big_map_eq 🔴
  131. dep_diff_of_sapling_state_eq 🔴
  132. dep_has_lazy_storage_value_eq 🔴
  133. dep_extract_lazy_storage_updates_eq 🔴
  134. dep_fold_lazy_storage_eq 🔴
  135. dep_collect_lazy_storage_eq 🔴
  136. dep_extract_lazy_storage_diff_eq 🔴
  137. dep_list_of_big_map_ids_eq 🔴
  138. dep_parse_data_eq 🔴
  139. dep_parse_comparable_data_eq 🔴
  140. dep_parse_instr_eq 🔴
  141. dep_unparse_data_eq 🔴
  142. dep_unparse_code_eq 🔴
  143. dep_parse_contract_data_eq 🔴
  144. dep_parse_toplevel_eq 🟢
  145. dep_parse_comparable_ty_eq 🟢
  146. dep_parse_big_map_value_ty_eq 🟢
  147. dep_parse_packable_ty_eq 🟢
  148. dep_parse_passable_ty_eq 🟢
  149. dep_parse_any_ty_eq 🟢
  150. dep_parse_ty_eq 🟢
  151. dep_parse_parameter_ty_and_entrypoints_eq 🟢
  152. dep_get_single_sapling_state_eq 🟢
  153. dep_script_size_eq 🟢
  154. dep_typecheck_code_eq 🟢