No admitted in Deterministic proof

3 files changed, 10 insertions, 14 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 27eb9e5..51c0fa1 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -513,8 +513,8 @@ Section CORRECTNESS.
       eapply H2 in ARCH. apply ARCH.
       pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2.
       eapply H2 in ARCH. apply ARCH.
-    - admit.
-    - admit.
+    - admit. (* mulhs *)
+    - admit. (* mulhu *)
     - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
     - rewrite Heqb in Heqb0. discriminate.
     - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 2718a46..af2b822 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -468,7 +468,7 @@ Qed.
 
 Lemma ZToValue_eq :
   forall w1,
-  (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted.
+  (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort.
 
 Lemma wordsize_32 :
   Int.wordsize = 32%nat.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 9659189..78b057d 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -245,7 +245,7 @@ Definition program := AST.program fundef unit.
 Definition posToLit (p : positive) : expr :=
   Vlit (posToValue p).
 
-Definition fext := assocmap.
+Definition fext := unit.
 Definition fextclk := nat -> fext.
 
 (** ** State
@@ -345,10 +345,6 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       expr_runp fext reg stack iexp i ->
       arr_assocmap_lookup stack r (valueToNat i) = Some v ->
       expr_runp fext reg stack (Vvari r iexp) v
-  | erun_Vinputvar :
-      forall fext reg stack r v,
-      fext!r = Some v ->
-      expr_runp fext reg stack (Vinputvar r) v
   | erun_Vbinop :
       forall fext reg stack op l r lv rv resv,
       expr_runp fext reg stack l lv ->
@@ -391,11 +387,11 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-Definition access_fext (f : fext) (r : reg) : res value :=
+(*Definition access_fext (f : fext) (r : reg) : res value :=
   match AssocMap.get r f with
   | Some v => OK v
   | _ => OK (ZToValue 0)
-  end.
+  end.*)
 
 (* TODO FIX Vvar case without default *)
 (*Fixpoint expr_run (assoc : assocmap) (e : expr)
@@ -650,11 +646,11 @@ Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat
 assumed to be the starting state of the module, and may have to be changed if
 other arguments to the module are also to be supported. *)
 
-Definition initial_fextclk (m : module) : fextclk :=
+(*Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
            | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap)
            | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap)
-           end.
+           end.*)
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=
   mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
@@ -886,11 +882,11 @@ Lemma semantics_determinate :
 Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
   - invert H; invert H0; constructor. (* Traces are always empty *)
-  - invert H; invert H0; crush. assert (f = f0) by admit; subst.
+  - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
     pose proof (mis_stepp_determinate H5 H15).
     crush.
   - constructor. invert H; crush.
   - invert H; invert H0; unfold ge0, ge1 in *; crush.
   - red; simplify; intro; invert H0; invert H; crush.
   - invert H; invert H0; crush.
-Admitted.
+Qed.