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

new step in code semantic lemma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.