diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 14:55:49 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 14:55:49 +0200 |
| commit | 020f1dfa53642fa452f73cbe71103572c2cc2cea (patch) | |
| tree | 00841cc9788da4b5ba12ad779f941151e722f697 /backend/Injectproof.v | |
| parent | d1adc4858ec70963233945542b717fcd1459a96a (diff) | |
| download | compcert-kvx-020f1dfa53642fa452f73cbe71103572c2cc2cea.tar.gz compcert-kvx-020f1dfa53642fa452f73cbe71103572c2cc2cea.zip | |
inject_at injects the end
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 31 |
1 files changed, 26 insertions, 5 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index eeaadb2a..a568d519 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -168,11 +168,26 @@ Proof. all: apply inject_list_increases. Qed. -Definition inject_l (prog : code) extra_pc injections := - List.fold_left (fun already (injection : node * (list inj_instr)) => - inject_at' already (fst injection) (snd injection)) - injections - (extra_pc, prog). +Lemma inject_at_injected: + forall l prog pc extra_pc k (BOUND : (k < (List.length l))%nat), + PTree.get (pos_add_nat extra_pc k) (snd (inject_at prog pc extra_pc l)) = + Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat extra_pc k))). +Proof. + intros. unfold inject_at. + destruct (prog ! pc); apply inject_list_injected. +Qed. + +Lemma inject_at_injected_end: + forall l prog pc extra_pc i, + PTree.get pc prog = Some i -> + PTree.get (pos_add_nat extra_pc (List.length l)) + (snd (inject_at prog pc extra_pc l)) = + Some (Inop (successor i)). +Proof. + intros until i. intro REW. unfold inject_at. + rewrite REW. + apply inject_list_injected_end. +Qed. Lemma pair_expand: forall { A B : Type } (p : A*B), @@ -181,6 +196,12 @@ Proof. destruct p; simpl; trivial. Qed. +Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (injection : node * (list inj_instr)) => + inject_at' already (fst injection) (snd injection)) + injections + (extra_pc, prog). + Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> |