Changeset 2655


Ignore:
Timestamp:
Feb 11, 2013, 4:52:37 PM (6 years ago)
Author:
tranquil
Message:

new step in code semantic lemma

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2645 r2655  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "basics/lists/listb.ma".
    910include "joint/String.ma".
    1011
     
    9798  | POP: acc_a_reg p → joint_seq p globals
    9899  | PUSH: acc_a_arg p → joint_seq p globals
    99   | ADDRESS: ∀i: ident. (member ? (eq_identifier ?) i globals) → dpl_reg p → dph_reg p → joint_seq p globals
     100  | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals
    100101  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    101102  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
  • src/joint/joint_semantics.ma

    r2645 r2655  
    147147  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    148148    bl = Error … [MSG BadFunction].
    149  #F#V#i#p ** #r #id #EQ1 destruct
     149 #F#V#i#p ** #id #EQ1 #EQ2 destruct
    150150 whd in match fetch_internal_function;
    151151  whd in match fetch_function; normalize nodelta
     
    398398  | _ ⇒ Error … [MSG NoSuccessor]
    399399  ].
     400
     401lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A.
     402(x = y → P true) → (x ≠ y → P false) → P (x == y).
     403#A #P #x #y #H1 #H2 inversion (x == y) #EQ
     404[ @H1 @(proj1 … (eqb_true … ) EQ) | @H2 % #EQ' destruct
     405  >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed.
    400406
    401407definition eval_seq_no_pc :
     
    461467  elim globals [*]
    462468  #hd #tl #IH #H elim (orb_Prop_true … H) -H
    463   [@eq_identifier_elim #H * >H %1 % ]
    464   #G %2 @IH @G
     469  [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ]
    465470qed.
    466471
  • src/joint/semantics_blocks.ma

    r2599 r2655  
    3838#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
    3939[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
     40qed.
     41
     42lemma produce_step_trace :
     43  ∀p : evaluation_params.
     44  ∀st : state_pc p.
     45  ∀curr_id,curr_fn.
     46  ∀s : joint_seq p (globals p).
     47  ∀dst : code_point p.
     48  ∀st' : state p.
     49  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     50    return 〈curr_id, curr_fn〉 →
     51  let src ≝ point_of_pc p (pc … st) in
     52  step_in_code … (joint_if_code … curr_fn) src s dst →
     53  eval_seq_no_pc p (globals p) (ev_genv p) curr_id curr_fn s st = return st' →
     54  as_execute (joint_abstract_status p) st
     55    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     56#p #st#curr_id #curr_fn #s #dst #st' #EQfetch * #nxt * #EQstmt_at #EQdst
     57#EQeval whd whd in match eval_state; whd in match eval_statement_no_pc;
     58whd in match fetch_statement; normalize nodelta >EQfetch >m_return_bind
     59>EQstmt_at >m_return_bind normalize nodelta >EQeval >m_return_bind
     60whd in ⊢ (??%%); @eq_f whd in match next; normalize nodelta
     61whd in match (pc ??);  whd in match succ_pc; normalize nodelta >EQdst %
    4062qed.
    4163
Note: See TracChangeset for help on using the changeset viewer.