diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-01 09:11:43 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-01 09:11:43 +0000 |
| commit | 0bc9bc9f6318a820352a1af1f3ec8f7d7d4a1821 (patch) | |
| tree | 8d1ab56b56f15429ba82e9ea6f78605a7379a197 | |
| parent | c50b4607f501a991e18088f75d04ff6d5bce66a8 (diff) | |
| download | vericert-0bc9bc9f6318a820352a1af1f3ec8f7d7d4a1821.tar.gz vericert-0bc9bc9f6318a820352a1af1f3ec8f7d7d4a1821.zip | |
Add Admitted theorems for existence proofs
| -rw-r--r-- | src/hls/Abstr.v | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index d1b008e..abc4181 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1341,18 +1341,11 @@ Section CORRECT. End SEM_PRED_CORR. - Inductive match_instr_state : instr_state -> instr_state -> Prop := - | match_instr_state_intro : forall i1 i2, - is_mem i1 = is_mem i2 -> - (forall x, (is_rs i1) !! x = (is_rs i2) !! x) -> - (forall x, (is_ps i1) !! x = (is_ps i2) !! x) -> - match_instr_state i1 i2. - Lemma check_correct: forall (fa fb : forest) i i', check fa fb = true -> sem ictx fa i -> sem octx fb i' -> - match_instr_state i i'. + match_states i i'. Proof using HSIM. intros. unfold check, get_forest in *; intros; @@ -1378,7 +1371,7 @@ Admitted. forall (fa fb : forest) i, check fa fb = true -> sem ictx fa i -> - exists i', sem octx fb i' /\ match_instr_state i i'. + exists i', sem octx fb i' /\ match_states i i'. Proof. Admitted. End CORRECT. |