diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 14:09:54 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-06 14:09:54 +0100 |
commit | 78e549331ba3f136ebe94955f68767bd384df454 (patch) | |
tree | e82c58fc59b6b4b1e9472cf26ce35ce0e6efdf14 /src/verilog | |
parent | c76ac9be323e3513aa0db2721ecd0f6c3987aef0 (diff) | |
download | vericert-kvx-78e549331ba3f136ebe94955f68767bd384df454.tar.gz vericert-kvx-78e549331ba3f136ebe94955f68767bd384df454.zip |
HTLgenproof compiles again
- Commented out Iload, Istore proofs for now
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/HTL.v | 6 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 12 |
2 files changed, 11 insertions, 7 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 3ba5b59..b3d1442 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -141,8 +141,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 064474a..9659189 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -736,8 +736,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g res m args, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) - (init_params args m.(mod_args))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) + (init_params args m.(mod_args))))) (empty_stack m)) | step_return : forall g m asr i r sf pc mst asa, @@ -884,9 +886,9 @@ Lemma semantics_determinate : Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. - (*pose proof (mis_stepp_determinate H4 H13)*) - admit. + - invert H; invert H0; crush. assert (f = f0) by admit; subst. + pose proof (mis_stepp_determinate H5 H15). + crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. - red; simplify; intro; invert H0; invert H; crush. |