Finishe load error case in model_E1E2_L3_orutt_strict.

vellvm · Jun 28, 2023 · ee14219 · ee14219
1 parent 0e7e6bd
commit ee14219
Showing 1 changed file with 0 additions and 10 deletions.
diff --git a/src/coq/Semantics/InfiniteToFinite.v b/src/coq/Semantics/InfiniteToFinite.v
@@ -15183,13 +15183,6 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
       rewrite H.
       exists x. exists ms_inf.
       split; cbn; auto.
-
-      assert (length a_inf = length a_fin) as LEN.
-      { eapply Util.Forall2_length; eauto.
-      }
-
-      apply read_bytes_spec_length in RBS.
-      lia.
   Qed.
 
   (* TODO: Move to where the other frame stack lemmas are *)
@@ -16466,9 +16459,6 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
                         pose proof Heqs as DESER_INF.
                         eapply deserialize_sbytes_fail_fin_inf in DESER_INF.
                         2: apply H0.
-                        2: {
-                          admit. (* Length / sizeof stuff... *)
-                        }
 
                         exists msg.
                         split; [reflexivity|].