Ignore:
Timestamp:
Sep 15, 2011, 4:42:58 PM (8 years ago)
Author:
sacerdot
Message:

Only one axiom left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1215 r1217  
    1616 λaddr1,addr2.
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    18 
    19 axiom address_of_label: bemem → label → address.
    2018
    2119record sem_params: Type[1] ≝
     
    3937 
    4038 ; init_locals : localsT p → regsT
     39 ; pointer_of_label: label → Σp:pointer. ptype p = Code
    4140 }.
     41
     42definition address_of_label: sem_params → label → address.
     43 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label p l)))
     44 cases (beval_pair_of_pointer (pointer_of_label p l)) in ⊢ (???% → ?)
     45  [ #res #_ @res
     46  | #msg cases (pointer_of_label p l) * * #q #com #off #E1 #E2 destruct ]
     47qed.
    4248
    4349record state (p: sem_params): Type[0] ≝
     
    8288 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
    8389
    84 (* CSC: was build_state in RTL *)
    8590definition goto: ∀p:sem_params. label → state p → state p ≝
    86  λp,l,st. set_pc … (address_of_label … (m … st) l) st.
     91 λp,l,st. set_pc … (address_of_label p l) st.
    8792
    8893definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
     
    134139(* removes the top frame from the frames list *)
    135140definition pop_frame: ∀p. state p → res (state p) ≝
    136  (* CSC: monadic notation missing here *)
    137141 λp,st.
    138142  do frames ← pop_frame_ p (st_frms … st);
     
    158162definition save_ra : ∀p. state p → label → res (state p) ≝
    159163 λp,st,l.
    160   let 〈addrl,addrh〉 ≝ address_of_label … (m … st) l in
     164  let 〈addrl,addrh〉 ≝ address_of_label p l in
    161165  do st ← push … st addrl;
    162166  push … st addrh.
     
    272276            ! st ← set_result … vs st;
    273277              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
    274           ]
    275       ]
     278          ]]
    276279    | joint_st_return ⇒
    277280      ! st ← pop_frame … st;
     
    279282      ! 〈st,pcl〉 ← pop … st;
    280283        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
    281     | joint_st_extension c ⇒ exec_extended … p ge c st
    282     ].
     284    | joint_st_extension c ⇒ exec_extended … p ge c st ].
    283285cases addr //
    284286qed.
Note: See TracChangeset for help on using the changeset viewer.