Complete HTLspec (mostly)

3 files changed, 133 insertions, 52 deletions

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 0fae032..84c272b 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -218,7 +218,9 @@ Ltac liapp :=
          | _ => idtac
          end.
 
-Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
+Ltac plia := solve [ unfold Ple in *; lia ].
+
+Ltac crush := simplify; try discriminate; try congruence; try plia; liapp;
               try assumption; try (solve [auto]).
 
 Ltac crush_trans :=
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index a979a40..c63847a 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -21,6 +21,7 @@ Require Import Coq.micromega.Lia.
 
 Require Import compcert.lib.Maps.
 Require compcert.common.Errors.
+Require Import compcert.lib.Integers.
 Require compcert.common.Globalenvs.
 Require compcert.lib.Integers.
 Require Import compcert.common.AST.
@@ -81,20 +82,40 @@ Module HTLState <: State.
     map_incr st_datapath s1 s2 ->
     map_incr st_controllogic s1 s2 ->
     map_incr st_externctrl s1 s2 ->
+    (forall n, (st_externctrl s1) ! n = None ->
+          (exists x, (st_externctrl s2) ! n = Some x) ->
+          (n >= st_freshreg s1)%positive) ->
     st_incr s1 s2.
   Hint Constructors st_incr : htlh.
 
   Definition st_prop := st_incr.
   Hint Unfold st_prop : htlh.
 
-  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
+  Lemma st_refl : forall s, st_prop s s.
+  Proof. split; try solve [ auto with htlh; crush ]. Qed.
 
   Lemma st_trans :
     forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
   Proof.
-    intros. inv H. inv H0.
-    apply state_incr_intro; autounfold with htlh in *;
-      eauto using Ple_trans; intros; try congruence; specialize_all n; intuition congruence.
+    intros * H0 H1. inv H0. inv H1.
+    split; autounfold with htlh in *; intros; try solve [crush].
+    - destruct H4 with n; destruct H10 with n; intuition crush.
+    - destruct H5 with n; destruct H11 with n; intuition crush.
+    - destruct H6 with n; destruct H12 with n; intuition crush.
+    - destruct H6 with n; destruct H12 with n.
+      + specialize (H13 n ltac:(auto) ltac:(auto)).
+        crush.
+      + apply H7; auto.
+        rewrite <- H16.
+        auto.
+      + specialize (H13 n ltac:(auto) ltac:(auto)).
+        unfold Ple in *.
+        lia.
+      + contradict H14.
+        rewrite H16.
+        rewrite H15.
+        rewrite H1.
+        intuition crush.
   Qed.
 
 End HTLState.
@@ -153,23 +174,23 @@ Local Ltac st_tac :=
   match goal with
   | [ H : (?map ?s) ! ?n = None, n' : positive |- _] => destruct (peq n n')
   end;
