Skip to main content

Sprints

Gitlab

Sprint 8โ€‹

2022-10-17 - 2022-10-28

Done: 0/0

IssueAssignedWeightDoneTitle
Issue #589?ย ๐Ÿ’ช๐Ÿ”ดVerify Sc_rollups.v
Issue #590?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_big_map.v
Issue #591?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_cache.v
Issue #592?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_comparable.v
Issue #593?ย ๐Ÿ’ช๐ŸŸขVerify Script_expr_hash.v
Issue #594?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_int.v
Issue #595?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_interpreter.v
Issue #596?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_interpreter_defs.v
Issue #597?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_interpreter_logging.v
Issue #598?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_ir_annot.v
Issue #599?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_ir_translator.v
Issue #600?ย ๐Ÿ’ช๐ŸŸขVerify Script_ir_translator_config.v
Issue #601?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_ir_unparser.v
Issue #602?ย ๐Ÿ’ช๐ŸŸขVerify Script_list.v
Issue #603EM?ย ๐Ÿ’ช๐ŸŸขVerify Script_map.v
Issue #604?ย ๐Ÿ’ช๐ŸŸขVerify Script_repr.v
Issue #605?ย ๐Ÿ’ช๐ŸŸขVerify Script_set.v
Issue #606EM?ย ๐Ÿ’ช๐ŸŸขVerify Script_string.v
Issue #607?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_tc_context.v
Issue #608?ย ๐Ÿ’ช๐ŸŸขVerify Script_tc_errors.v
Issue #609?ย ๐Ÿ’ช๐ŸŸขVerify Script_tc_errors_registration.v
Issue #610?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_timestamp.v
Issue #611EM?ย ๐Ÿ’ช๐ŸŸขVerify Script_typed_ir.v
Issue #612?ย ๐Ÿ’ช๐Ÿ”ดVerify Script_typed_ir_size.v
Issue #613?ย ๐Ÿ’ช๐ŸŸขVerify Script_typed_ir_size_costs.v
Issue #614?ย ๐Ÿ’ช๐ŸŸขVerify Seed_repr.v
Issue #615DH?ย ๐Ÿ’ช๐ŸŸขVerify Seed_storage.v
Issue #616?ย ๐Ÿ’ช๐ŸŸขVerify Services_registration.v
Issue #617?ย ๐Ÿ’ช๐ŸŸขVerify Skip_list_repr.v
Issue #618AK?ย ๐Ÿ’ช๐Ÿ”ดVerify Slot_repr.v
Issue #619AK?ย ๐Ÿ’ช๐Ÿ”ดVerify Stake_storage.v
Issue #620?ย ๐Ÿ’ช๐ŸŸขVerify State_hash.v
Issue #621?ย ๐Ÿ’ช๐ŸŸขVerify Storage.v
Issue #622?ย ๐Ÿ’ช๐ŸŸขVerify Storage_costs.v
Issue #623?ย ๐Ÿ’ช๐ŸŸขVerify Storage_description.v
Issue #624?ย ๐Ÿ’ช๐ŸŸขVerify Storage_functors.v
Issue #625?ย ๐Ÿ’ช๐ŸŸขVerify Storage_sigs.v
Issue #626?ย ๐Ÿ’ช๐ŸŸขVerify Tez_repr.v
Issue #627GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_accounting.v
Issue #628GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_balance_key.v
Issue #629GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_costs.v
Issue #630GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_hash_builder.v
Issue #631?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_hash_repr.v
Issue #632GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_lazy_storage_diff.v
Issue #633GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_operations_diff.v
Issue #634GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_scanner.v
Issue #635GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_storage.v
Issue #636GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_token.v
Issue #637GC?ย ๐Ÿ’ช๐ŸŸขVerify Ticket_token_map.v
Issue #638?ย ๐Ÿ’ช๐ŸŸขVerify Time_repr.v
Issue #639NK?ย ๐Ÿ’ช๐ŸŸขVerify Token.v
Issue #640?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_commitment_repr.v
Issue #641GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_commitment_storage.v
Issue #642?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_errors_repr.v
Issue #643EM?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_gas.v
Issue #644AK?ย ๐Ÿ’ช๐Ÿ”ดVerify Tx_rollup_hash_builder.v
Issue #645?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_inbox_repr.v
Issue #646GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_inbox_storage.v
Issue #647AK?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_address.v
Issue #648?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_apply.v
Issue #649?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_batch.v
Issue #650GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_context.v
Issue #651?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_context_hash.v
Issue #652GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_context_sig.v
Issue #653?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_proof.v
Issue #654?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_qty.v
Issue #655GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_storage_sig.v
Issue #656EM?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_l2_verifier.v
Issue #657?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_level_repr.v
Issue #658?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_hash_repr.v
Issue #659?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_repr.v
Issue #660?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_result_hash_repr.v
Issue #661?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_result_repr.v
Issue #662GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_parameters.v
Issue #663NK?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_prefixes.v
Issue #664?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_repr.v
Issue #665?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_reveal_repr.v
Issue #666GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_reveal_storage.v
Issue #667?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_services.v
Issue #668?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_state_repr.v
Issue #669?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_state_storage.v
Issue #670GC?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_storage.v
Issue #671EM?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_ticket.v
Issue #672?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_withdraw_list_hash_repr.v
Issue #673?ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_withdraw_repr.v
Issue #674?ย ๐Ÿ’ช๐Ÿ”ดVerify Validate.v
Issue #675?ย ๐Ÿ’ช๐ŸŸขVerify Validate_errors.v
Issue #676?ย ๐Ÿ’ช๐ŸŸขVerify Vote_repr.v
Issue #677GC?ย ๐Ÿ’ช๐ŸŸขVerify Vote_storage.v
Issue #678?ย ๐Ÿ’ช๐ŸŸขVerify Voting_period_repr.v
Issue #679GC?ย ๐Ÿ’ช๐ŸŸขVerify Voting_period_storage.v
Issue #680?ย ๐Ÿ’ช๐ŸŸขVerify Voting_services.v
Issue #681?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_account_repr.v
Issue #682NK?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_apply.v
Issue #683?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_operation_repr.v
Issue #684?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_repr.v
Issue #685NK?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_scalar.v
Issue #686?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_state_repr.v
Issue #687GC?ย ๐Ÿ’ช๐ŸŸขVerify Zk_rollup_storage.v
Issue #688DH?ย ๐Ÿ’ช๐ŸŸขVerify Amendment

