diff options
author | James Pollard <james@pollard.dev> | 2020-06-01 16:08:56 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-01 16:08:56 +0100 |
commit | 41f1832503686a6afdd1a82b761c19679611426a (patch) | |
tree | 9aa99cdb81ad31636435ae2141088fd341235f7e | |
parent | c3fe9469171bbf706dcb7bc84297123590377100 (diff) | |
parent | 71ba686359b9cdf2178d0837552fc564a905b18f (diff) | |
download | vericert-kvx-41f1832503686a6afdd1a82b761c19679611426a.tar.gz vericert-kvx-41f1832503686a6afdd1a82b761c19679611426a.zip |
Merge branch 'develop' into arrays-proof
-rw-r--r-- | src/translation/HTLgenspec.v | 9 | ||||
-rw-r--r-- | src/verilog/HTL.v | 23 |
2 files changed, 19 insertions, 13 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 713a373..7cc0861 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -350,10 +350,9 @@ Proof. econstructor; simpl; trivial. intros. inv_incr. - assert (st_controllogic s8 = st_controllogic s2) by congruence. - rewrite <- H10. - assert (st_datapath s8 = st_datapath s2) by congruence. - assert (st_st s5 = st_st s2) by congruence. - rewrite H80. rewrite H81. rewrite H82. + assert (STC: st_controllogic s8 = st_controllogic s2) by congruence. + assert (STD: st_datapath s8 = st_datapath s2) by congruence. + assert (STST: st_st s8 = st_st s2) by congruence. + rewrite STC. rewrite STD. rewrite STST. eauto with htlspec. Qed. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index a21064c..fffbb81 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -47,10 +47,13 @@ Record module: Type := mod_return : reg }. +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + (** * Operational Semantics *) -Definition genv := Globalenvs.Genv.t unit unit. -Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil. +Definition genv := Globalenvs.Genv.t fundef unit. Inductive state : Type := | State : @@ -84,15 +87,19 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := step g (State m st assoc) t (Returnstate retval). Hint Constructors step : htl. -Inductive initial_state (m : module) : state -> Prop := -| initial_state_intro : forall st, - st = m.(mod_entrypoint) -> - initial_state m (State m st empty_assocmap). +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 st m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + st = m.(mod_entrypoint) -> + initial_state p (State m st empty_assocmap). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, value_int_eqb retval retvali = true -> final_state (Returnstate retval) retvali. -Definition semantics (m : module) := - Smallstep.Semantics step (initial_state m) final_state genv_empty. +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). |