Changeset 3255 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (7 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r3037 r3255  
    11include "joint/Joint.ma".
    22
    3 inductive move_dst: Type[0] ≝
    4   | PSD: register → move_dst
    5   | HDW: Register → move_dst.
     3inductive psd_or_hdw : Type[0] ≝
     4  | PSD: register → psd_or_hdw
     5  | HDW: Register → psd_or_hdw.
    66
    7 definition move_src ≝ argument move_dst.
     7definition ertl_hdw_readable : Register → Prop ≝
     8λR.match R with
     9  [ RegisterA ⇒ False
     10  | RegisterB ⇒ False
     11  | RegisterDPL ⇒ False
     12  | RegisterDPH ⇒ False
     13  | Register04 (* = RegisterST0 *) ⇒ False
     14  | Register05 (* = RegisterST1 *) ⇒ False
     15  | _ ⇒ True
     16  ].
    817
    9 definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
    10 coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
     18definition ertl_readable ≝
     19λR.match R with
     20[ HDW R ⇒ ertl_hdw_readable R
     21| _ ⇒ True
     22].
     23
     24definition ertl_hdw_writable : Register → Prop ≝
     25λR.match R with
     26  [ Register06 (* = RegisterSPL *) ⇒ False
     27  | Register07 (* = RegisterSPH *) ⇒ False
     28  | _ ⇒ True
     29  ].
     30 
     31definition ertl_writable : psd_or_hdw → Prop ≝
     32λR.match R with
     33[ HDW R ⇒ ertl_hdw_writable R
     34| _ ⇒ True
     35].
     36
     37definition move_dst ≝ Σr : psd_or_hdw.ertl_writable r.
     38unification hint 0 ≔ ⊢ move_dst ≡ Sig psd_or_hdw (λr.ertl_writable r).
     39
     40definition move_src ≝ argument (Σr : psd_or_hdw.ertl_readable r).
     41
     42definition move_src_from_reg :
     43  (Σr.ertl_readable r) → move_src ≝ Reg ?.
     44coercion reg_to_move_src :
     45  ∀r : (Σr : psd_or_hdw.ertl_readable r).move_src ≝
     46  move_src_from_reg on _r : Sig psd_or_hdw ? to move_src.
    1147
    1248definition psd_argument_move_src : psd_argument → move_src ≝
    13   λarg.match arg with
     49  λarg.match arg return λ_.move_src with
    1450  [ Imm b ⇒ Imm ? b
    1551  | Reg r ⇒ Reg ? (PSD r)
    16   ].
     52  ]. @I qed.
    1753coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
    1854  psd_argument_move_src on _a : psd_argument to move_src.
    1955
    2056inductive ertl_seq : Type[0] ≝
    21   | ertl_new_frame: ertl_seq
    22   | ertl_del_frame: ertl_seq
    2357  | ertl_frame_size: register → ertl_seq.
    2458
Note: See TracChangeset for help on using the changeset viewer.