Finished all the proofsv1.0.0

Removed support for case statements temporarily.

3 files changed, 46 insertions, 39 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 87a6de6..68e0293 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -478,8 +478,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
         add_branch_instr e n n1 n2
       else error (Errors.msg "State is larger than 2^32.")
     | Ijumptable r tbl =>
-      do s <- get;
-      add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))
+      (*do s <- get;
+      add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)
+      error (Errors.msg "Ijumptable: Case statement not supported.")
     | Ireturn r =>
       match r with
       | Some r' =>
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 6664617..403a97f 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -2327,39 +2327,47 @@ Section CORRECTNESS.
   Proof.
     intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE.
     inv_state.
-
-    eexists. split. apply Smallstep.plus_one.
-    eapply HTL.step_module; eauto.
-    inv CONST; assumption.
-    inv CONST; assumption.
-(*    eapply Verilog.stmnt_runp_Vnonblock_reg with
-        (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
-    constructor.
-
-    simpl.
     destruct b.
-    eapply Verilog.erun_Vternary_true.
-    eapply eval_cond_correct; eauto.
-    constructor.
-    apply boolToValue_ValueToBool.
-    eapply Verilog.erun_Vternary_false.
-    eapply eval_cond_correct; eauto.
-    constructor.
-    apply boolToValue_ValueToBool.
-    constructor.
+    - eexists. split. apply Smallstep.plus_one.
+      clear H33.
+      eapply HTL.step_module; eauto.
+      inv CONST; assumption.
+      inv CONST; assumption.
+      econstructor; simpl; trivial.
+      constructor; trivial.
+      eapply Verilog.erun_Vternary_true; simpl; eauto.
+      eapply eval_cond_correct; eauto. intros.
+      intros. eapply RTL.max_reg_function_use. apply H22. auto.
+      econstructor. auto.
+      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      apply AssocMap.gss.
 
-    big_tac.
+      inv MARR. inv CONST.
+      big_tac.
+      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
+    - eexists. split. apply Smallstep.plus_one.
+      clear H32.
+      eapply HTL.step_module; eauto.
+      inv CONST; assumption.
+      inv CONST; assumption.
+      econstructor; simpl; trivial.
+      constructor; trivial.
+      eapply Verilog.erun_Vternary_false; simpl; eauto.
+      eapply eval_cond_correct; eauto. intros.
+      intros. eapply RTL.max_reg_function_use. apply H22. auto.
+      econstructor. auto.
+      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      apply AssocMap.gss.
 
-    invert MARR.
-    destruct b; rewrite assumption_32bit; big_tac.
+      inv MARR. inv CONST.
+      big_tac.
+      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
 
-    Unshelve.
-    constructor.
-  Qed.*)
-  Admitted.
+      Unshelve. all: exact tt.
+  Qed.
   Hint Resolve transl_icond_correct : htlproof.
 
-  Lemma transl_ijumptable_correct:
+  (*Lemma transl_ijumptable_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
       (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node)
       (n : Integers.Int.int) (pc' : RTL.node),
@@ -2372,8 +2380,8 @@ Section CORRECTNESS.
           Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
   Proof.
     intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
-  Admitted.
-  Hint Resolve transl_ijumptable_correct : htlproof.
+  
+  Hint Resolve transl_ijumptable_correct : htlproof.*)
 
   Lemma transl_ireturn_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
@@ -2674,5 +2682,3 @@ Section CORRECTNESS.
   Qed.
 
 End CORRECTNESS.
-
-Check transl_step_correct.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 93d5612..541f9fa 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -147,11 +147,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
-               (state_goto st n)
-| tr_instr_Ijumptable :
+               (state_goto st n).
+(*| tr_instr_Ijumptable :
     forall cexpr tbl r,
     cexpr = tbl_to_case_expr st tbl ->
-    tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).
+    tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*)
 Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
@@ -446,7 +446,7 @@ Proof.
   - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
   - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
     congruence.
-  - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.
+  (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*)
 Qed.
 Hint Resolve transf_instr_freshreg_trans : htlspec.
 
@@ -551,12 +551,12 @@ Proof.
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.
 
-    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + inversion H2.
       * inversion H14. constructor. congruence.
       * apply in_map with (f := fst) in H14. contradiction.
-
+      *)
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + inversion H2.