diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:02:14 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:02:14 +0100 |
| commit | 87fba8b56e25130519f7b4bea4b9887bc14ec31f (patch) | |
| tree | 10a742e88804c8325dd51ede561bf828fd4af458 /src/hls/HTLgenspec.v | |
| parent | f7616136f1a2f3561500b1c28219ae725c4cda17 (diff) | |
| download | vericert-87fba8b56e25130519f7b4bea4b9887bc14ec31f.tar.gz vericert-87fba8b56e25130519f7b4bea4b9887bc14ec31f.zip | |
Add "join state is <=Int.max_unsigned" to HTLgenspec
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 0c15f53..7480231 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -103,7 +103,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap (forall n arg, List.nth_error args n = Some arg -> exists r, In (r, arg) (List.combine fn_params args) /\ externctrl ! r = Some (fn, ctrl_param n)) /\ - + Z.pos pc2 <= Int.max_unsigned /\ stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ trans!pc = Some (state_goto st pc2) /\ stmnts!pc2 = Some (join fn_return fn_rst dst) /\ @@ -393,6 +393,7 @@ Proof. * intros. destruct (map_externctrl_params_spec _ _ _ _ _ _ _ _ EQ1 ltac:(eauto)) as [param [? ?]]. exists param; crush; trans_step s3 s'. + * monadInv EQ2. crush. + (* Icond *) tr_code_simple_tac. + (* Ireturn *) inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. |