From 9a9a6510ab9a3bf7b17093501584bc06ea0e4dfd Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 20 Apr 2022 12:29:55 +0100
Subject: Start work on Inop proof

---
 src/hls/RTLBlockgenproof.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index e33e3a3..d62ccf9 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -230,6 +230,9 @@ Section CORRECTNESS.
                /\ match_states (RTL.State s f sp pc' rs m) s2'.
   Proof.
     intros s f sp pc rs m pc' H.
+    inversion 1; simplify. inv H1. inv H0. inv BB0.
+    inv PC0.
+    -
   Admitted.
 
   Lemma transl_Iop_correct:
-- 
cgit