Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (8 years ago)
Author:
sacerdot
Message:

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1390 r1395  
    7979 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
    8080
    81 definition address_of_label: sem_params → label → address.
    82  #p #l generalize in match (refl … (address_of_pointer (pointer_of_label … p l)))
    83  cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
    84   [ #res #_ @res
    85   | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 try destruct
    86     normalize in E2; destruct ]
    87 qed.
     81definition address_of_label: sem_params → label → address ≝
     82 λp,l.address_of_code_pointer (pointer_of_label … p l).
    8883
    8984definition set_m: ∀p. bemem → state p → state p ≝
     
    352347
    353348 λpars,sparams.
    354   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ? (globalenv Genv … (λx.[Init_space x]) p)).
    355 cases daemon (*CSC: XXXXXXXXXXXXX*)
    356 qed.
     349 (* Invariant: a -1 block is unused in common/Globalenvs *)
     350 let b ≝ mk_block Code (-1) in
     351 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
     352 let addr ≝ address_of_code_pointer ptr in
     353  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … (λx.[Init_space x]) p)).
     354% qed.
    357355
    358356definition make_initial_state :
Note: See TracChangeset for help on using the changeset viewer.