source: src/joint/joint_fullexec.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 1.8 KB
Line 
1include "joint/Traces.ma".
2include "common/Measurable.ma".
3
4(* fullexec and co. *)
5record joint_global (p : sem_params) : Type[0] ≝
6{ jglobals : list ident
7; jgenv :> genv p jglobals
8}.
9
10definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝
11λp,gl.mk_evaluation_params (jglobals … gl) p gl.
12
13coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝
14eval_params_of_global on _gl : joint_global ? to evaluation_params.
15
16definition make_joint_global : ∀p : sem_params.
17  (joint_program p × (ident → option ℕ)) →
18  joint_global p ≝
19λpars, p_stack.
20let p ≝ \fst p_stack in
21let stack_sizes ≝ \snd p_stack in
22let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
23mk_joint_global pars
24  (globals … ev_pars)
25  (ev_genv … ev_pars).
26
27definition joint_exec: sem_params → trans_system io_out io_in ≝
28  λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
29   (λenv.joint_final G (jglobals … env) env)
30   (λenv.λst.! st' ← eval_state … env st ;
31    let charge ≝ match joint_label_of_pc env (pc … st) with
32      [ Some c ⇒ Echarge c | None ⇒ E0 ] in
33     return 〈charge, st'〉).
34
35definition joint_fullexec :
36  sem_params → fullexec io_out io_in ≝
37  λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
38    (joint_exec G)
39    (make_joint_global G)
40    (λp_stacks.
41      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
42
43definition joint_preclassified_system : sem_params →
44  preclassified_system ≝
45  λG.mk_preclassified_system (joint_fullexec G)
46    (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st)))
47    (λenv.joint_classify (eval_params_of_global … env))
48    (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s).
Note: See TracBrowser for help on using the repository browser.