Sprint 7โ€‹

2022-08-22 - 2022-08-26

Done: 90/119

IssueAssignedWeightDoneTitle
Issue #2108ย ๐Ÿ’ช๐Ÿ”ดHave complete translation of the protocol K
Issue #212GC13ย ๐Ÿ’ช๐ŸŸขMerge fork branches
Issue #247?ย ๐Ÿ’ช๐ŸŸขVerify set
Issue #248?ย ๐Ÿ’ช๐ŸŸขVerify map
Issue #249NK?ย ๐Ÿ’ช๐ŸŸขVerify big_map
Issue #250?ย ๐Ÿ’ช๐ŸŸขVerify string
Issue #251?ย ๐Ÿ’ช๐ŸŸขVerify bytes
Issue #252GC?ย ๐Ÿ’ช๐ŸŸขVerify tez
Issue #253DH?ย ๐Ÿ’ช๐ŸŸขVerify arith
Issue #254DH?ย ๐Ÿ’ช๐ŸŸขVerify bool arith
Issue #255?ย ๐Ÿ’ช๐ŸŸขVerify compare
Issue #257?ย ๐Ÿ’ช๐Ÿ”ดVerify view
Issue #258?ย ๐Ÿ’ช๐Ÿ”ดVerify transfer
Issue #259DH?ย ๐Ÿ’ช๐ŸŸขVerify create contract
Issue #263?ย ๐Ÿ’ช๐ŸŸขVerify unpack
Issue #265?ย ๐Ÿ’ช๐Ÿ”ดVerify dig
Issue #266?ย ๐Ÿ’ช๐ŸŸขVerify voting
Issue #267BK?ย ๐Ÿ’ช๐ŸŸขVerify comb
Issue #268?ย ๐Ÿ’ช๐ŸŸขVerify ticket
Issue #269?ย ๐Ÿ’ช๐ŸŸขVerify continuation
Issue #296AK2ย ๐Ÿ’ช๐ŸŸขVerify Block_header_repr.v
Issue #309AK2ย ๐Ÿ’ช๐ŸŸขVerify Entrypoint_repr.v
Issue #317AK2ย ๐Ÿ’ช๐ŸŸขVerify Operation_repr.v
Issue #328SK2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_game_repr.v
Issue #363EM8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (2/14)
Issue #366BK8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (5/14)
Issue #367SK, BK8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (6/14)
Issue #368AK13ย ๐Ÿ’ช๐Ÿ”ดVerify backward-compatibility instructions (7/14)
Issue #369DH13ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (8/14)
Issue #370DH8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (9/14)
Issue #371BK?ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (10/14)
Issue #372AK8ย ๐Ÿ’ช๐Ÿ”ดVerify backward-compatibility instructions (11/14)
Issue #373NK8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (12/14)
Issue #374DH8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (13/14)
Issue #375DH8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (14/14)
Issue #380GC?ย ๐Ÿ’ช๐Ÿ”ดState lemma for backward compatibility on the interpreter with gas cost
Issue #381GC?ย ๐Ÿ’ช๐Ÿ”ดFinish porting the proofs to proto K

