Merge pull request #600 from formal-land/gy@Interpreter

`interpreter` simulation, Part 1

CoqOfRust/move_sui/simulations/move_binary_format/errors.v

@@ -10,9 +10,6 @@ Module IndexKind := move_binary_format.lib.IndexKind.
 (* TODO(progress):
   - Rewrite `mut` functions with `StatePanic` monads, for example `at_code_offset`. 
     Maybe implement Lens for `PartialVMError`. See the NOTE there
-  - Mutual dependency issue: only make copies of `PartialVMError` 
-    and `PartialVMResult` at the `file_format`'s side since it's 
-    relatively smaller
 *)
 
 Require CoqOfRust.move_sui.simulations.move_binary_format.file_format.

CoqOfRust/move_sui/simulations/move_binary_format/file_format.v

@@ -9,10 +9,6 @@ Require Import CoqOfRust.core.simulations.eq.
 Require CoqOfRust.move_sui.simulations.move_core_types.vm_status.
 Module StatusCode := vm_status.StatusCode.
 
-(* TODO(misc tasks):
-- See if we need to handle the `?` and debugs with `panic` monad. See NOTEs everywhere
-*)
-
 (* NOTE(MUTUAL DEPENDENCY ISSUE): This is just a stub to fill in needed information
   to use else where. When other files are using this type, they should have to
   extract the `StatusCode` and construct the actual PartialVMError by themselves. *)
@@ -1286,8 +1282,6 @@ Module CompiledModule.
         let ability := List.nth (Z.to_nat idx) constraints default_ability in
         Result.Ok ability
 
-      (* NOTE: belows are cases that are slightly more complicated,
-          since they involves `?`... *)
       | SignatureToken.Vector ty => 
       let abilities_result := abilities self ty constraints in
         match abilities_result with
@@ -1327,7 +1321,6 @@ Module CompiledModule.
           | Result.Ok  type_arguments =>
               AbilitySet.Impl_AbilitySet.polymorphic_abilities
                 declared_abilities is_phantom_list type_arguments
-          (* NOTE: maybe handle with a panic? *)
           | Result.Err err            => Result.Err err
           end
       end.

CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v

@@ -49,15 +49,15 @@ Module AbstractStack := move_abstract_stack.lib.AbstractStack.
 Require CoqOfRust.move_sui.simulations.move_bytecode_verifier_meter.lib.
 Module Scope := move_bytecode_verifier_meter.lib.Scope.
 (* NOTE: For now we just simplify `Meter` to the actual `BoundMeter` struct
-   since it's the only implementation that contains useful logic *)
+   since it's the only implementation that contains useful logic 
+   To modify the actual instance of `Meter`, we might need to:
+   1. Create a separate file `include.v`
+   2. Import dependencides in that `include` file
+   3. Define the `Meter` instance as the instance you want
+   4. Import the `include`'s instance into this file
+   *)
 Module Meter := move_bytecode_verifier_meter.lib.Meter.BoundMeter.
 
-(* TODO(progress):
-  - Integrate the new monad into this simulation:
-    - Check `safe_unwrap_err` propagation
-    - Check for sole `if` clauses, `Err`s has been *correctly* propagated to the end
-*)
-
 (* DRAFT: template for adding trait parameters *)
 (* Definition test_0 : forall (A : Set), { _ : Set @ Meter.Trait A } -> A -> Set. Admitted. *)
 

CoqOfRust/move_sui/simulations/move_bytecode_verifier_meter/lib.v

@@ -11,13 +11,6 @@ Module PartialVMError := errors.PartialVMError.
 Require CoqOfRust.move_sui.simulations.move_core_types.vm_status.
 Module StatusCode := vm_status.StatusCode.
 
-(* TODO(progress):
-- Investigate the exact function chains from `verify_instr` 
-  - Explain when will other verify functions use `verify_instr`
-  - Examine further if `DummyMeter` can be safely replaced by `BoundMeter`
-  - Carefully check where does `DummyMeter` apply and what properties or functions are being accessed
- *)
-
 (* NOTE: 
 - We can restructure the `Meter` into a large module, since its content are pretty few.
   Currently we implement the structs as the following tree: