proof for jumptable

1 files changed, 27 insertions, 1 deletions

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 661329e8..cc4ab686 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -1074,7 +1074,33 @@ Proof.
       * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
-      admit.
+      
+      (* BEGIN INVARIANT *)
+      fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite forallb_forall in IND_step_me.
+      assert (RB.ge (invs # pc') (Some inv_pc)) as GE.
+      {
+        apply relb_leb_correct.
+        specialize IND_step_me with (pc', Some inv_pc).
+        apply IND_step_me.
+        apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))).
+        eapply list_nth_z_in.
+        eassumption.
+      }
+      destruct (invs # pc'); cbn in *.
+      2: contradiction.
+      eapply rel_ge; eauto.
+      (* END INVARIANT *)
 
   - (* Ireturn *)
     destruct or as [arg | ].