Changeset 2399 for src/compiler.ma


Ignore:
Timestamp:
Oct 17, 2012, 6:45:20 PM (8 years ago)
Author:
campbell
Message:

Fill in some details about the statement of correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2320 r2399  
    5757include "RTLabs/semantics.ma".
    5858
    59 axiom RTLabs_abstract_status : genv → abstract_status.
    60 
    6159include "joint/Traces.ma".
    6260
    6361include "ASM/Fetch.ma". (* For load_code_memory only *)
    6462
    65 axiom in_clight_program : costlabel → Prop.
    66 
    6763definition lift_cost_map_back_to_front :
    68   ∀code_memory, lbls.
     64  ∀clight, code_memory, lbls.
    6965   (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
    7066       ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
    7167  as_cost_map (ASM_abstract_status code_memory lbls) →
    72   (Σl : costlabel.in_clight_program l) → ℕ ≝ λcode_memory,lbls,dec,k,l_sig.
     68  (Σl : costlabel.in_clight_program clight l) → ℕ ≝ λclight,code_memory,lbls,dec,k,l_sig.
    7369   match dec l_sig with
    7470   [ inl prf ⇒ k «l_sig, prf»
     
    7773
    7874definition compile : clight_program →
    79   res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝
     75  res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝
    8076λp.
    8177  ! 〈init_cost,p',p〉 ← front_end p;
     
    8480  let k ≝ ASM_cost_map p ? in
    8581  let k' ≝ lift_cost_map_back_to_front
     82    p'
    8683    (load_code_memory (\fst p))
    8784    (\snd p)
    8885    ? k
    8986    in
    90   return 〈p, p', k'〉.
     87  return 〈p, ❬p', k'❭〉.
    9188  cases daemon
    9289  qed.
Note: See TracChangeset for help on using the changeset viewer.