diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 22:20:38 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 22:20:38 +0100 |
| commit | 211cea99ccdb8f0798b81b4bf85859b01e0666db (patch) | |
| tree | 2ba098d8874e4ecefb1803514155c25b2539f5cd | |
| parent | ecd5a00f5a386a7993bf335f2b10d714f09e444b (diff) | |
| download | vericert-211cea99ccdb8f0798b81b4bf85859b01e0666db.tar.gz vericert-211cea99ccdb8f0798b81b4bf85859b01e0666db.zip | |
[sched] Add start to proof of sem_value_det
| -rw-r--r-- | src/hls/Abstr.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index a6b4505..c04b31c 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -748,6 +748,18 @@ Section CORRECT. Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx). + Lemma sem_value_det: + forall e v v', sem_value ictx e v -> sem_value octx e v' -> v = v'. + Proof. + induction e using expression_ind2 + with (P0 := fun p => forall v, sem_val_list ictx p v -> sem_val_list octx p v); + try solve [inversion 1]; + simplify; inv HSIM. + - inv H0. inv H. eauto. + - inv H0. inv H. simplify. + simplify. unfold ge_preserved in *; crush. + - inv H. simplify. econstructor. + Lemma check_correct_sem_value: forall x x' v v' n, beq_pred_expr n x x' = true -> |