diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 15:20:10 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 15:20:10 +0200 |
| commit | 4c65d76a7b00c01f812db3e1464fec4ecb5562c5 (patch) | |
| tree | 45561d930469303d7062fbf6ddc623623df29eff /backend/Injectproof.v | |
| parent | 020f1dfa53642fa452f73cbe71103572c2cc2cea (diff) | |
| download | compcert-kvx-4c65d76a7b00c01f812db3e1464fec4ecb5562c5.tar.gz compcert-kvx-4c65d76a7b00c01f812db3e1464fec4ecb5562c5.zip | |
injection positions are ok
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index a568d519..838230e4 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -196,12 +196,36 @@ Proof. destruct p; simpl; trivial. Qed. +Fixpoint inject_l_position extra_pc + (injections : list (node * (list inj_instr))) : node := + match injections with + | nil => extra_pc + | (pc,l)::t => inject_l_position + (Pos.succ (pos_add_nat extra_pc (List.length l))) t + end. + 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_position_ok: + forall injections prog extra_pc, + (fst (inject_l prog extra_pc injections)) = + inject_l_position extra_pc injections. +Proof. + induction injections; intros; simpl; trivial. + destruct a as [pc l]. + unfold inject_l. simpl. + rewrite (pair_expand (inject_at prog pc extra_pc l)). + fold (inject_l (snd (inject_at prog pc extra_pc l)) (fst (inject_at prog pc extra_pc l)) injections). + rewrite IHinjections. + f_equal. + rewrite inject_at_increases. + reflexivity. +Qed. + Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> |