diff options
Diffstat (limited to 'src/hls/HTLPargenproof.v')
| -rw-r--r-- | src/hls/HTLPargenproof.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v index 04b87f0..9e0dccc 100644 --- a/src/hls/HTLPargenproof.v +++ b/src/hls/HTLPargenproof.v @@ -1265,17 +1265,6 @@ Proof. now rewrite AssocMap.gempty. Qed. - Lemma transl_iop_correct: - forall ctrl sp max_reg max_pred d d' curr_p next_p rs ps m rs' ps' p op args dst asr arr asr' arr' stk stk_len, - transf_instr ctrl (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') -> - step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) -> - stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d (e_assoc asr') (e_assoc_arr stk stk_len arr') -> - match_assocmaps max_reg max_pred rs ps asr' -> - exists asr'', stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d' (e_assoc asr'') (e_assoc_arr stk stk_len arr') - /\ match_assocmaps max_reg max_pred rs' ps' asr''. - Proof. - Admitted. - Transparent Mem.load. Transparent Mem.store. Transparent Mem.alloc. |