diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-18 16:20:25 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-18 16:20:25 +0100 |
| commit | ec4f412f64b93d0bda18cd0f766eb0bf0fb93450 (patch) | |
| tree | dff40dfd65a12ab07ca0899539e3ae4a130f9e44 /src/hls/DVeriloggenproof.v | |
| parent | f2df2bfc1451cfe8c96403ad02afb9ec6626d189 (diff) | |
| download | vericert-ec4f412f64b93d0bda18cd0f766eb0bf0fb93450.tar.gz vericert-ec4f412f64b93d0bda18cd0f766eb0bf0fb93450.zip | |
More work on proof
Diffstat (limited to 'src/hls/DVeriloggenproof.v')
| -rw-r--r-- | src/hls/DVeriloggenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/DVeriloggenproof.v b/src/hls/DVeriloggenproof.v index 31cdfca..0d417db 100644 --- a/src/hls/DVeriloggenproof.v +++ b/src/hls/DVeriloggenproof.v @@ -262,7 +262,7 @@ Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed Lemma mod_params_equiv m : mod_args (transl_module m) = DHTL.mod_params m. Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed. -Lemma empty_stack_equiv m : empty_stack (transl_module m) = DHTL.empty_stack m. +Lemma empty_stack_equiv m : empty_stack (transl_module m) = DHTL.empty_stack m.(DHTL.mod_stk) m.(DHTL.mod_stk_len). Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed. Ltac rewrite_eq := rewrite mod_return_equiv |