Complete HTLspec (mostly)

1 files changed, 64 insertions, 34 deletions

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