diff options
| author | James Pollard <james@pollard.dev> | 2020-07-02 16:38:23 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-02 16:38:23 +0100 |
| commit | cf19dd40f466691d28f4dfd86211724b700aa217 (patch) | |
| tree | fc758531cbfc1e16e1c50b2669dba3489cfeb9bb /src | |
| parent | fc51e46012219e9410931820ef7c0612734620aa (diff) | |
| download | vericert-kvx-cf19dd40f466691d28f4dfd86211724b700aa217.tar.gz vericert-kvx-cf19dd40f466691d28f4dfd86211724b700aa217.zip | |
Fix callstate proof.
Diffstat (limited to 'src')
| -rw-r--r-- | src/translation/HTLgenproof.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9b61b27..e4bbb8f 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -2023,9 +2023,9 @@ Section CORRECTNESS. unfold Mem.load. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. small_tac. exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. @@ -2039,11 +2039,11 @@ Section CORRECTNESS. unfold Mem.store. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. small_tac. - exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. + exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. crush. |