1 files changed, 22 insertions, 17 deletions
diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v
index 5a1c5acf..b0cf0879 100644
--- a/backend/FirstNopproof.v
+++ b/backend/FirstNopproof.v
@@ -178,23 +178,28 @@ Proof.
       apply eval_operation_preserved.
       apply symbols_preserved.
     + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
-      all: rewrite <- H0.
-      all: auto using eval_addressing_preserved, symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
+  - left. inv H0.
+    + econstructor. split.
+      * eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
+        eapply has_loaded_normal; eauto.
+        all: rewrite <- EVAL.
+        all: auto using eval_addressing_preserved, symbols_preserved.
+      * constructor; auto with firstnop.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v). econstructor; split.
+        -- eapply plus_one. eapply exec_Iload; eauto with firstnop.
+           eapply has_loaded_default; eauto.
+           all:
+           rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved];
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto.
+        -- constructor; auto with firstnop.
+      * econstructor; split.
+        -- eapply plus_one. eapply exec_Iload; eauto with firstnop.
+           eapply has_loaded_default; eauto.
+           all:
+           rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved];
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto.
+        -- constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Istore; eauto with firstnop.
       all: rewrite <- H0;