Sprint 6โ€‹

2022-08-03 - 2022-08-19

Done: 156/156

IssueAssignedWeightDoneTitle
Issue #286EM3ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_comparable.v
Issue #287EM1ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_family.v
Issue #288EM5ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_interpreter_defs.v
Issue #289DH5ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_interpreter.v
Issue #291DH2ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_map.v
Issue #295DH3ย ๐Ÿ’ช๐ŸŸขFix proofs in Script_typed_ir.v
Issue #296AK2ย ๐Ÿ’ช๐ŸŸขVerify Block_header_repr.v
Issue #2972ย ๐Ÿ’ช๐ŸŸขVerify Block_payload_repr.v
Issue #298AK2ย ๐Ÿ’ช๐ŸŸขVerify Bond_id_repr.v
Issue #2992ย ๐Ÿ’ช๐ŸŸขVerify Cache_repr.v
Issue #3002ย ๐Ÿ’ช๐ŸŸขVerify Commitment_repr.v
Issue #301AK2ย ๐Ÿ’ช๐ŸŸขVerify Constants_parametric_previous_repr.v
Issue #3052ย ๐Ÿ’ช๐ŸŸขVerify Cycle_repr.v
Issue #308AK2ย ๐Ÿ’ช๐ŸŸขVerify Destination_repr.v
Issue #309AK2ย ๐Ÿ’ช๐ŸŸขVerify Entrypoint_repr.v
Issue #310AK2ย ๐Ÿ’ช๐ŸŸขVerify Fitness_repr.v
Issue #311AK2ย ๐Ÿ’ช๐ŸŸขVerify Fixed_point_repr.v
Issue #312AK2ย ๐Ÿ’ช๐ŸŸขVerify Gas_limit_repr.v
Issue #313AK2ย ๐Ÿ’ช๐ŸŸขVerify Level_repr.v
Issue #3142ย ๐Ÿ’ช๐ŸŸขVerify Liquidity_baking_repr.v
Issue #3152ย ๐Ÿ’ช๐ŸŸขVerify Manager_repr.v
Issue #3162ย ๐Ÿ’ช๐ŸŸขVerify Migration_repr.v
Issue #317AK2ย ๐Ÿ’ช๐ŸŸขVerify Operation_repr.v
Issue #318SK2ย ๐Ÿ’ช๐ŸŸขVerify Parameters_repr.v
Issue #3192ย ๐Ÿ’ช๐ŸŸขVerify Period_repr.v
Issue #320SK2ย ๐Ÿ’ช๐ŸŸขVerify Ratio_repr.v
Issue #3212ย ๐Ÿ’ช๐ŸŸขVerify Raw_level_repr.v
Issue #3222ย ๐Ÿ’ช๐ŸŸขVerify Receipt_repr.v
Issue #3232ย ๐Ÿ’ช๐ŸŸขVerify Round_repr.v
Issue #3242ย ๐Ÿ’ช๐ŸŸขVerify Sapling_repr.v
Issue #3252ย ๐Ÿ’ช๐ŸŸขVerify Saturation_repr.v
Issue #3262ย ๐Ÿ’ช๐ŸŸขVerify Script_repr.v
Issue #3272ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_commitment_repr.v
Issue #328SK2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_game_repr.v
Issue #329SK2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_inbox_message_repr.v
Issue #330DH2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_inbox_repr.v
Issue #331DH2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_outbox_message_repr.v
Issue #332DH2ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_proof_repr.v
Issue #3332ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_repr.v
Issue #3342ย ๐Ÿ’ช๐ŸŸขVerify Sc_rollup_tick_repr.v
Issue #3352ย ๐Ÿ’ช๐ŸŸขVerify Seed_repr.v
Issue #336SK2ย ๐Ÿ’ช๐ŸŸขVerify Skip_list_repr.v
Issue #3372ย ๐Ÿ’ช๐ŸŸขVerify Slot_repr.v
Issue #3382ย ๐Ÿ’ช๐ŸŸขVerify Tez_repr.v
Issue #3392ย ๐Ÿ’ช๐ŸŸขVerify Ticket_hash_repr.v
Issue #3412ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_commitment_repr.v
Issue #3422ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_errors_repr.v
Issue #3432ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_inbox_repr.v
Issue #3442ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_level_repr.v
Issue #345SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_hash_repr.v
Issue #346SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_repr.v
Issue #347SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_result_hash_repr.v
Issue #348SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_message_result_repr.v
Issue #349SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_repr.v
Issue #350SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_reveal_repr.v
Issue #351SK2ย ๐Ÿ’ช๐ŸŸขVerify Tx_rollup_state_repr.v
Issue #359GC8ย ๐Ÿ’ช๐ŸŸขWrite migration for kinstr
Issue #360GC3ย ๐Ÿ’ช๐ŸŸขWrite migration for continuation
Issue #361GC2ย ๐Ÿ’ช๐ŸŸขWrite statement for backward-compatibility on continutations
Issue #362EM8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (1/14)
Issue #363EM8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (2/14)
Issue #364GC8ย ๐Ÿ’ช๐ŸŸขVerify backward-compatibility instructions (3/14)

