[2286] | 1 | include "common/BackEndOps.ma". |
---|
[757] | 2 | include "common/CostLabel.ma". |
---|
| 3 | include "common/Registers.ma". |
---|
[2286] | 4 | include "ASM/I8051.ma". |
---|
[1176] | 5 | include "common/Graphs.ma". |
---|
[2286] | 6 | include "utilities/lists.ma". |
---|
| 7 | include "common/LabelledObjects.ma". |
---|
| 8 | include "ASM/Util.ma". |
---|
[2655] | 9 | include "basics/lists/listb.ma". |
---|
[2645] | 10 | include "joint/String.ma". |
---|
[733] | 11 | |
---|
[2286] | 12 | (* Here is the structure of parameter records (downward edges are coercions, |
---|
| 13 | the ↓ edges are the only explicitly defined coercions). lin_params and |
---|
| 14 | graph_params are simple wrappers of unserialized_params, and the coercions |
---|
[2490] | 15 | from them to params instantate the missing bits with values for linarized |
---|
[2286] | 16 | programs and graph programs respectively. |
---|
[1164] | 17 | |
---|
[2286] | 18 | lin_params graph_params |
---|
| 19 | | \_____ /____ | |
---|
| 20 | | / \ | |
---|
| 21 | | / ↓ ↓ |
---|
| 22 | | | params |
---|
| 23 | | | | |
---|
| 24 | | | stmt_params |
---|
| 25 | | | / |
---|
| 26 | unserialized_params |
---|
[1233] | 27 | |
---|
[2286] | 28 | unserialized_params : things unrelated to being in graph or linear form |
---|
| 29 | stmt_params : adds successor type needed to define statements |
---|
| 30 | params : adds type of code and related properties *) |
---|
[1280] | 31 | |
---|
[2457] | 32 | (* |
---|
[2286] | 33 | inductive possible_flows : Type[0] ≝ |
---|
| 34 | | Labels : list label → possible_flows |
---|
| 35 | | Call : possible_flows. |
---|
[2457] | 36 | *) |
---|
[733] | 37 | |
---|
[2286] | 38 | inductive argument (T : Type[0]) : Type[0] ≝ |
---|
| 39 | | Reg : T → argument T |
---|
[2490] | 40 | | Imm : Byte → argument T. |
---|
[1169] | 41 | |
---|
[2286] | 42 | definition psd_argument ≝ argument register. |
---|
| 43 | |
---|
| 44 | definition psd_argument_from_reg : register → psd_argument ≝ Reg register. |
---|
| 45 | coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg |
---|
| 46 | on _r : register to psd_argument. |
---|
[2490] | 47 | (* |
---|
[2286] | 48 | definition psd_argument_from_beval : beval → psd_argument ≝ Imm register. |
---|
| 49 | coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval |
---|
| 50 | on _b : beval to psd_argument. |
---|
[2490] | 51 | *) |
---|
| 52 | definition psd_argument_from_byte : Byte → psd_argument ≝ Imm ?. |
---|
[2286] | 53 | coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte |
---|
| 54 | on _b : Byte to psd_argument. |
---|
| 55 | |
---|
| 56 | definition hdw_argument ≝ argument Register. |
---|
| 57 | |
---|
| 58 | definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register. |
---|
| 59 | coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg |
---|
| 60 | on _r : Register to hdw_argument. |
---|
[2490] | 61 | (* |
---|
[2286] | 62 | definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register. |
---|
| 63 | coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval |
---|
| 64 | on _b : beval to hdw_argument. |
---|
[2490] | 65 | *) |
---|
| 66 | definition hdw_argument_from_byte : Byte → hdw_argument ≝ Imm ?. |
---|
[2286] | 67 | coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte |
---|
| 68 | on _b : Byte to hdw_argument. |
---|
| 69 | |
---|
| 70 | definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8. |
---|
| 71 | definition zero_byte : Byte ≝ bv_zero 8. |
---|
| 72 | |
---|
| 73 | record unserialized_params : Type[1] ≝ |
---|
| 74 | { acc_a_reg: Type[0] (* registers that will eventually need to be A *) |
---|
| 75 | ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) |
---|
| 76 | ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *) |
---|
| 77 | ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *) |
---|
| 78 | ; dpl_reg: Type[0] (* low address registers *) |
---|
| 79 | ; dph_reg: Type[0] (* high address registers *) |
---|
| 80 | ; dpl_arg: Type[0] (* low address registers *) |
---|
| 81 | ; dph_arg: Type[0] (* high address registers *) |
---|
| 82 | ; snd_arg : Type[0] (* second argument of binary op *) |
---|
| 83 | ; pair_move: Type[0] (* argument of move instructions *) |
---|
| 84 | ; call_args: Type[0] (* arguments of function calls *) |
---|
| 85 | ; call_dest: Type[0] (* possible destination of function computation *) |
---|
| 86 | (* other instructions not fitting in the general framework *) |
---|
| 87 | ; ext_seq : Type[0] |
---|
[2532] | 88 | ; ext_seq_labels : ext_seq → list label |
---|
[2457] | 89 | ; has_tailcalls : bool |
---|
[2286] | 90 | (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) |
---|
| 91 | ; paramsT : Type[0] |
---|
[1280] | 92 | }. |
---|
[2783] | 93 | |
---|
| 94 | record get_pseudo_reg_functs (p : unserialized_params) : Type[0] ≝ |
---|
| 95 | { acc_a_regs : acc_a_reg p → list register |
---|
| 96 | ; acc_b_regs : acc_b_reg p → list register |
---|
| 97 | ; acc_a_args : acc_a_arg p → list register |
---|
| 98 | ; acc_b_args : acc_b_arg p → list register |
---|
| 99 | ; dpl_regs : dpl_reg p → list register |
---|
| 100 | ; dph_regs : dph_reg p → list register |
---|
| 101 | ; dpl_args : dpl_arg p → list register |
---|
| 102 | ; dph_args : dph_arg p → list register |
---|
| 103 | ; snd_args : snd_arg p → list register |
---|
| 104 | ; pair_move_regs : pair_move p → list register |
---|
| 105 | ; f_call_args : call_args p → list register |
---|
| 106 | ; f_call_dest : call_dest p → list register |
---|
| 107 | ; ext_seq_regs : ext_seq p → list register |
---|
| 108 | ; params_regs : paramsT p → list register |
---|
| 109 | }. |
---|
[1280] | 110 | |
---|
[2783] | 111 | record uns_params : Type[1] ≝ |
---|
| 112 | { u_pars :> unserialized_params |
---|
| 113 | ; functs : get_pseudo_reg_functs u_pars |
---|
| 114 | }. |
---|
| 115 | |
---|
[2286] | 116 | inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝ |
---|
| 117 | | COMMENT: String → joint_seq p globals |
---|
| 118 | | MOVE: pair_move p → joint_seq p globals |
---|
| 119 | | POP: acc_a_reg p → joint_seq p globals |
---|
| 120 | | PUSH: acc_a_arg p → joint_seq p globals |
---|
[2655] | 121 | | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals |
---|
[2286] | 122 | | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals |
---|
| 123 | | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals |
---|
| 124 | | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals |
---|
| 125 | (* int done with generic move *) |
---|
| 126 | (*| INT: generic_reg p → Byte → joint_seq p globals *) |
---|
| 127 | | CLEAR_CARRY: joint_seq p globals |
---|
| 128 | | SET_CARRY: joint_seq p globals |
---|
| 129 | | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals |
---|
| 130 | | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals |
---|
[2437] | 131 | | extension_seq : ext_seq p → joint_seq p globals. |
---|
[2783] | 132 | |
---|
| 133 | definition get_used_registers_from_seq : ∀p : unserialized_params.∀globals. |
---|
| 134 | get_pseudo_reg_functs p → joint_seq p globals → list register ≝ |
---|
| 135 | λp,globals,functs,seq. |
---|
| 136 | match seq with |
---|
| 137 | [ COMMENT _ ⇒ [ ] |
---|
| 138 | | MOVE pm ⇒ pair_move_regs … functs pm |
---|
| 139 | | POP r ⇒ acc_a_regs … functs r |
---|
| 140 | | PUSH r ⇒ acc_a_args … functs r |
---|
| 141 | | ADDRESS i prf r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2) |
---|
| 142 | | OPACCS o r1 r2 r3 r4 ⇒ (acc_a_regs … functs r1) @ (acc_b_regs … functs r2) |
---|
| 143 | @ (acc_a_args … functs r3) @ (acc_b_args … functs r4) |
---|
| 144 | | OP1 o r1 r2 ⇒ (acc_a_regs … functs r1) @ (acc_a_regs … functs r2) |
---|
| 145 | | OP2 o r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (acc_a_args … functs r2) @ |
---|
| 146 | (snd_args … functs r3) |
---|
| 147 | | CLEAR_CARRY ⇒ [ ] |
---|
| 148 | | SET_CARRY ⇒ [ ] |
---|
| 149 | | LOAD r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (dpl_args … functs r2) @ |
---|
| 150 | (dph_args … functs r3) |
---|
| 151 | | STORE r1 r2 r3 ⇒ (dpl_args … functs r1) @ (dph_args … functs r2) @ |
---|
| 152 | (acc_a_args … functs r3) |
---|
| 153 | | extension_seq ext ⇒ ext_seq_regs … functs ext |
---|
| 154 | ]. |
---|
[2286] | 155 | |
---|
| 156 | definition NOOP ≝ λp,globals.COMMENT p globals EmptyString. |
---|
| 157 | |
---|
| 158 | notation "r ← a1 .op. a2" with precedence 60 for |
---|
| 159 | @{'op2 $op $r $a1 $a2}. |
---|
| 160 | notation "r ← . op . a" with precedence 60 for |
---|
| 161 | @{'op1 $op $r $a}. |
---|
| 162 | notation "r ← a" with precedence 60 for |
---|
| 163 | @{'mov $r $a}. (* to be set in individual languages *) |
---|
| 164 | notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for |
---|
| 165 | @{'opaccs $op $r $s $a1 $a2}. |
---|
| 166 | |
---|
| 167 | interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). |
---|
| 168 | interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). |
---|
| 169 | interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). |
---|
| 170 | |
---|
| 171 | coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝ |
---|
| 172 | extension_seq on _s : ext_seq ? to joint_seq ??. |
---|
[2437] | 173 | |
---|
[2286] | 174 | (* inductive joint_branch (p : step_params) : Type[0] ≝ |
---|
| 175 | | COND: acc_a_reg p → label → joint_branch p |
---|
| 176 | | extension_branch : ext_branch p → joint_branch p.*) |
---|
| 177 | |
---|
| 178 | (*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝ |
---|
| 179 | extension_branch on _s : ext_branch ? to joint_branch ?.*) |
---|
| 180 | |
---|
| 181 | inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝ |
---|
[2688] | 182 | | COST_LABEL: costlabel → joint_step p globals |
---|
[2561] | 183 | | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals |
---|
[2562] | 184 | | COND: acc_a_reg p → label → joint_step p globals |
---|
| 185 | | step_seq : joint_seq p globals → joint_step p globals. |
---|
[2783] | 186 | |
---|
| 187 | definition get_used_registers_from_step : ∀p : unserialized_params.∀globals. |
---|
| 188 | get_pseudo_reg_functs p → joint_step p globals → list register ≝ |
---|
| 189 | λp,globals,functs,step. |
---|
| 190 | match step with |
---|
| 191 | [ COST_LABEL c ⇒ [ ] |
---|
[2843] | 192 | | CALL id args dest ⇒ |
---|
| 193 | let r_id ≝ match id with |
---|
| 194 | [ inl _ ⇒ [ ] |
---|
| 195 | | inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @ |
---|
| 196 | ((dph_args … functs) (\snd ptr)) |
---|
| 197 | ] in |
---|
| 198 | r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest) |
---|
[2783] | 199 | | COND r lbl ⇒ acc_a_regs … functs r |
---|
| 200 | | step_seq s ⇒ get_used_registers_from_seq … functs s |
---|
| 201 | ]. |
---|
[2286] | 202 | |
---|
| 203 | coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝ |
---|
| 204 | step_seq on _s : joint_seq ?? to joint_step ??. |
---|
| 205 | |
---|
[2457] | 206 | definition step_labels ≝ |
---|
| 207 | λp, globals.λs : joint_step p globals. |
---|
[2286] | 208 | match s with |
---|
[2532] | 209 | [ step_seq s ⇒ |
---|
| 210 | match s with |
---|
| 211 | [ extension_seq ext ⇒ ext_seq_labels … ext |
---|
| 212 | | _ ⇒ [ ] |
---|
| 213 | ] |
---|
[2457] | 214 | | COND _ l ⇒ [l] |
---|
[2688] | 215 | | _ ⇒ [ ] |
---|
[2286] | 216 | ]. |
---|
| 217 | |
---|
| 218 | definition step_forall_labels : ∀p.∀globals. |
---|
| 219 | (label → Prop) → joint_step p globals → Prop ≝ |
---|
| 220 | λp,g,P,inst. All … P (step_labels … inst). |
---|
| 221 | |
---|
| 222 | record stmt_params : Type[1] ≝ |
---|
[2783] | 223 | { uns_pars :> uns_params |
---|
[2286] | 224 | ; succ : Type[0] |
---|
| 225 | ; succ_label : succ → option label |
---|
[2532] | 226 | ; has_fcond : bool |
---|
| 227 | }. |
---|
[2286] | 228 | |
---|
| 229 | inductive joint_fin_step (p: unserialized_params): Type[0] ≝ |
---|
| 230 | | GOTO: label → joint_fin_step p |
---|
| 231 | | RETURN: joint_fin_step p |
---|
[2457] | 232 | | TAILCALL : |
---|
[2537] | 233 | has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) → |
---|
[2457] | 234 | call_args p → joint_fin_step p. |
---|
[2286] | 235 | |
---|
[2457] | 236 | definition fin_step_labels ≝ λp.λs : joint_fin_step p. |
---|
[2286] | 237 | match s with |
---|
[2457] | 238 | [ GOTO l ⇒ [l] |
---|
| 239 | | _ ⇒ [ ] |
---|
[2286] | 240 | ]. |
---|
| 241 | |
---|
| 242 | inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ |
---|
| 243 | | sequential: joint_step p globals → succ p → joint_statement p globals |
---|
[2532] | 244 | | final: joint_fin_step p → joint_statement p globals |
---|
| 245 | | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals. |
---|
[2286] | 246 | |
---|
| 247 | coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. |
---|
| 248 | ∀s : joint_fin_step p.joint_statement p globals ≝ |
---|
| 249 | final on _s : joint_fin_step ? to joint_statement ??. |
---|
| 250 | |
---|
| 251 | record params : Type[1] ≝ |
---|
| 252 | { stmt_pars :> stmt_params |
---|
| 253 | ; codeT: list ident → Type[0] |
---|
| 254 | ; code_point : Type[0] |
---|
| 255 | ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals) |
---|
| 256 | ; point_of_label : ∀globals.codeT globals → label → option code_point |
---|
| 257 | ; point_of_succ : code_point → succ stmt_pars → code_point |
---|
[1246] | 258 | }. |
---|
| 259 | |
---|
[2286] | 260 | definition code_has_point ≝ |
---|
| 261 | λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false]. |
---|
[1252] | 262 | |
---|
[2286] | 263 | (* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *) |
---|
[2532] | 264 | (* |
---|
[2286] | 265 | definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). |
---|
| 266 | unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)). |
---|
| 267 | |
---|
| 268 | definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code. |
---|
| 269 | match pt with |
---|
| 270 | [ mk_Sig pt' pt_prf ⇒ |
---|
| 271 | match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with |
---|
| 272 | [ Some x ⇒ λ_.x |
---|
| 273 | | None ⇒ λabs.⊥ |
---|
| 274 | ] (refl …) |
---|
| 275 | ]. normalize in pt_prf; |
---|
| 276 | >abs in pt_prf; // qed. |
---|
[2532] | 277 | *) |
---|
[2286] | 278 | |
---|
| 279 | definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals) ≝ |
---|
| 280 | λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s. |
---|
| 281 | |
---|
| 282 | definition forall_statements_i : |
---|
| 283 | ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) → |
---|
| 284 | codeT p globals → Prop ≝ |
---|
| 285 | λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s. |
---|
| 286 | |
---|
| 287 | lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals). |
---|
| 288 | #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. |
---|
| 289 | |
---|
| 290 | lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) → |
---|
| 291 | ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c. |
---|
| 292 | #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. |
---|
| 293 | |
---|
| 294 | definition code_has_label ≝ λp,globals,c,l. |
---|
| 295 | match point_of_label p globals c l with |
---|
| 296 | [ Some pt ⇒ code_has_point … c pt |
---|
| 297 | | None ⇒ false |
---|
| 298 | ]. |
---|
| 299 | |
---|
| 300 | definition stmt_explicit_labels : |
---|
| 301 | ∀p,globals. |
---|
| 302 | joint_statement p globals → list label ≝ |
---|
| 303 | λp,globals,stmt. match stmt with |
---|
| 304 | [ sequential c _ ⇒ step_labels … c |
---|
| 305 | | final c ⇒ fin_step_labels … c |
---|
[2532] | 306 | | FCOND _ _ l1 l2 ⇒ [l1 ; l2] |
---|
[2286] | 307 | ]. |
---|
| 308 | |
---|
| 309 | definition stmt_implicit_label : ∀p,globals.joint_statement p globals → |
---|
| 310 | option label ≝ |
---|
| 311 | λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?]. |
---|
| 312 | |
---|
| 313 | definition stmt_labels : ∀p : stmt_params.∀globals. |
---|
| 314 | joint_statement p globals → list label ≝ |
---|
| 315 | λp,g,stmt. |
---|
| 316 | (match stmt_implicit_label … stmt with |
---|
| 317 | [ Some l ⇒ [l] |
---|
| 318 | | None ⇒ [ ] |
---|
| 319 | ]) @ stmt_explicit_labels … stmt. |
---|
[2783] | 320 | |
---|
| 321 | definition stmt_registers : ∀p : stmt_params.∀globals. |
---|
| 322 | joint_statement p globals → list register ≝ |
---|
| 323 | λp,globals,stmt. |
---|
| 324 | match stmt with |
---|
| 325 | [ sequential c _ ⇒ get_used_registers_from_step … (functs … p) c |
---|
| 326 | | final c ⇒ |
---|
| 327 | match c with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ] |
---|
| 328 | | FCOND _ r _ _ ⇒ acc_a_regs … (functs … p) r |
---|
| 329 | ]. |
---|
[2286] | 330 | |
---|
| 331 | definition stmt_forall_labels ≝ |
---|
| 332 | λp, globals.λ P : label → Prop.λs : joint_statement p globals. |
---|
| 333 | All … P (stmt_labels … s). |
---|
[2783] | 334 | |
---|
[2286] | 335 | |
---|
| 336 | lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals. |
---|
| 337 | stmt_forall_labels … P s → All … P (stmt_explicit_labels … s). |
---|
| 338 | #p#globals#P #s |
---|
| 339 | whd in ⊢ (% → ?); |
---|
| 340 | whd in ⊢ (???% → ?); |
---|
| 341 | elim (stmt_implicit_label ???) [2: #next * #_] // |
---|
| 342 | qed. |
---|
| 343 | |
---|
| 344 | lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals. |
---|
| 345 | stmt_forall_labels … P s → |
---|
| 346 | opt_All … P (stmt_implicit_label … s). |
---|
| 347 | #p#globals#P#s |
---|
| 348 | whd in ⊢ (% → ?); |
---|
| 349 | whd in ⊢ (???% → ?); |
---|
| 350 | elim (stmt_implicit_label ???) |
---|
| 351 | [ // |
---|
| 352 | | #next * #Pnext #_ @Pnext |
---|
| 353 | ] |
---|
| 354 | qed. |
---|
| 355 | |
---|
| 356 | definition code_forall_labels ≝ |
---|
| 357 | λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c. |
---|
| 358 | |
---|
| 359 | lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) → |
---|
| 360 | ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝ |
---|
| 361 | λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?). |
---|
| 362 | |
---|
| 363 | record lin_params : Type[1] ≝ |
---|
[2783] | 364 | { l_u_pars : uns_params }. |
---|
[2286] | 365 | |
---|
| 366 | lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|). |
---|
| 367 | #tag #A #lbl #l elim l [*] |
---|
| 368 | ** [2: #id] #a #tl #IH |
---|
| 369 | [ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????); |
---|
| 370 | change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????); |
---|
| 371 | @eq_identifier_elim #Heq normalize nodelta |
---|
| 372 | [ #_ normalize / by /] |
---|
| 373 | | whd in ⊢ (?%→?%?); |
---|
| 374 | ] |
---|
| 375 | #H >(index_of_label_from_internal … H) |
---|
| 376 | @le_S_S @(IH H) |
---|
| 377 | qed. |
---|
| 378 | |
---|
| 379 | (* mv *) |
---|
| 380 | lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|. |
---|
| 381 | #A #l elim l normalize [ #n #x #ABS destruct(ABS)] |
---|
| 382 | #hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by / |
---|
| 383 | qed. |
---|
| 384 | |
---|
| 385 | lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|. |
---|
| 386 | #A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)] |
---|
| 387 | #n' #H @le_S_S @(IH … H) |
---|
| 388 | qed. |
---|
| 389 | |
---|
| 390 | lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf). |
---|
| 391 | #A #l elim l |
---|
| 392 | [ #n #ABS @⊥ /2 by absurd/ |
---|
| 393 | | #hd #tl #IH * normalize // |
---|
| 394 | ] |
---|
| 395 | qed. |
---|
| 396 | |
---|
| 397 | definition lin_params_to_params ≝ |
---|
| 398 | λlp : lin_params. |
---|
| 399 | mk_params |
---|
[2532] | 400 | (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true) |
---|
[2286] | 401 | (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) |
---|
| 402 | (* code_point ≝ *)ℕ |
---|
| 403 | (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls) |
---|
| 404 | (* point_of_label ≝ *)(λglobals,c,lbl. |
---|
| 405 | If occurs_exactly_once ?? lbl c then with prf do |
---|
| 406 | return index_of_label ?? lbl c |
---|
| 407 | else |
---|
| 408 | None ?) |
---|
| 409 | (* point_of_succ ≝ *)(λcurrent.λ_.S (current)). |
---|
| 410 | |
---|
| 411 | coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params |
---|
| 412 | on _lp : lin_params to params. |
---|
| 413 | |
---|
| 414 | lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals. |
---|
| 415 | ∀pt.code_has_point … code pt = leb (S pt) (|code|). |
---|
| 416 | #lp #globals #code elim code |
---|
| 417 | [ #pt % |
---|
| 418 | | #hd #tl #IH * [%] |
---|
| 419 | #n @IH |
---|
| 420 | ]qed. |
---|
| 421 | |
---|
| 422 | lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals. |
---|
| 423 | ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code. |
---|
| 424 | #lp #globals #code #lbl |
---|
| 425 | whd in match (code_has_label ????); |
---|
| 426 | whd in match (point_of_label ????); |
---|
| 427 | elim (true_or_false_Prop (occurs_exactly_once ?? lbl code)) |
---|
| 428 | #Heq >Heq normalize nodelta |
---|
| 429 | [ >lin_code_has_point @(leb_elim (S ?)) [#_ | |
---|
| 430 | #ABS elim(absurd ?? ABS) -ABS |
---|
| 431 | @index_of_label_length assumption ]] % |
---|
| 432 | qed. |
---|
| 433 | |
---|
| 434 | record graph_params : Type[1] ≝ |
---|
[2783] | 435 | { g_u_pars : uns_params }. |
---|
[2286] | 436 | |
---|
[1280] | 437 | (* One common instantiation of params via Graphs of joint_statements |
---|
| 438 | (all languages but LIN) *) |
---|
[2286] | 439 | definition graph_params_to_params ≝ |
---|
| 440 | λgp : graph_params. |
---|
| 441 | mk_params |
---|
[2532] | 442 | (mk_stmt_params (g_u_pars gp) label (Some ?) false) |
---|
[2286] | 443 | (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) |
---|
| 444 | (* code_point ≝ *)label |
---|
| 445 | (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code) |
---|
| 446 | (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl) |
---|
| 447 | (* point_of_succ ≝ *)(λ_.λlbl.lbl). |
---|
[1252] | 448 | |
---|
[2286] | 449 | coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params |
---|
| 450 | on _gp : graph_params to params. |
---|
[1280] | 451 | |
---|
[2286] | 452 | lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals. |
---|
| 453 | ∀pt.code_has_point … code pt = (pt ∈ code). // qed. |
---|
[1280] | 454 | |
---|
[2286] | 455 | lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals. |
---|
| 456 | ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed. |
---|
| 457 | |
---|
| 458 | definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop. |
---|
| 459 | λs : joint_statement p globals. |
---|
| 460 | match s with |
---|
| 461 | [ sequential _ n ⇒ P n |
---|
| 462 | | _ ⇒ True |
---|
| 463 | ]. |
---|
| 464 | |
---|
| 465 | definition statement_closed : ∀globals.∀p : params. |
---|
| 466 | codeT p globals → code_point p → (joint_statement p globals) → Prop ≝ |
---|
| 467 | λglobals,p,code,pt,s. |
---|
| 468 | All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧ |
---|
| 469 | stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s. |
---|
| 470 | |
---|
| 471 | definition code_closed : ∀p : params.∀globals. |
---|
| 472 | codeT p globals → Prop ≝ λp,globals,code. |
---|
| 473 | forall_statements_i … (statement_closed … code) code. |
---|
| 474 | |
---|
| 475 | record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝ |
---|
[1176] | 476 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
| 477 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
[2286] | 478 | (* Paolo: if we want this machinery to work for RTLabs too, we will need the |
---|
| 479 | following, right? *) |
---|
[1176] | 480 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
[2286] | 481 | joint_if_result : call_dest p; |
---|
[1233] | 482 | joint_if_params : paramsT p; |
---|
[1176] | 483 | joint_if_stacksize: nat; |
---|
[2808] | 484 | joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions |
---|
| 485 | (that are already on stack in the front end) *) |
---|
[2286] | 486 | joint_if_code : codeT p globals ; |
---|
[2823] | 487 | joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ; |
---|
[2595] | 488 | joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *) |
---|
[1176] | 489 | }. |
---|
| 490 | |
---|
[2783] | 491 | definition regs_in_universe : ∀p,globals. |
---|
| 492 | codeT p globals → universe RegisterTag → Prop ≝ |
---|
| 493 | λp,globals,c,u.∀pt,stmt.stmt_at p globals c pt = return stmt → |
---|
| 494 | All ? (λreg.fresh_for_univ … reg u) (stmt_registers … stmt). |
---|
| 495 | |
---|
[2681] | 496 | definition code_in_universe : ∀p,globals. |
---|
| 497 | codeT p globals → universe LabelTag → Prop ≝ |
---|
| 498 | λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u. |
---|
| 499 | |
---|
| 500 | lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m. |
---|
| 501 | i ∈ m → present tag A m i. |
---|
| 502 | #tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i) |
---|
| 503 | [ * | #x #_ % #ABS destruct ] |
---|
| 504 | qed. |
---|
| 505 | |
---|
| 506 | lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m. |
---|
| 507 | present tag A m i → bool_to_Prop (i∈m). |
---|
| 508 | #tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i) |
---|
| 509 | [ * #ABS cases (ABS (refl …)) | #x #_ % ] |
---|
| 510 | qed. |
---|
| 511 | |
---|
| 512 | lemma graph_code_in_universe_if : ∀p : graph_params.∀globals. |
---|
| 513 | ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝ |
---|
| 514 | λp,g,c,u,H,l,G.H ? (memb_to_present … G). |
---|
| 515 | |
---|
| 516 | lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals. |
---|
| 517 | ∀c : codeT p globals.∀u. |
---|
| 518 | code_in_universe … c u → fresh_map_for_univ … c u ≝ |
---|
| 519 | λp,g,c,u,H,l,G.H ? (present_to_memb … G). |
---|
| 520 | |
---|
| 521 | include alias "basics/logic.ma". |
---|
[2863] | 522 | check stmt_at |
---|
[2681] | 523 | record good_if |
---|
| 524 | (p : params) (globals : list ident) (def : joint_internal_function p globals) |
---|
| 525 | : Prop ≝ |
---|
[2712] | 526 | { entry_costed : |
---|
[2681] | 527 | ∃l,nxt. |
---|
| 528 | stmt_at … (joint_if_code … def) (joint_if_entry … def) = |
---|
| 529 | Some … (sequential … (COST_LABEL … l) nxt) |
---|
[2712] | 530 | ; entry_unused : |
---|
[2823] | 531 | let entry ≝ joint_if_entry … def in |
---|
[2712] | 532 | let code ≝ joint_if_code … def in |
---|
| 533 | forall_statements_i … |
---|
| 534 | (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧ |
---|
| 535 | stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code |
---|
[2681] | 536 | ; code_is_closed : code_closed … (joint_if_code … def) |
---|
| 537 | ; code_is_in_universe : |
---|
| 538 | code_in_universe … (joint_if_code … def) (joint_if_luniverse … def) |
---|
[2783] | 539 | ; regs_are_in_univers : |
---|
| 540 | regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def) |
---|
[2863] | 541 | ; entry_is_cost : |
---|
| 542 | ∃nxt,c. |
---|
| 543 | stmt_at p globals (joint_if_code … def) (joint_if_entry … def) = |
---|
| 544 | Some ? (sequential p ? (COST_LABEL ?? c) nxt) |
---|
[2681] | 545 | }. |
---|
| 546 | |
---|
[2286] | 547 | definition joint_closed_internal_function ≝ |
---|
| 548 | λp,globals. |
---|
[2681] | 549 | Σdef : joint_internal_function p globals.good_if … def. |
---|
[1245] | 550 | |
---|
[2462] | 551 | unification hint 0 ≔ p,g ⊢ |
---|
| 552 | joint_closed_internal_function p g ≡ |
---|
[2681] | 553 | Sig (joint_internal_function p g) (λdef.good_if … def). |
---|
[2462] | 554 | |
---|
[1471] | 555 | definition set_joint_code ≝ |
---|
| 556 | λglobals: list ident. |
---|
[2286] | 557 | λpars: params. |
---|
| 558 | λint_fun: joint_internal_function pars globals. |
---|
| 559 | λgraph: codeT pars globals. |
---|
[1471] | 560 | λentry. |
---|
[2595] | 561 | (*λexit.*) |
---|
[2286] | 562 | mk_joint_internal_function pars globals |
---|
[1471] | 563 | (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) |
---|
[2595] | 564 | (joint_if_params … int_fun) (joint_if_stacksize … int_fun) |
---|
[2808] | 565 | (joint_if_local_stacksize … int_fun) |
---|
[2595] | 566 | graph entry (*exit*). |
---|
[1471] | 567 | |
---|
[1220] | 568 | definition set_luniverse ≝ |
---|
[1252] | 569 | λglobals,pars. |
---|
| 570 | λp : joint_internal_function globals pars. |
---|
[1220] | 571 | λluniverse: universe LabelTag. |
---|
[1252] | 572 | mk_joint_internal_function globals pars |
---|
| 573 | luniverse (joint_if_runiverse … p) (joint_if_result … p) |
---|
[2808] | 574 | (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) |
---|
[2595] | 575 | (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). |
---|
[1220] | 576 | |
---|
[1254] | 577 | definition set_runiverse ≝ |
---|
| 578 | λglobals,pars. |
---|
| 579 | λp : joint_internal_function globals pars. |
---|
| 580 | λruniverse: universe RegisterTag. |
---|
| 581 | mk_joint_internal_function globals pars |
---|
| 582 | (joint_if_luniverse … p) runiverse (joint_if_result … p) |
---|
[2808] | 583 | (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) |
---|
[2595] | 584 | (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). |
---|
[2286] | 585 | |
---|
[1252] | 586 | (* Specialized for graph_params *) |
---|
| 587 | definition add_graph ≝ |
---|
[2286] | 588 | λg_pars : graph_params.λglobals.λl:label.λstmt. |
---|
| 589 | λp:joint_internal_function g_pars globals. |
---|
| 590 | let code ≝ add … (joint_if_code … p) l stmt in |
---|
| 591 | mk_joint_internal_function … |
---|
[1252] | 592 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
[2808] | 593 | (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) |
---|
[2286] | 594 | code |
---|
[2823] | 595 | (joint_if_entry … p) |
---|
[2595] | 596 | (*(pi1 … (joint_if_exit … p))*). |
---|
[1252] | 597 | |
---|
[2422] | 598 | definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals). |
---|
[1176] | 599 | |
---|
[1246] | 600 | definition joint_program ≝ |
---|
[2547] | 601 | λp:params. program (joint_function p) nat. |
---|
[2774] | 602 | |
---|
| 603 | (* The cost model for stack consumption *) |
---|
| 604 | definition stack_cost_model ≝ list (ident × nat). |
---|
| 605 | |
---|
| 606 | definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝ |
---|
| 607 | λp,pr. |
---|
| 608 | foldr … |
---|
| 609 | (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in |
---|
| 610 | match fun with |
---|
| 611 | [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc |
---|
| 612 | | External _ ⇒ acc ]) |
---|
| 613 | [ ] (prog_funct ?? pr). |
---|
| 614 | |
---|
[2824] | 615 | definition globals_stacksize : ∀p.joint_program p → nat ≝ |
---|
| 616 | λpars,p. |
---|
| 617 | Σ_{entry ∈ prog_vars … p}(\snd entry). |
---|
| 618 | |
---|