-  subst; auto with htlh.
+  subst; auto with htlh; intuition crush.
 
 Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
   fun s => OK tt (mkstate
-                     (st_st s)
-                     (st_freshreg s)
-                     (st_freshstate s)
-                     (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
-                     (st_arrdecls s)
-                     (st_externctrl s)
-                     (st_datapath s)
-                     (st_controllogic s)) ltac:(st_tac).
+             (st_st s)
+             (st_freshreg s)
+             (st_freshstate s)
+             (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+             (st_arrdecls s)
+             (st_externctrl s)
+             (st_datapath s)
+             (st_controllogic s)) ltac:(st_tac).
 
 Definition create_reg (i : option io) (sz : nat) : mon reg :=
   fun s => let r := s.(st_freshreg) in
         OK r (mkstate
-            s.(st_st)
+            (st_st s)
             (Pos.succ r)
             (st_freshstate s)
             (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
@@ -178,34 +199,43 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
             (st_datapath s)
             (st_controllogic s)) ltac:(st_tac).
 
-Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg :=
-  do r <- create_reg None (controlsignal_sz ctrl);
-  fun s => match check_unmapped_externctrl s r with
-        | left CTRL => OK r (mkstate
+Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg.
+  refine (
+  fun s => match check_unmapped_externctrl s (st_freshreg s) with
+        | left CTRL => OK (st_freshreg s) (mkstate
                           (st_st s)
                           (st_freshreg s)
                           (st_freshstate s)
                           (st_scldecls s)
                           (st_arrdecls s)
-                          (AssocMap.set r (othermod, ctrl) (st_externctrl s))
+                          (AssocMap.set (st_freshreg s) (othermod, ctrl) (st_externctrl s))
                           (st_datapath s)
-                          (st_controllogic s)) ltac:(st_tac)
+                          (st_controllogic s)) _
         | right CTRL => Error (Errors.msg "HTL.map_externctrl")
-        end.
+        end).
+  st_tac.
+  rewrite PTree.gsspec in *.
+  destruct_match; crush.
+Defined.
+
+Definition create_state : mon node.
+  refine (fun s => let r := s.(st_freshstate) in
+                if Z.leb (Z.pos s.(st_freshstate)) Integers.Int.max_unsigned
+                then OK r (mkstate
+                         (st_st s)
+                         (st_freshreg s)
+                         (Pos.succ (st_freshstate s))
+                         (st_scldecls s)
+                         (st_arrdecls s)
+                         (st_externctrl s)
+                         (st_datapath s)
+                         (st_controllogic s)) _
+                else Error (Errors.msg "HTL.create_state")).
+  split; autounfold with htlh; crush.
+Defined.
 
-Definition create_state : mon node :=
-  fun s => let r := s.(st_freshstate) in
-        if Z.leb (Z.pos s.(st_freshstate)) Integers.Int.max_unsigned
-        then OK r (mkstate
-                 s.(st_st)
-                 (st_freshreg s)
-                 (Pos.succ (st_freshstate s))
-                 (st_scldecls s)
-                 (st_arrdecls s)
-                 (st_externctrl s)
-                 (st_datapath s)
-                 (st_controllogic s)) ltac:(st_tac)
-        else Error (Errors.msg "HTL.create_state").
+Lemma create_state_max : forall s s' i x, create_state s = OK x s' i -> Z.pos x <= Int.max_unsigned.
+Admitted.
 
 Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit :=
   fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index b666620..21de6bd 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -137,7 +137,7 @@ Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop :=
       (start > stk)%positive ->
       (rst > start)%positive ->
       (clk > rst)%positive ->
-      (forall r, (exists x, externctrl!r = Some x) -> (r > clk)%positive) ->
+      (forall n, (exists x, externctrl!n = Some x) -> (n > clk)%positive) ->
       tr_module ge f m.
 Hint Constructors tr_module : htlspec.
 
@@ -265,7 +265,6 @@ Ltac trans_step s1 s2 :=
 
 (* Try to prove a goal about a state by first proving it for an earlier state and then transfering it to the final. *)
 Ltac monad_crush :=
-  crush;
   match goal with
   | [ finalstate : st, prevstate : st |- _] =>
     match goal with
@@ -284,7 +283,7 @@ Ltac monad_crush :=
 
 Ltac full_split := repeat match goal with [ |- _ /\ _ ] => split end.
 
-Ltac some_monad_inv :=
+Ltac relevant_monad_inv :=
   multimatch goal with
   | [ EQ : _ ?s = OK ?x _ _ |- context[?x] ] => monadInv EQ
   | [ EQ : _ ?s = OK (?x, _) _ _ |- context[?x] ] => monadInv EQ
@@ -292,6 +291,12 @@ Ltac some_monad_inv :=
   | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ
   end.
 
+Ltac any_monad_inv :=
+  relevant_monad_inv +
+  multimatch goal with
+  | [ EQ : _ ?s = OK _ _ _ |- _ ] => monadInv EQ
+  end.
+
 Ltac some_incr :=
   saturate_incr;
   multimatch goal with
@@ -327,7 +332,7 @@ Proof.
   induction args.
   - sauto use: nth_error_nil.
   - destruct n; intros * ? * H; monadInv H.
-    + eexists. monad_crush.
+    + eexists. crush. monad_crush.
     + sauto.
 Qed.
 
@@ -382,19 +387,26 @@ Proof.
       destruct (map_externctrl_params_combine _ _ _ _ _ _ EQ1) as [? [? ?]]; subst.
       repeat (eapply ex_intro).
 
-      repeat split; try monad_crush. (* slow *)
+      repeat split; try crush; try monad_crush; eauto with htlspec. (* slow *)
       * intros.
         destruct (map_externctrl_params_spec _ _ _ _ _ _ _ _ EQ1 ltac:(eauto)) as [param [? ?]].
-        exists param; crush; trans_step s3 s'.
-      * admit. (* (* FIXME: Causes Qed to hang *) monadInv EQ2. crush. *)
+        exists param; simplify; eauto; trans_step s3 s'.
+      * eapply create_state_max; eassumption.
+      * replace x5 with (st_freshreg s6) in * by intro_step.
+        monad_crush.
+      * replace x6 with (st_freshreg s7) in * by intro_step.
+        replace x5 with (st_freshreg s6) in * by intro_step.
+        monad_crush.
+      * replace x4 with (st_freshreg s5) in * by intro_step.
+        monad_crush.
     + (* Icond *) tr_code_simple_tac.
     + (* Ireturn *)
       inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction].
       inversion H.
-      eapply tr_code_return; crush; eexists; monad_crush.
+      eapply tr_code_return; crush; eexists; simplify; monad_crush.
   - eapply IHl; eauto.
     intuition crush.
-Admitted.
+Qed.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
 Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A),
