diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-05 23:17:33 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:38:45 +0100 |
| commit | 1c8e0373d735ac88740f96c5da1d929ce3f7b688 (patch) | |
| tree | 60c170715bdc960778f58502f56dcb28775d3e13 /src/hls/HTL.v | |
| parent | 34a0415ad0c65602ba097c37e23ced9cb3cf390e (diff) | |
| download | vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.tar.gz vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.zip | |
Move HTL renaming pass to own file
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 12b6493..1eb86e1 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -30,6 +30,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.ValueInt. Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. +Require Import vericert.common.Maps. Require vericert.hls.Verilog. (** The purpose of the hardware transfer language (HTL) is to create a more @@ -246,3 +247,14 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + +Lemma max_pc_wf : + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. |