diff options
| author | James Pollard <james@pollard.dev> | 2020-06-22 17:15:29 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-22 17:15:29 +0100 |
| commit | be6ad3cd886b3ea79abe6addc2f2add779f55292 (patch) | |
| tree | 2c17b96f3fa650e7dcc1f14f2dccde990df5d54d /src/translation/HTLgenspec.v | |
| parent | e05b93c540d2e0e2cb9f4ab01460eba080b65401 (diff) | |
| download | vericert-kvx-be6ad3cd886b3ea79abe6addc2f2add779f55292.tar.gz vericert-kvx-be6ad3cd886b3ea79abe6addc2f2add779f55292.zip | |
Tidy up proof for Aindexed2scaled.
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a916cb5..528c662 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -189,6 +189,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) -> m = (mkmodule f.(RTL.fn_params) data control @@ -452,7 +453,11 @@ Proof. inversion s; subst. unfold transf_module in *. - destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND; + destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; + simplify; + monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. |