@@ -415,10 +427,12 @@ Proof.
     * trans_step s s'.
     * inversion Htrans.
       destruct H6 with pc. crush.
-      rewrite H11. eauto.
+      replace ((st_datapath s') ! pc).
+      eassumption.
     * inversion Htrans.
       destruct H7 with pc. crush.
-      rewrite H11. eauto.
+      replace ((st_controllogic s') ! pc).
+      eassumption.
     * inversion Htrans. crush.
   + eapply tr_code_call; eauto with htlspec.
     simplify.
@@ -453,6 +467,19 @@ Proof.
 Qed.
 Hint Resolve declare_params_freshreg_trans : htlspec.
 
+Lemma declare_params_externctrl_trans : forall params s s' x i,
+    declare_params params s = OK x s' i ->
+    st_externctrl s = st_externctrl s'.
+Proof.
+  induction params; unfold declare_params in *; intros * H.
+  - inv H. trivial.
+  - monadInv H.
+    transitivity (st_externctrl s0).
+    + monadInv EQ. auto.
+    + eauto.
+Qed.
+Hint Resolve declare_params_freshreg_trans : htlspec.
+
 Theorem transl_module_correct :
   forall p f m,
     transl_module p f = Errors.OK m -> tr_module (Globalenvs.Genv.globalenv p) f m.
@@ -478,10 +505,32 @@ Proof.
 
   econstructor;
     eauto with htlspec;
-    try solve [ repeat some_monad_inv; crush ].
+    try solve [ repeat relevant_monad_inv; crush ].
   - auto_apply declare_params_freshreg_trans.
-    some_monad_inv; monad_crush.
-  - (* forall r, (exists x, externctrl!r = Some x) -> (r >= clk)%positive *)
-    (* Problematic because it does not cover  *)
-    admit.
-Admitted.
+    replace (st_st s').
+    monadInv EQ1.
+    inversion INCR.
+    repeat match goal with
+           | [ H : context[st_freshreg (max_state _)] |- _ ] => unfold max_state in H; simpl in H
+           end.
+    crush.
+  - assert (forall n, (st_externctrl (max_state f)) ! n = None) by (simplify; eauto using AssocMap.gempty).
+    assert (forall n, (st_externctrl s0) ! n = None) by (erewrite <- (declare_params_externctrl_trans); eauto).
+    assert (forall n, (st_externctrl s1) ! n = None) by (any_monad_inv; simplify; auto).
+    assert (forall n, (st_externctrl s2) ! n = None) by (any_monad_inv; simplify; auto).
+    assert (forall n, (st_externctrl s3) ! n = None) by (any_monad_inv; simplify; auto).
+    assert (forall n, (st_externctrl s4) ! n = None) by (any_monad_inv; simplify; auto).
+    assert (forall n, (st_externctrl s5) ! n = None) by (any_monad_inv; simplify; auto).
+
+    assert (forall n, (st_externctrl s6) ! n = None) by (any_monad_inv; simplify; auto).
+    assert ((st_freshreg s6) > x6)%positive by (relevant_monad_inv; simplify; crush).
+
+    intros.
+    repeat match goal with
+           | [ H: forall (_ : positive), _ |- _ ] => specialize (H r)
+           end.
+
+    enough (n >= st_freshreg s6)%positive by lia.
+    inversion INCR13.
+    auto.
+Qed.