Finished proof of spec completely

2 files changed, 94 insertions, 5 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 670dcd4..26dc630 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -142,6 +142,37 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
 
+Lemma add_instr_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       (AssocMap.add n st s.(st_datapath))
+       (AssocMap.add n Vskip s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               (AssocMap.add n st s.(st_datapath))
+               (AssocMap.add n Vskip s.(st_controllogic)))
+         (add_instr_skip_state_incr s n st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -285,9 +316,9 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
     | Ireturn r =>
       match r with
       | Some r' =>
-        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
       | None =>
-        add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z)))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z))))
       end
     end
   end.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index c8f1751..06ed68d 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -148,7 +148,8 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
+    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+                                                  (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
@@ -226,7 +227,15 @@ Lemma translate_instr_tr_op :
   forall op args s s' e i,
     translate_instr op args s = OK e s' i ->
     tr_op op args e.
-Admitted.
+Proof.
+  intros.
+  destruct op eqn:?; try (econstructor; apply H); try discriminate; simpl in *;
+    try (match goal with
+           [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
+           repeat (destruct args; try discriminate)
+         end);
+    monadInv H; constructor.
+Qed.
 
 Lemma iter_expand_instr_spec :
   forall l fin rtrn s s' i x,
@@ -241,7 +250,7 @@ Proof.
     destruct (peq pc pc1).
 
     + subst.
-      destruct instr1 eqn:?.
+      destruct instr1 eqn:?; try discriminate.
 
       * unfold add_instr in EQ.
         destruct (check_empty_node_datapath s1 pc1); try discriminate.
@@ -275,6 +284,55 @@ Proof.
 
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
+      * monadInv EQ.
+        inv_incr.
+        unfold add_branch_instr in EQ2.
+        destruct (check_empty_node_datapath s0 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s0 pc1); try discriminate.
+        inversion EQ2.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor.
+        apply EQ1.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+      * destruct o3 eqn:?.
+        unfold add_instr_skip in EQ.
+        destruct (check_empty_node_datapath s1 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+        inversion EQ.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. constructor.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+        unfold add_instr_skip in EQ.
+        destruct (check_empty_node_datapath s1 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+        inversion EQ.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. apply constructor.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
     + eapply IHl. apply EQ0. assumption.
       destruct H1. inversion H1. subst. contradiction.
       assumption.