Changeset 2489


Ignore:
Timestamp:
Nov 23, 2012, 5:28:25 PM (7 years ago)
Author:
campbell
Message:

Conjecture some Clight/Cminor? simulation results.

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2471 r2489  
    249249
    250250include "Clight/Cexec.ma".
    251 include "Cminor/semantics.ma".
     251include "Clight/abstract.ma".
     252include "Cminor/abstract.ma".
     253
     254(* Invariants used in simulation *)
    252255
    253256record clight_cminor_inv : Type[0] ≝ {
     
    261264      find_funct … ge_cm v = Some ? f'
    262265}.
     266
     267
     268axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
     269
     270(* Conjectured simulation results
     271
     272   We split these based on the start state:
     273   
     274   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
     275      normal steps in Cminor;
     276   2. call and return steps are simulated by a call/return step plus [m] normal
     277      steps (to copy stack allocated parameters / results); and
     278   3. lone cost label steps are simulates by a lone cost label step
     279   
     280   These should allow us to maintain enough structure to identify the Cminor
     281   subtrace corresponding to a measurable Clight subtrace.
     282 *)
     283
     284definition clight_normal : Clight_state → bool ≝
     285λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
     286
     287definition cminor_normal : Cminor_state → bool ≝
     288λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
     289
     290axiom clight_cminor_normal :
     291  ∀INV:clight_cminor_inv.
     292  ∀s1,s1',s2,tr.
     293  clight_cminor_rel INV s1 s1' →
     294  clight_normal s1 →
     295  ¬ Clight_labelled s1 →
     296  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
     297  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
     298    tr = tr' ∧
     299    clight_cminor_rel INV s2 s2'
     300  ).
     301
     302axiom clight_cminor_call_return :
     303  ∀INV:clight_cminor_inv.
     304  ∀s1,s1',s2,tr.
     305  clight_cminor_rel INV s1 s1' →
     306  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
     307  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
     308  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
     309    tr = tr' ∧
     310    clight_cminor_rel INV s2 s2'
     311  ).
     312
     313axiom clight_cminor_cost :
     314  ∀INV:clight_cminor_inv.
     315  ∀s1,s1',s2,tr.
     316  clight_cminor_rel INV s1 s1' →
     317  Clight_labelled s1 →
     318  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
     319  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
     320    tr = tr' ∧
     321    clight_cminor_rel INV s2 s2'
     322  ).
     323
Note: See TracChangeset for help on using the changeset viewer.