From 1ca4288064dcf9759c06f30b06b415dc7b4e45a1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 13 Nov 2021 23:01:53 +0000
Subject: Small progress on the proof of correctness

---
 src/hls/RTLPargenproof.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index df0615a..588f67f 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -742,7 +742,11 @@ Lemma sem_update :
   match_states st' st''' ->
   @step_instr A ge sp st''' x st'' ->
   exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst.
-Proof. Admitted.
+Proof.
+  intros. destruct x.
+  - inv H1. econstructor. simplify. eauto. symmetry; auto.
+  - inv H1. inv H0. econstructor.
+    Admitted.
 
 Lemma rtlblock_trans_correct :
   forall bb ge sp st st',
-- 
cgit