draft: try Unpack instruction

formal-land · Dec 24, 2024 · d909741 · d909741
1 parent 610a67b
commit d909741
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -779,9 +779,21 @@ Proof.
     admit.
   }
   { guard_instruction (Bytecode.Unpack t).
+    unfold_state_monad.
+    destruct CompiledModule.struct_def_at; cbn; trivial.
+    destruct H_type_safety_checker as [H_stack].
+    destruct type_safety_checker; cbn in *.
+    unfold set; cbn.
+    pose proof (AbstractStack.pop_is_valid stack H_stack).
+    destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
+    unfold safe_unwrap_err.
+    step; cbn; trivial.
+    step; cbn; trivial.
+    (* FOLD Issue *)
     admit.
   }
   { guard_instruction (Bytecode.UnpackGeneric t).
+
     admit.
   }
   { guard_instruction Bytecode.ReadRef.