source: src/LIN/LINToASM.ma @ 2443

Last change on this file since 2443 was 2443, checked in by tranquil, 8 years ago

changed joint's stack pointer and internal stack

File size: 20.3 KB
Line 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
4include "ASM/ASM.ma".
5
6definition register_address: Register → [[ acc_a; direct; registr ]] ≝
7  λr: Register.
8    match r with
9    [ Register00 ⇒ REGISTER [[ false; false; false ]]
10    | Register01 ⇒ REGISTER [[ false; false; true ]]
11    | Register02 ⇒ REGISTER [[ false; true; false ]]
12    | Register03 ⇒ REGISTER [[ false; true; true ]]
13    | Register04 ⇒ REGISTER [[ true; false; false ]]
14    | Register05 ⇒ REGISTER [[ true; false; true ]]
15    | Register06 ⇒ REGISTER [[ true; true; false ]]
16    | Register07 ⇒ REGISTER [[ true; true; true ]]
17    | RegisterA ⇒ ACC_A
18    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
19    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
20    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
21    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
22    ]. @I qed.
23
24let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
25                    on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
26  match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
27  [ nil ⇒ Ⓧ
28  | cons hd tl ⇒
29    λprf.
30    If eq_A a (\fst hd) then \snd hd else with eq_prf do
31      association … eq_A a tl ?
32  ].
33  elim (orb_Prop_true … prf)
34    [ > eq_prf *
35    | # H
36      assumption
37    ]
38qed.
39
40definition association_ident ≝ association ident nat (eq_identifier ?).
41definition association_block ≝ association block Word eq_block.
42
43definition asm_cst_well_def :
44  list (block × Word) → beval → bool ≝
45λglobals,bv.match bv with
46[ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals)
47| _ ⇒ true
48].
49
50definition vector_cast :
51∀A,n,m.A → Vector A n → Vector A m ≝
52λA,n,m,dflt,v.
53If leb n m then with prf do
54  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
55else with prf do
56  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
57lapply prf @(leb_elim n)
58[2,3: #_ * #abs elim (abs I) ]
59#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
60[ assumption ]
61@(transitive_le … (not_le_to_lt … H)) %2 %1
62qed.
63
64definition asm_byte_of_beval :
65  ∀globals,bv.asm_cst_well_def globals bv → Byte ≝
66  λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with
67    [ BVByte b ⇒ λ_.b
68    | BVundef ⇒ λ_.(* any will do *) zero_byte
69    | BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]]
70    | BVnull _ ⇒ λ_.zero_byte (* is it correct? *)
71    | BVptr b p o ⇒ λprf.
72      let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in
73      let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in
74      head' … inst
75    ].
76
77definition asm_arg_well_def :
78  list (block × Word) → hdw_argument → bool ≝
79λglobals,a.match a with
80[ Imm bv ⇒ asm_cst_well_def globals bv
81| _ ⇒ true
82].
83
84definition arg_address : ∀globals,arg.asm_arg_well_def globals arg →
85  [[ acc_a ; direct ; registr ; data ]] ≝
86  λglobals,a.
87  match a
88  return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]]
89  with
90  [ Reg r ⇒ λ_.register_address r
91  | Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf)
92  ].
93  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
94  | @I
95  ]
96qed.
97
98definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
99
100definition asm_stmt_well_def :
101  list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝
102  λblocks,old_globals,stmt.
103  match stmt with
104  [ sequential instr _ ⇒
105    match instr with
106    [ step_seq instr' ⇒
107      match instr' with
108      [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg
109      | MOVE regs ⇒
110        match regs with
111        [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv
112        | int_to_acc _ bv ⇒ asm_cst_well_def blocks bv
113        | _ ⇒ true
114        ]
115      | _ ⇒ true
116      ]
117    | _ ⇒ true
118    ]
119  | _ ⇒ true
120  ].
121 
122definition statement_labels ≝
123  λg: list ident.
124  λs: lin_statement g.
125  let 〈label, instr〉 ≝ s in
126  let generated ≝
127    match instr with
128    [ sequential instr' _ ⇒
129      match instr' with
130      [ step_seq instr'' ⇒
131        match instr'' with
132        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
133        | _ ⇒ ∅
134        ]
135      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
136      ]
137    | final instr' ⇒
138      match instr' with
139      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
140      | _ ⇒ ∅
141      ]
142    ]
143  in
144  match label with
145  [ None ⇒ generated
146  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
147  ].
148
149definition function_labels_internal ≝
150  λglobals: list ident.
151  λlabels: identifier_set ?.
152  λstatement: lin_statement globals.
153    labels ∪ (statement_labels globals statement).
154
155(* dpm: A = Identifier *)
156definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
157  λA: Type[0].
158  λglobals: list ident.
159  λf: A × (joint_function LIN globals).
160  let 〈ignore, fun_def〉 ≝ f in
161  match fun_def return λ_. identifier_set ? with
162  [ Internal stmts ⇒
163      foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
164  | External _ ⇒ ∅
165  ].
166 
167definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
168  λA: Type[0].
169  λglobals: list ident.
170  λlabels: identifier_set ?.
171  λfunct: A × (joint_function LIN globals).
172    labels ∪ (function_labels ? globals funct).
173
174(* CSC: here we are silently throwing away the region information *)
175definition program_labels ≝
176 λprogram: lin_program.
177    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
178              ∅ (prog_funct … program).
179 
180definition data_of_int ≝ λbv. DATA bv.
181definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
182definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
183
184(* TODO: check and change to free bit *)
185definition asm_other_bit ≝ BIT_ADDR (zero_byte).
186
187definition translate_statements ≝
188  λglobals: list (ident × nat).
189  λblocks: list (block × Word).
190  λglobals_old: list ident.
191  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
192  λstatement: joint_statement LIN globals_old.
193  match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with
194  [ final instr ⇒ λ_.
195    match instr with
196    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
197    | RETURN ⇒ Instruction (RET ?)
198    | tailcall abs ⇒ match abs in void with [ ]
199    ]
200  | sequential instr _ ⇒
201      match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with
202      [ step_seq instr' ⇒
203        match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with
204        [ extension_seq ext ⇒ λ_.
205          match ext with
206          [ SAVE_CARRY ⇒
207            Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
208          | RESTORE_CARRY ⇒
209            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
210          ]
211        | COMMENT comment ⇒ λ_.Comment comment
212        | COST_LABEL lbl ⇒ λ_.Cost lbl
213        | POP _ ⇒ λ_.Instruction (POP ? accumulator_address)
214        | PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address)
215        | CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY)
216        | CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f)
217        | extension_call abs ⇒ λ_.match abs in void with [ ]
218        | OPACCS accs _ _ _ _ ⇒ λ_.
219          match accs with
220          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
221          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
222          ]
223        | OP1 op1 _ _ ⇒ λ_.
224          match op1 with
225          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
226          | Inc ⇒ Instruction (INC ? ACC_A)
227          | Rl ⇒ Instruction (RL ? ACC_A)
228          ]
229        | OP2 op2 _ _ reg ⇒ λprf'.?
230          | _ ⇒ ?] | _ ⇒ ? ]].[12: whd in prf : (?%);
231
232          match op2 with
233          [ Add ⇒
234            let reg' ≝ arg_address … prf' in
235            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
236                                                           direct;
237                                                           registr;
238                                                           data ]] x) → ? with
239            [ ACC_A ⇒ λacc_a: True.
240              Instruction (ADD ? ACC_A accumulator_address)
241            | DIRECT d ⇒ λdirect1: True.
242              Instruction (ADD ? ACC_A (DIRECT d))
243            | REGISTER r ⇒ λregister1: True.
244              Instruction (ADD ? ACC_A (REGISTER r))
245            | DATA b ⇒ λdata : True.
246              Instruction (ADD ? ACC_A (DATA b))
247            | _ ⇒ Ⓧ
248            ] (subaddressing_modein … reg')
249          | Addc ⇒
250            let reg' ≝ arg_address … prf' in
251            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
252                                                           direct;
253                                                           registr;
254                                                           data ]] x) → ? with
255            [ ACC_A ⇒ λacc_a: True.
256              Instruction (ADDC ? ACC_A accumulator_address)
257            | DIRECT d ⇒ λdirect2: True.
258              Instruction (ADDC ? ACC_A (DIRECT d))
259            | REGISTER r ⇒ λregister2: True.
260              Instruction (ADDC ? ACC_A (REGISTER r))
261            | DATA b ⇒ λdata : True.
262              Instruction (ADDC ? ACC_A (DATA b))
263            | _ ⇒ Ⓧ
264            ] (subaddressing_modein … reg')
265          | Sub ⇒
266            let reg' ≝ arg_address … prf' in
267            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
268                                                           direct;
269                                                           registr;
270                                                           data ]] x) → ? with
271            [ ACC_A ⇒ λacc_a: True.
272              Instruction (SUBB ? ACC_A accumulator_address)
273            | DIRECT d ⇒ λdirect3: True.
274              Instruction (SUBB ? ACC_A (DIRECT d))
275            | REGISTER r ⇒ λregister3: True.
276              Instruction (SUBB ? ACC_A (REGISTER r))
277            | DATA b ⇒ λdata : True.
278              Instruction (SUBB ? ACC_A (DATA b))
279            | _ ⇒ Ⓧ
280            ] (subaddressing_modein … reg')
281          | And ⇒
282            let reg' ≝ arg_address … prf' in
283            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
284                                                           direct;
285                                                           registr;
286                                                           data ]] x) → ? with
287            [ ACC_A ⇒ λacc_a: True.
288              Instruction (NOP ?)
289            | DIRECT d ⇒ λdirect4: True.
290              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
291            | REGISTER r ⇒ λregister4: True.
292              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
293            | DATA b ⇒ λdata : True.
294              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
295            | _ ⇒ Ⓧ
296            ] (subaddressing_modein … reg')
297          | Or ⇒
298            let reg' ≝ arg_address … prf' in
299            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
300                                                           direct;
301                                                           registr ; data ]] x) → ? with
302            [ ACC_A ⇒ λacc_a: True.
303              Instruction (NOP ?)
304            | DIRECT d ⇒ λdirect5: True.
305              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
306            | REGISTER r ⇒ λregister5: True.
307              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
308            | DATA b ⇒ λdata : True.
309              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
310            | _ ⇒ Ⓧ
311            ] (subaddressing_modein … reg')
312          | Xor ⇒
313            let reg' ≝ arg_address … prf' in
314            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
315                                                           direct;
316                                                           registr ; data ]] x) → ? with
317            [ ACC_A ⇒ λacc_a: True.
318              Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
319            | DIRECT d ⇒ λdirect6: True.
320              Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
321            | REGISTER r ⇒ λregister6: True.
322              Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
323            | DATA b ⇒ λdata : True.
324              Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
325            | _ ⇒ Ⓧ
326            ] (subaddressing_modein … reg')
327          ]
328        | LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
329        | STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
330        | ADDRESS addr proof _ _ ⇒ λ_.
331          let look ≝ association_ident addr globals (prf ? proof) in
332            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
333        | SET_CARRY ⇒ λ_.
334          Instruction (SETB ? CARRY)
335        | MOVE regs ⇒
336          match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with
337          [ to_acc _ reg ⇒ λ_.
338             let reg' ≝ register_address reg in
339               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
340                                                              direct;
341                                                              registr ]] x) → ? with
342               [ REGISTER r ⇒ λregister9: True.
343                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
344               | DIRECT d ⇒ λdirect9: True.
345                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
346               | ACC_A ⇒ λacc_a: True.
347                 Instruction (NOP ?)
348               | _ ⇒ λother: False. ⊥
349               ] (subaddressing_modein … reg')
350          | from_acc reg _ ⇒ λ_.
351             let reg' ≝ register_address reg in
352               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
353                                                              direct;
354                                                              registr ]] x) → ? with
355               [ REGISTER r ⇒ λregister8: True.
356                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
357               | ACC_A ⇒ λacc: True.
358                 Instruction (NOP ?)
359               | DIRECT d ⇒ λdirect8: True.
360                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
361               | _ ⇒ λother: False. ⊥
362               ] (subaddressing_modein … reg')
363          | int_to_reg reg bv ⇒ λprf'.
364            let b ≝ asm_byte_of_beval … prf' in
365            let reg' ≝ register_address reg in
366              match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
367                                                             direct;
368                                                             registr ]] x) → ? with
369              [ REGISTER r ⇒ λregister7: True.
370                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
371              | ACC_A ⇒ λacc: True.
372                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
373              | DIRECT d ⇒ λdirect7: True.
374                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
375              | _ ⇒ λother: False. ⊥
376              ] (subaddressing_modein … reg')
377          | int_to_acc _ bv ⇒ λprf'.
378            let b ≝ asm_byte_of_beval … prf' in
379            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
380          ]
381        ]
382      | COND _ lbl ⇒ λ_.
383        (* dpm: this should be handled in translate_code! *)
384        Instruction (JNZ ? (toASM_ident ? lbl))
385      ]
386    ].
387  try @I
388  assumption
389qed.
390
391(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
392definition ident_of_label: label → Identifier ≝
393 toASM_ident LabelTag.
394
395definition build_translated_statement ≝
396  λglobals.
397  λglobals_old.
398  λprf.
399  λstatement: lin_statement globals_old.
400    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
401
402definition translate_code ≝
403  λglobals: list (ident × nat).
404  λglobals_old: list ident.
405  λprf.
406  λcode: list (lin_statement globals_old).
407    map ? ? (build_translated_statement globals globals_old prf) code.
408
409definition translate_fun_def ≝
410  λglobals: list (ident × nat).
411  λglobals_old.
412  λprf.
413  λid_def.
414    let 〈id, def〉 ≝ id_def in
415    match def with
416    [ Internal int ⇒
417      let code ≝ joint_if_code LIN globals_old int in
418      match translate_code globals globals_old prf code with
419      [ nil ⇒ ⊥
420      | cons hd tl ⇒
421        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
422          map ? ? (
423            λr.
424            match fst ? ? r with
425            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
426            | None ⇒ 〈None ?, \snd r〉
427            ]) rest
428      ]
429    | External _ ⇒ [ ]
430    ].
431cases daemon (*CSC: XXX will be fixed by an invariant later *)
432qed.
433
434include "common/Identifiers.ma".
435
436let rec flatten_fun_defs
437  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
438    (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
439      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
440  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
441  [ cons hd tl ⇒
442    let fun_def ≝ \snd hd in
443    let fun_id ≝ \fst hd in
444    let translated ≝ translate_fun_def globals globals_old prf hd in
445    let size_translated ≝ | translated | in
446    let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
447    let new_hd ≝ translated @ tail_trans in
448    let new_map ≝ add ? ? tail_map fun_id initial_pc in
449      〈new_hd, new_map〉
450  | nil ⇒ 〈[ ], empty_map …〉
451  ].
452
453definition translate_functs ≝
454  λglobals.
455  λglobals_old.
456  λprf.
457  λexit_label.
458  λmain.
459  λfuncts.
460  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
461  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
462   〈preamble @ flattened, map〉.
463
464(*CSC: region silently thrown away here *)
465definition globals_addr ≝
466 λl.
467  let globals_addr_internal ≝
468   λres_offset.
469   λx_size: ident × region × nat.
470    let 〈res, offset〉 ≝ res_offset in
471    let 〈x, region, size〉 ≝ x_size in
472      〈〈x, offset〉 :: res, offset + size〉
473  in
474    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
475
476(* dpm: plays the role of the string "_exit" in the O'caml source *)
477axiom identifier_prefix: Identifier.
478(*CSC: XXXXXXX wrong anyway since labels from different functions can now
479  clash with each other and with names of functions *)
480axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
481
482(* dpm: fresh prefix stuff needs unifying with brian *)
483definition lin_to_asm : lin_program → pseudo_assembly_program ≝
484  λp.
485  let prog_lbls ≝ program_labels … p in
486  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
487  let global_addr ≝ globals_addr (prog_vars … p) in
488  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
489  let 〈translated, funct_map〉 ≝ translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p) in
490    〈〈funct_map, global_addr'〉, translated〉.
491 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
492 normalize in match prog_var_names; normalize nodelta
493 elim (prog_vars … p) //
494 #hd #tl #IH whd in ⊢ (% → %);
495 whd in match globals_addr; normalize nodelta
496 whd in match (foldl ???? (hd::tl)); normalize nodelta
497 cases hd * #id #reg #size normalize nodelta
498 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
499qed.
Note: See TracBrowser for help on using the repository browser.