diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-07 01:11:04 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-07 01:11:04 +0100 |
| commit | 8573889ca84a84475761b4d75d55547a2995c831 (patch) | |
| tree | cb1c78a976b0f03c9dbb46b521696bc4f90fa825 /src/hls/HTL.v | |
| parent | 6b56454246620cc1a0cda6949c524e20264d1935 (diff) | |
| download | vericert-8573889ca84a84475761b4d75d55547a2995c831.tar.gz vericert-8573889ca84a84475761b4d75d55547a2995c831.zip | |
Basically done with proof
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index e614246..61ea541 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -92,6 +92,7 @@ Record module: Type := mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; + mod_params_wf : Forall (Pos.gt mod_st) mod_params; }. Definition fundef := AST.fundef module. @@ -338,3 +339,16 @@ Proof. inversion 1 as [ Hv | Hv ]; unfold max_reg_module; apply max_reg_stmnt_le_stmnt_tree in Hv; lia. Qed. + +Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l. +Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed. + +Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True}. + refine ( + match bool_dec (max_list l <? st) true with + | left _ => left _ + | _ => _ + end + ); auto. + apply max_list_correct. apply Pos.ltb_lt in e. lia. +Qed. |