Sprint 5โ€‹

2022-06-20 - 2022-08-01

Done: 85/117

IssueAssignedWeightDoneTitle
Issue #983ย ๐Ÿ’ช๐Ÿ”ดEncodings in ๐Ÿ—‚๏ธ Indexable.v
Issue #208EM5ย ๐Ÿ’ช๐ŸŸขFix OCaml compilation of the K branch for the protocol
Issue #209AK, EM8ย ๐Ÿ’ช๐ŸŸขFix translation to Coq of the K branch for the protocol
Issue #2108ย ๐Ÿ’ช๐Ÿ”ดHave complete translation of the protocol K
Issue #211DH8ย ๐Ÿ’ช๐ŸŸขHave complete translation of the protocol J
Issue #212GC13ย ๐Ÿ’ช๐ŸŸขMerge fork branches
Issue #213GC13ย ๐Ÿ’ช๐ŸŸขHave a shared environment
Issue #214SK3ย ๐Ÿ’ช๐ŸŸขDefinition simulation for dep_well_formed_entrypoints
Issue #215AK, NK, SK13ย ๐Ÿ’ช๐ŸŸขDefine simulation for parse_instr_aux
Issue #216AK3ย ๐Ÿ’ช๐ŸŸขDefine simulation for parse_view_returning
Issue #218RY1ย ๐Ÿ’ช๐ŸŸขDefine simulation for diff_of_big_map
Issue #219AK5ย ๐Ÿ’ช๐ŸŸขDefine simulation for parse_returning
Issue #220DH5ย ๐Ÿ’ช๐ŸŸขVerify simulation for diff_of_big_map
Issue #221SK5ย ๐Ÿ’ช๐Ÿ”ดVerify simulation for parse_returning
Issue #222SK3ย ๐Ÿ’ช๐Ÿ”ดVerify simulation for parse_view_returning
Issue #22313ย ๐Ÿ’ช๐Ÿ”ดVerify simulation for parse_instr_aux
Issue #224SK8ย ๐Ÿ’ช๐ŸŸขVerify simulation for dep_well_formed_entrypoints

