diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-05 18:22:30 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-05 18:22:30 +0100 |
| commit | 337d9e45bb6b96ec89f905cf0192d732c7bd53ff (patch) | |
| tree | 8a15b877253e589d6b838c55111aac38c05c3ef7 /src/hls/RTLBlockgenproof.v | |
| parent | dba20d6c8201c1271ebda9f228ad95c77c6ca8a6 (diff) | |
| download | vericert-337d9e45bb6b96ec89f905cf0192d732c7bd53ff.tar.gz vericert-337d9e45bb6b96ec89f905cf0192d732c7bd53ff.zip | |
Work on the match_states definition
Diffstat (limited to 'src/hls/RTLBlockgenproof.v')
| -rw-r--r-- | src/hls/RTLBlockgenproof.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index f57af34..a0a1ee8 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -115,7 +115,12 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop := forall stk stk' f tf sp pc rs m pc' ps bb (TF: transl_function f = OK tf) (PC: find_block_spec tf.(fn_code) pc pc') - (STK: Forall2 match_stackframe stk stk'), + (STK: Forall2 match_stackframe stk stk') + (BB: forall i bb', + f.(RTL.fn_code) ! pc = Some i -> + tf.(fn_code) ! pc' = Some bb' -> + list_drop (Pos.to_nat pc' - Pos.to_nat pc)%nat bb'.(bb_body) = i' :: bb + ), match_states (RTL.State stk f sp pc rs m) (State stk' tf sp pc' bb rs ps m). |