diff options
| author | James Pollard <james@pollard.dev> | 2020-06-12 18:13:52 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-12 18:13:52 +0100 |
| commit | eacdec2dd13611f94fe12a41cf04cf38dc389092 (patch) | |
| tree | aef1f0e8d8688351bc0a0c882d2263f07dadac0e /src | |
| parent | a01219884ec78f6c32ed98b31587a66278e0cddc (diff) | |
| download | vericert-kvx-eacdec2dd13611f94fe12a41cf04cf38dc389092.tar.gz vericert-kvx-eacdec2dd13611f94fe12a41cf04cf38dc389092.zip | |
Fix broken proof.
Diffstat (limited to 'src')
| -rw-r--r-- | src/translation/HTLgenspec.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 57d2d87..57d7d62 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -433,8 +433,8 @@ Proof. Qed. Hint Resolve iter_expand_instr_spec : htlspec. -Lemma create_arr_inv : forall x y z a b c d, - create_arr x y z = OK (a, b) c d -> y = b. +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> y = b. Proof. inversion 1. reflexivity. Qed. @@ -454,14 +454,14 @@ Proof. monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN. + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. rewrite <- STK_LEN. econstructor; simpl; trivial. intros. inv_incr. assert (EQ3D := EQ3). - destruct x3. + destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. |