Sprint 4โ€‹

2022-05-06 - 2022-06-17

Done: 48/140

IssueAssignedWeightDoneTitle
Issue #9013ย ๐Ÿ’ช๐ŸŸขVerify back_path_is_valid for skip lists
Issue #983ย ๐Ÿ’ช๐Ÿ”ดEncodings in ๐Ÿ—‚๏ธ Indexable.v
Issue #100NK5ย ๐Ÿ’ช๐ŸŸขEncodings in โš—๏ธ Liquidity_baking_repr.v
Issue #101NK3ย ๐Ÿ’ช๐ŸŸขEncodings in ๐Ÿง‘ Main.v
Issue #102NK3ย ๐Ÿ’ช๐ŸŸขEncodings in ๐Ÿ–ผ๏ธ Raw_context.v
Issue #117GC13ย ๐Ÿ’ช๐Ÿ”ดDefine all remaining cases for dep_step
Issue #11813ย ๐Ÿ’ช๐Ÿ”ดTerminate the proof of dep_step_eq
Issue #127EM8ย ๐Ÿ’ช๐ŸŸขVerify carbonated maps (3/3)
Issue #1358ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 20-29
Issue #137AK13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 40-49
Issue #138KH13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 50-59
Issue #139AK13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 60-69
Issue #140RY8ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 70-79
Issue #1418ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 80-89
Issue #161GC13ย ๐Ÿ’ช๐ŸŸขVerify the simulations in Script_set.v
Issue #173GC3ย ๐Ÿ’ช๐ŸŸขFix definition of arb_tez_sizes in test of Tez_repr

Sprint 3โ€‹

2022-05-06 - 2022-06-03

Done: 90/179

IssueAssignedWeightDoneTitle
Issue #83NK5ย ๐Ÿ’ช๐ŸŸขVerify encoding for skip lists
Issue #9013ย ๐Ÿ’ช๐ŸŸขVerify back_path_is_valid for skip lists
Issue #117GC13ย ๐Ÿ’ช๐Ÿ”ดDefine all remaining cases for dep_step
Issue #11813ย ๐Ÿ’ช๐Ÿ”ดTerminate the proof of dep_step_eq
Issue #122DH8ย ๐Ÿ’ช๐ŸŸขExpress predicate for internal errors
Issue #125EM3ย ๐Ÿ’ช๐ŸŸขVerify carbonated maps (1/3)
Issue #126EM5ย ๐Ÿ’ช๐ŸŸขVerify carbonated maps (2/3)
Issue #127EM8ย ๐Ÿ’ช๐ŸŸขVerify carbonated maps (3/3)
Issue #130SK2ย ๐Ÿ’ช๐ŸŸขInline dep_step auxiliary functions
Issue #133GC?ย ๐Ÿ’ช๐ŸŸขRemove abstract-large-number warnings from Proofs/Script_ir_translator.v
Issue #134KH5ย ๐Ÿ’ช๐ŸŸขTranslator simulations 10-19
Issue #1358ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 20-29
Issue #136KH8ย ๐Ÿ’ช๐ŸŸขTranslator simulations 30-39
Issue #137AK13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 40-49
Issue #138KH13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 50-59
Issue #139AK13ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 60-69
Issue #140RY8ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 70-79
Issue #1418ย ๐Ÿ’ช๐Ÿ”ดTranslator simulations 80-89
Issue #142GC5ย ๐Ÿ’ช๐ŸŸขTranslator simulations 90-99
Issue #161GC13ย ๐Ÿ’ช๐ŸŸขVerify the simulations in Script_set.v
Issue #162GC13ย ๐Ÿ’ช๐ŸŸขVerify the simulations in Script_map.v
Issue #170GC2ย ๐Ÿ’ช๐ŸŸขHave a predicate over the instructions