Changeset 1882 for src/joint


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

Location:
src/joint
Files:
2 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1419 r1882  
    4444     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
    4545
     46definition is_addressable : region → bool ≝ λr.match r with
     47  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
     48
     49
     50definition is_address : (beval × beval) → Prop ≝ λa.
     51  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
     52    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
     53    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
     54
     55definition is_addressb : (beval × beval) → bool ≝ λa.
     56  match a with
     57  [ mk_Prod a0 a1 ⇒
     58    match a0 with
     59    [ BVptr p0 part0 ⇒
     60      is_addressable (ptype p0) ∧ eqb part0 0 ∧
     61        match a1 with
     62        [ BVptr p1 part1 ⇒
     63          eq_pointer p0 p1 ∧ eqb part1 1
     64        | _ ⇒ false
     65        ]
     66    | _ ⇒ false
     67    ]
     68  ].
     69
     70lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
     71  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
     72#P * *
     73[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
     74#p0 #part0 #a1
     75whd in match is_addressb; normalize nodelta
     76elim (true_or_false_Prop (is_addressable (ptype p0)))
     77#H >H
     78[ @(eqb_elim part0 0) #Heq
     79  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
     80    [4: @eq_pointer_elim #Heq'
     81      [ @(eqb_elim part1 1) #Heq''
     82        [ #Ptrue #_ @Ptrue destruct
     83          %{p1} [assumption] %{part0} %{part1}
     84          % [ % [ % ]] try % assumption
     85        ]
     86      ]
     87    ]
     88  ]
     89]
     90#_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
     91#H0 #H1 #H2 #H3 destruct /2 by absurd/
     92qed.
     93
    4694(* CSC: only pointers to XRAM or code memory ATM *)
    4795definition address ≝ beval × beval.
     96definition safe_address ≝ Sig address is_address.
     97unification hint 0 ≔ ;
     98P ≟ Prod beval beval
     99(*------------------*)⊢
     100safe_address ≡ Sig P is_address.
    48101
    49102definition eq_address: address → address → bool ≝
     
    53106definition pointer_of_address: address → res pointer ≝
    54107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    55 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
    56 
    57 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
     108 
     109definition pointer_of_address_safe : safe_address → pointer ≝
     110  λp.match \fst p return λx.\fst p = x → ? with
     111    [ BVptr ptr _ ⇒ λ_.ptr
     112    | _ ⇒ λabs.⊥
     113    ] (refl …).
     114lapply abs -abs cases p
     115* #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
     116destruct(H0 H4)
     117qed.
     118
     119definition pointer_compat' ≝ λb,r.
     120  match b with
     121  [ mk_block r' z ⇒
     122    if eq_region r' r then True
     123    else
     124      match r with
     125      [ Any ⇒ True
     126      | XData ⇒ match r' with
     127        [ PData ⇒ True
     128        | _ ⇒ False
     129        ]
     130      | _ ⇒ False
     131      ]
     132   ].
     133
     134lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
     135** #z ** //
     136qed.
     137
     138lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
     139#b #r #H inversion H
     140[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
     141| #id #EQ1 #EQ2 #EQ3 %
     142| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
     143]
     144qed.
     145
     146lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     147** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
     148cases r in Hr ⊢ %; #Hr *
     149** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
     150destruct normalize
     151@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     152@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     153#_ #_ normalize %
     154qed.
     155   
     156definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
     157
     158example address_of_pointer_OK_to_safe :
     159  ∀p,a.address_of_pointer p = OK … a → is_address a.
     160#p
     161lapply (refl … p)
     162generalize in match p in ⊢ (???%→%); **
     163whd in match (address_of_pointer ?);
     164#b #H #o #EQp * #a0 #a1
     165normalize #EQ destruct(EQ)
     166%{p} >EQp [1,3: %]
     167% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
     168qed.
     169
     170definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
     171  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
     172
     173lemma address_of_pointer_is_safe :
     174  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
     175****#z #H
     176lapply (pointer_compat_from_ind ?? H) * #o
     177normalize %
     178qed.
     179
     180definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
     181code_pointer_of_beval_pair.
     182
    58183definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
    59184
     185definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
     186cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     187lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     188%{«mk_pointer ? (mk_block Code z) H o,I»}
     189% [2: % [2: % [ % [ % ]] % |]|]
     190qed.
     191
     192(* Paolo: why only code pointers and not XRAM too? *)
    60193definition addr_add: address → nat → res address ≝
    61194 λaddr,n.
     
    65198qed.
    66199
     200definition safe_addr_add: safe_address → nat → res safe_address ≝
     201 λaddr,n.
     202  do ptr ← code_pointer_of_address addr ;
     203  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
     204normalize cases ptr #p #E @E
     205qed.
     206
    67207definition addr_sub: address → nat → res address ≝
    68208 λaddr,n.
     
    71211normalize cases ptr #p #E @E
    72212qed.
     213
     214definition safe_addr_sub: safe_address → nat → res safe_address ≝
     215 λaddr,n.
     216  do ptr ← code_pointer_of_address addr ;
     217  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
     218normalize cases ptr #p #E @E
     219qed.
  • src/joint/Joint_paolo.ma

    r1644 r1882  
    44include "common/Registers.ma".
    55include "common/Graphs.ma".
     6include "utilities/lists.ma".
     7include "common/LabelledObjects.ma".
     8include "ASM/Util.ma".
    69
    710(* Here is the structure of parameter records (downward edges are coercions,
     
    1215
    1316        lin_params      graph_params
    14           |       \_____ /____   |
    15           |             /     \  |
    16           \_______     /      ↓  ↓
    17                   \   _\____ params
    18                    \_/  \      |
    19                     / \  \     ↓
    20               _____/   unserialized_params
    21              /      _______/   |
    22             /      /           |
    23      stmt_params  /   local_params
    24         |      __/             |
    25     inst_params       funct_params
    26 
    27 inst_params : types needed to define instructions
     17              |   \_____ /____   |
     18              |         /     \  |
     19              |        /      ↓  ↓
     20              |       |      params
     21              |       |        |
     22              |       |   stmt_params
     23              |       |    /   
     24          unserialized_params             
     25            |            \       
     26            |             \     
     27            |         local_params
     28            |              |   
     29    step_params       funct_params
     30
     31step_params : types needed to define steps (stmts with a default fallthrough)
    2832stmt_params : adds successor type needed to define statements
    2933funct_params : types of result register and parameters of function
    3034local_params : adds types of local registers
    31 params : adds type of code and lookup function
    32 graph_params : is made just of inst_params and local_params, and the coercion
    33   to params adds structure common to graph languages *)
    34 
    35 record inst_params : Type[1] ≝
     35params : adds type of code and related properties *)
     36
     37record step_params : Type[1] ≝
    3638 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
    3739 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     
    4648 ; call_args: Type[0] (* arguments of function calls *)
    4749 ; call_dest: Type[0] (* possible destination of function computation *)
    48  ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
    49  ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
    50  ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
    51  ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
     50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
     51 ; ext_step_labels : ext_step → list label
     52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     53 ; ext_fin_stmt_labels : ext_fin_stmt → list label
    5254 }.
    5355 
    54 inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
    55   | COMMENT: String → joint_instruction p globals
    56   | COST_LABEL: costlabel → joint_instruction p globals
    57   | MOVE: pair_move p → joint_instruction p globals
    58   | POP: acc_a_reg p → joint_instruction p globals
    59   | PUSH: acc_a_arg p → joint_instruction p globals
    60   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    61   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
    62   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    63   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
     56inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
     57  | COMMENT: String → joint_step p globals
     58  | COST_LABEL: costlabel → joint_step p globals
     59  | MOVE: pair_move p → joint_step p globals
     60  | POP: acc_a_reg p → joint_step p globals
     61  | PUSH: acc_a_arg p → joint_step p globals
     62  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
     63  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
     64  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
     65  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
    6466  (* int done with generic move *)
    65 (*| INT: generic_reg p → Byte → joint_instruction p globals *)
    66   | CLEAR_CARRY: joint_instruction p globals
    67   | SET_CARRY: joint_instruction p globals
    68   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
    69   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
    70   | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    71   | COND: acc_a_reg p → label → joint_instruction p globals
    72   | extension: ext_instruction p → joint_instruction p globals.
    73 
    74 coercion extension_to_instruction :
    75   ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
    76   extension
    77   on _c : ext_instruction ? to joint_instruction ??.
    78 
    79 notation "r ← a1 .op. a2" with precedence 50 for
     67(*| INT: generic_reg p → Byte → joint_step p globals *)
     68  | CLEAR_CARRY: joint_step p globals
     69  | SET_CARRY: joint_step p globals
     70  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
     71  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
     72  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
     73  | COND: acc_a_reg p → label → joint_step p globals
     74  | extension: ext_step p → joint_step p globals.
     75
     76notation "r ← a1 .op. a2" with precedence 55 for
    8077  @{'op2 $op $r $a1 $a2}.
    81 notation "r ← . op . a" with precedence 50 for
     78notation "r ← . op . a" with precedence 55 for
    8279  @{'op1 $op $r $a}.
    83 notation "r ← a" with precedence 50 for
     80notation "r ← a" with precedence 55 for
    8481  @{'mov $r $a}. (* to be set in individual languages *)
    8582notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     
    9087interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9188
    92 
    93 definition inst_forall_labels : ∀p : inst_params.∀globals.
    94     (label → Prop) → joint_instruction p globals → Prop ≝
    95 λp,g,P,inst. match inst with
    96   [ COND _ l ⇒ P l
    97   | extension ext_s ⇒ ext_forall_labels p P ext_s
    98   | _ ⇒ True
    99  ].
    100 
     89coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
     90  extension on _s : ext_step ? to joint_step ??.
     91
     92definition step_labels ≝
     93  λp, globals.λs : joint_step p globals.
     94    match s with
     95    [ COND _ l ⇒ [l]
     96    | extension ext_s ⇒ ext_step_labels ? ext_s
     97    | _ ⇒ [ ]
     98    ].
     99
     100definition step_forall_labels : ∀p : step_params.∀globals.
     101    (label → Prop) → joint_step p globals → Prop ≝
     102λp,g,P,inst. All … P (step_labels … inst).
     103 
    101104record funct_params : Type[1] ≝
    102105  { resultT : Type[0]
     
    109112 }.
    110113
     114
    111115record unserialized_params : Type[1] ≝
    112  { u_inst_pars :> inst_params
     116 { u_inst_pars :> step_params
    113117 ; u_local_pars :> local_params
    114118 }.
    115119
    116120record stmt_params : Type[1] ≝
    117   { unserialized_pars :> unserialized_params
     121  { uns_pars :> unserialized_params
    118122  ; succ : Type[0]
    119   ; succ_forall_labels : (label → Prop) → succ → Prop
     123  ; succ_label : succ → option label
    120124  }.
    121125
    122126inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    123   | sequential: joint_instruction p globals → succ p → joint_statement p globals
     127  | sequential: joint_step p globals → succ p → joint_statement p globals
    124128  | GOTO: label → joint_statement p globals
    125129  | RETURN: joint_statement p globals
    126   | extension_fin : ext_fin_instruction p → joint_statement p globals.
    127 
    128 coercion extension_fin_to_statement :
    129   ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
    130   extension_fin
    131   on _c : ext_fin_instruction ? to joint_statement ??.
     130  | extension_fin : ext_fin_stmt p → joint_statement p globals.
     131
     132coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
     133  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
     134
     135definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
     136  match s with
     137  [ sequential _ _ ⇒ False
     138  | _ ⇒ True
     139  ].
    132140
    133141record params : Type[1] ≝
    134142 { stmt_pars :> stmt_params
    135143 ; codeT: list ident → Type[0]
    136  ; code_has_label: ∀globals.codeT globals → label → Prop
    137  ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
    138     codeT globals → Prop
     144 ; code_point : Type[0]
     145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
     146 ; point_of_label : ∀globals.codeT globals → label → option code_point
     147 ; point_of_succ : code_point → succ stmt_pars → code_point
    139148 }.
    140149
    141 
    142 definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    143     (label → Prop) → joint_statement p globals → Prop ≝
    144   λp,g,P,stmt. match stmt with
    145   [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
    146   | GOTO l ⇒ P l
    147   | RETURN ⇒ True
    148   | extension_fin c ⇒ ext_fin_forall_labels … P c
     150definition code_has_point ≝
     151  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
     152
     153interpretation "code membership" 'mem p c = (code_has_point ?? c p).
     154
     155definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     156unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
     157
     158definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
     159  match pt with
     160  [ mk_Sig pt' pt_prf ⇒
     161    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
     162    [ Some x ⇒ λ_.x
     163    | None ⇒ λabs.⊥
     164    ] (refl …)
     165  ]. normalize in pt_prf;
     166    >abs in pt_prf; // qed.
     167
     168definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     169  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
     170
     171definition forall_statements_i :
     172  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
     173    codeT p globals → Prop  ≝
     174  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
     175
     176lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
     177#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     178
     179lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
     180  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
     181#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     182
     183definition code_has_label ≝ λp,globals,c,l.
     184  match point_of_label p globals c l with
     185  [ Some pt ⇒ code_has_point … c pt
     186  | None ⇒ false
    149187  ].
     188
     189definition stmt_explicit_labels :
     190  ∀p,globals.
     191  joint_statement p globals → list label ≝
     192  λp,globals,stmt. match stmt with
     193  [ sequential c _ ⇒ step_labels … c
     194  | GOTO l ⇒ [ l ]
     195  | RETURN ⇒ [ ]
     196  | extension_fin c ⇒ ext_fin_stmt_labels … c
     197  ].
     198
     199definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
     200  option label ≝
     201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
     202 
     203definition stmt_labels : ∀p : stmt_params.∀globals.
     204    joint_statement p globals → list label ≝
     205  λp,g,stmt.
     206  (match stmt_implicit_label … stmt with
     207     [ Some l ⇒ [l]
     208     | None ⇒ [ ]
     209     ]) @ stmt_explicit_labels … stmt.
     210
     211definition stmt_forall_labels ≝
     212  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
     213  All … P (stmt_labels … s).
     214
     215lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     216  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
     217#p#globals#P #s
     218whd in ⊢ (% → ?);
     219whd in ⊢ (???% → ?);
     220elim (stmt_implicit_label ???) [2: #next * #_] //
     221qed.
     222
     223lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
     224  stmt_forall_labels … P s →
     225    opt_All … P (stmt_implicit_label … s).
     226#p#globals#P#s
     227whd in ⊢ (% → ?);
     228whd in ⊢ (???% → ?);
     229elim (stmt_implicit_label ???)
     230[ //
     231| #next * #Pnext #_ @Pnext
     232]
     233qed.
     234
     235definition code_forall_labels ≝
     236  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
     237
     238lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
     239  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
     240  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
    150241
    151242record lin_params : Type[1] ≝
    152243  { l_u_pars :> unserialized_params }.
    153 
    154 include "utilities/option.ma".
     244 
     245lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     246#tag #A #lbl #l elim l [*]
     247** [2: #id] #a #tl #IH
     248[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
     249  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
     250  @eq_identifier_elim #Heq normalize nodelta
     251  [ #_ normalize / by /]
     252| whd in ⊢ (?%→?%?);
     253]
     254#H >(index_of_label_from_internal … H)
     255@le_S_S @(IH H)
     256qed.
     257
     258(* mv *)
     259lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
     260#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
     261#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
     262qed.
     263
     264lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
     265#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
     266#n' #H @le_S_S @(IH … H)
     267qed.
     268
     269lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
     270#A #l elim l
     271[ #n #ABS @⊥ /2 by absurd/
     272| #hd #tl #IH * normalize //
     273]
     274qed.
    155275
    156276definition lin_params_to_params ≝
    157277  λlp : lin_params.
    158278     mk_params
    159       (mk_stmt_params lp unit (λ_.λ_.True))
     279      (mk_stmt_params lp unit (λ_.None ?))
    160280    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    161     (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
    162         (λl_stmt. \fst l_stmt = Some ? lbl) code)
    163     (* forall_statements ≝ *)(λglobals,P,code.All ?
    164         (λl_stmt. P (\snd l_stmt)) code).
     281    (* code_point ≝ *)ℕ
     282    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
     283    (* point_of_label ≝ *)(λglobals,c,lbl.
     284      If occurs_exactly_once ?? lbl c then with prf do
     285        return index_of_label ?? lbl c
     286      else
     287        None ?)
     288    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
    165289
    166290coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
    167291  on _lp : lin_params to params.
     292 
     293lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     294  ∀pt.pt ∈ code = leb (S pt) (|code|).
     295#lp #globals #code elim code
     296[ #pt %
     297| #hd #tl #IH * [%]
     298  #n @IH
     299]qed.
     300
     301lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     302  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
     303#lp #globals #code #lbl
     304whd in match (code_has_label ????);
     305whd in match (point_of_label ????);
     306elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
     307#Heq >Heq normalize nodelta
     308[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
     309  #ABS elim(absurd ?? ABS) -ABS
     310  @index_of_label_length assumption ]] %
     311qed.
    168312
    169313record graph_params : Type[1] ≝
    170314  { g_u_pars :> unserialized_params }.
     315
     316(* move *)
     317definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
     318  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
     319  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
     320    [ an_identifier i' ⇒
     321      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
     322      [ Some y ⇒ λ_.y
     323      | None ⇒ Ⓧ
     324      ]
     325    ]
     326  ].
     327 
     328lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
     329  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
     330#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
     331[ * ]
     332#s * #H @H %
     333qed.
    171334
    172335(* One common instantiation of params via Graphs of joint_statements
     
    175338  λgp : graph_params.
    176339     mk_params
    177       (mk_stmt_params gp label (λP.P))
     340      (mk_stmt_params gp label (Some ?))
    178341    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    179     (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
    180     (* forall_statements ≝ *)(λglobals,P,code.
    181       ∀l,s.lookup … code l = Some ? s → P s).
    182    
     342    (* code_point ≝ *)label
     343    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
     344    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
     345    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
     346
    183347coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    184348on _gp : graph_params to params.
    185    
    186 
    187 definition labels_present : ∀globals.∀p : params.
    188   codeT p globals → (joint_statement p globals) → Prop ≝
    189 λglobals,p,code,s. stmt_forall_labels p globals
    190   (λl.code_has_label ?? code l) s.
     349
     350lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     351  ∀pt.code_has_point … code pt = mem_set … code pt.
     352#gp#globals*#m*#i % qed.
     353
     354lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     355  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
     356#gp #globals * #m * #i % qed.
     357
     358definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     359  λs : joint_statement p globals.
     360  match s with
     361  [ sequential _ n ⇒ P n
     362  | _ ⇒ True
     363  ].
     364
     365definition statement_closed : ∀globals.∀p : params.
     366  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
     367λglobals,p,code,pt,s.
     368  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
     369  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
    191370
    192371definition code_closed : ∀p : params.∀globals.
    193372  codeT p globals → Prop ≝ λp,globals,code.
    194     forall_statements … (labels_present … code) code.
     373    forall_statements_i … (statement_closed … code) code.
    195374
    196375(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    197376definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
    198   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
     377  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    199378
    200379record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
     
    206385  joint_if_result   : resultT p;
    207386  joint_if_params   : paramsT p;
    208   joint_if_locals   : localsT p;
     387  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    209388(*CSC: XXXXX stacksize unused for LTL-...*)
    210389  joint_if_stacksize: nat;
    211390  joint_if_code     : codeT p globals ;
    212 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    213   joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    214 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    215   joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
     391  joint_if_entry : point_in_code … joint_if_code ;
     392  joint_if_exit : point_in_code … joint_if_code
    216393}.
    217394
     
    219396  λglobals,p.
    220397    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    221 
    222 (* Currified form *)
    223 definition set_joint_if_exit ≝
    224   λglobals,pars.
    225   λexit: label.
    226   λp:joint_internal_function globals pars.
    227   λprf: code_has_label … (joint_if_code … p) exit.
    228    mk_joint_internal_function globals pars
    229     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    230     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    231     (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
    232398
    233399definition set_joint_code ≝
     
    244410
    245411definition set_joint_if_graph ≝
    246   λglobals,pars.
     412  λglobals.λpars : graph_params.
    247413  λgraph.
    248414  λp:joint_internal_function globals pars.
    249   λentry_prf: code_has_label … graph (joint_if_entry … p).
    250   λexit_prf: code_has_label … graph (joint_if_exit … p).
     415  λentry_prf.
     416  λexit_prf.
    251417    set_joint_code globals pars p
    252418      graph
    253       (mk_Sig … (joint_if_entry … p) entry_prf)
    254       (mk_Sig … (joint_if_exit p) exit_prf).
     419      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
     420      (mk_Sig … (joint_if_exit ?? p) exit_prf).
    255421
    256422definition set_luniverse ≝
     
    272438    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    273439   
    274 (* Paolo: probably should move these elsewhere *)
    275 definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
    276 definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
    277   graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
    278   mk_Sig … (pi1 ?? sig_l) ?.
    279 @graph_add_lookup
    280 @(pi2 … sig_l)
    281 qed.
    282 
    283440(* Specialized for graph_params *)
    284441definition add_graph ≝
     
    290447     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    291448     code
    292      (graph_dom_add_incl … (joint_if_entry … p))
    293      (graph_dom_add_incl … (joint_if_exit … p)).
     449     (pi1 … (joint_if_entry … p))
     450     (pi1 … (joint_if_exit … p)).
     451>graph_code_has_point whd in match code; >mem_set_add
     452@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     453#x #H <graph_code_has_point @H
     454qed.
    294455
    295456definition set_locals ≝
  • src/joint/TranslateUtils_paolo.ma

    r1643 r1882  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.λX,T : Type[0].
    8    T → state_monad (joint_internal_function … g pars) X.
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
    98
    109definition rtl_ertl_fresh_reg:
    1110 ∀inst_pars,funct_pars,globals.
    12   freshT globals (rtl_ertl_params inst_pars funct_pars) register unit
    13   λinst_pars,var_pars,globals,it,def.
     11  freshT globals (rtl_ertl_params inst_pars funct_pars) register
     12  λinst_pars,var_pars,globals,def.
    1413    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    1514    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    1615
     16include alias "basics/lists/list.ma".
    1717let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
    18   freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝
    19   match n with
    20   [ O ⇒ λ_. return [ ]
    21   | S n' ⇒ λ_.
    22     ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it;
    23     ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it;
    24     return (reg :: regs')
    25   ].
    26 
    27 lemma rtl_ertl_fresh_regs_length:
    28  ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals
    29   (rtl_ertl_params i_pars f_pars). ∀n: nat.
    30   |(\snd (rtl_ertl_fresh_regs … n it def))| = n.
    31  #ipars#fpars #globals #def #n elim n
    32   [ %
    33   | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    34     #def' #regs #EQ>EQ
    35     whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ]
    36 qed.
    37 
    38 definition rtl_ertl_fresh_regs_strong:
    39  ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) →
    40   ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝
    41  λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. //
    42 qed.
     18  freshT globals (rtl_ertl_params inst_pars funct_pars)
     19    (Σl : list register. |l| = n) ≝
     20  let ret_type ≝ (Σl : list register. |l| = n) in
     21  match n  return λx.x = n → freshT … ret_type with
     22  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
     23  | S n' ⇒ λeq'.
     24    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
     25    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
     26    return (mk_Sig … (reg :: regs') ?)
     27  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
     28  qed.
    4329
    4430definition fresh_label:
    45  ∀g_pars,globals.freshT globals g_pars label unit
    46   λg_pars,globals,it,def.
     31 ∀g_pars,globals.freshT globals g_pars label
     32  λg_pars,globals,def.
    4733    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    4834     〈set_luniverse … def luniverse, r〉.
     
    5238  (g_pars: graph_params)
    5339  (globals: list ident)
    54   (insts: list (joint_instruction g_pars globals))
     40  (insts: list (joint_step g_pars globals))
    5541  (src : label)
    5642  (dest : label)
     
    6349      add_graph … src (sequential … instr dest) def
    6450    | _ ⇒ (* need to generate label *)
    65       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     51      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    6652      adds_graph g_pars globals others tmp_lbl dest
    6753        (add_graph … src (sequential … instr tmp_lbl) def)
     
    7258  ∀g_pars: graph_params.
    7359  ∀globals: list ident.
    74   (* type of allocatable registers and of their types (unit if not in RTLabs) *)
    75   ∀R,T : Type[0].
    7660  (* fresh register creation *)
    77   freshT globals g_pars R T
    78   ∀insts: bind_list R T (joint_instruction g_pars globals).
     61  freshT globals g_pars (localsT … g_pars)
     62  ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    7963  ∀src : label.
    8064  ∀dest : label.
    8165  joint_internal_function globals g_pars →
    8266  joint_internal_function globals g_pars ≝
    83   λg_pars,globals,T,R,fresh_r,insts,src,dest,def.
     67  λg_pars,globals,fresh_r,insts,src,dest,def.
    8468  let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    8569  adds_graph … stmts src dest def'.
     
    8973  ∀src_g_pars,dst_g_pars : graph_params.
    9074  ∀globals: list ident.
    91   (* type of allocatable registers (unit if not in RTLabs) *)
    92   ∀T : Type[0].
    9375  (* fresh register creation *)
    94   freshT globals dst_g_pars (localsT dst_g_pars) T
     76  freshT globals dst_g_pars (localsT dst_g_pars)
    9577  (* function dictating the translation *)
    96   (label → joint_instruction src_g_pars globals →
    97     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     78  (label → joint_step src_g_pars globals →
     79    bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    9880    (* this can be added to allow redirections: × label *)) →
    99   (label → ext_fin_instruction src_g_pars →
    100     (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
    101     ×
    102     (joint_statement dst_g_pars globals)) →
     81  (label → ext_fin_stmt src_g_pars →
     82     bind_new (localsT dst_g_pars)
     83      ((list (joint_step dst_g_pars globals))
     84      ×
     85      (joint_statement dst_g_pars globals))) →
    10386  (* initialized function definition with empty graph *)
    10487  joint_internal_function globals dst_g_pars →
     
    10790  (* destination function *)
    10891  joint_internal_function globals dst_g_pars ≝
    109   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
     92  λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
    11093  let f : label → joint_statement (src_g_pars : params) globals →
    11194    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    11598    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    11699    | RETURN ⇒ add_graph … lbl (RETURN …) def
    117     | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    118       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
    119       b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
     100    | extension_fin c ⇒
     101      let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
     102      let 〈insts, fin〉 ≝ p in
     103      let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
     104      adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
    120105    ] in
    121106  foldi … f (joint_if_code … def) empty.
    122 
    123 definition b_graph_translate_no_fin :
    124   ∀src_g_pars : graph_params.
    125   ext_fin_instruction src_g_pars = void →
    126   ∀dst_g_pars : graph_params.
    127   ∀globals: list ident.
    128   (* type of allocatable registers (unit if not in RTLabs) *)
    129   ∀T : Type[0].
    130   (* fresh register creation *)
    131   freshT globals dst_g_pars (localsT dst_g_pars) T →
    132   (* function dictating the translation *)
    133   (label → joint_instruction src_g_pars globals →
    134     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    135     (* this can be added to allow redirections: × label *)) →
    136   (* initialized function definition with empty graph *)
    137   joint_internal_function globals dst_g_pars →
    138   (* source function *)
    139   joint_internal_function globals src_g_pars →
    140   (* destination function *)
    141   joint_internal_function globals dst_g_pars ≝
    142   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
    143     b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
    144       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    145107 
    146108(* translation without register allocation *)
     
    149111  ∀globals: list ident.
    150112  (* function dictating the translation *)
    151   (label → joint_instruction src_g_pars globals →
    152     list (joint_instruction dst_g_pars globals)) →
    153   (label → ext_fin_instruction src_g_pars →
    154     (list (joint_instruction dst_g_pars globals))
     113  (label → joint_step src_g_pars globals →
     114    list (joint_step dst_g_pars globals)) →
     115  (label → ext_fin_stmt src_g_pars →
     116    (list (joint_step dst_g_pars globals))
    155117    ×
    156118    (joint_statement dst_g_pars globals)) →
     
    171133    | RETURN ⇒ add_graph … lbl (RETURN …) def
    172134    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    173       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     135      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    174136      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    175137    ] in
    176138  foldi ??? f (joint_if_code ?? def) empty.
     139
     140definition graph_to_lin_statement :
     141  ∀p : unserialized_params.∀globals.
     142  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
     143  λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
     144  [ sequential c _ ⇒ sequential … c it
     145  | GOTO l ⇒ GOTO … l
     146  | RETURN ⇒ RETURN …
     147  | extension_fin c ⇒ extension_fin … c
     148  ].
     149
     150lemma graph_to_lin_labels :
     151  ∀p : unserialized_params.∀globals,s.
     152  stmt_labels … (graph_to_lin_statement p globals s) =
     153  stmt_explicit_labels … s.
     154#p#globals * //
     155qed.
     156
     157(* in order to make the coercion from lists to sets to work, one needs these hints *)
     158unification hint 0 ≔ ;
     159X ≟ identifier LabelTag
     160
     161list label ≡ list X.
     162
     163unification hint 0 ≔ ;
     164X ≟ identifier RegisterTag
     165
     166list register ≡ list X.
     167
     168   
     169definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
     170definition hide_Prop : Prop → Prop ≝ λP.P.
     171
     172interpretation "hide proof" 'hide p = (hide_prf ? p).
     173interpretation "hide Prop" 'hide p = (hide_Prop p).
     174
     175(* discard all elements failing test, return first element succeeding it *)
     176(* and the rest of the list, if any. *)
     177let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
     178  match l with
     179  [ nil ⇒ None ?
     180  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
     181  ].
     182
     183lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
     184  let x ≝ \fst pr in
     185  let post ≝ \snd pr in
     186  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
     187#A#f#l elim l
     188[ normalize * #x #post #EQ destruct
     189| #y #l' #Hi * #x #post
     190  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
     191  #EQ
     192  [ destruct >fy %{[ ]} /3 by refl, conj, I/
     193  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
     194    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
     195  ]
     196]
     197qed.
     198
     199lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
     200#A#f#l elim l
     201[ normalize #_ %
     202| #y #l' #Hi normalize
     203  elim (true_or_false_Prop (f y)) #fy >fy normalize
     204  #EQ
     205  [ destruct
     206  | /3 by conj, nmk/
     207  ]
     208]
     209qed.
     210
     211unification hint 0 ≔ p, globals;
     212lp ≟ lin_params_to_params p,
     213sp ≟ stmt_pars lp,
     214js ≟ joint_statement sp globals,
     215lo ≟ labelled_obj LabelTag js
     216(*----------------------------*)⊢
     217list lo ≡ codeT lp globals.
     218
     219definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     220  λentry : label.
     221  (Σ〈visited'   : identifier_map LabelTag ℕ,
     222   required'  : identifier_set LabelTag,
     223   generated' : codeT (mk_lin_params p) globals〉.'hide (
     224      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
     225        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
     226        (∀l,n.lookup ?? visited' l = Some ? n →
     227          And (code_has_label … (rev ? generated') l)
     228            (∃s.And (And
     229              (lookup … g l = Some ? s)
     230              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     231              (opt_All ?
     232                (λnext.Or (lookup … visited' next = Some ? (S n))
     233                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
     234                (stmt_implicit_label … s)))))).
     235               
     236unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
     237
     238let rec graph_visit
     239  (p : unserialized_params)
     240  (globals: list ident)
     241  (g : codeT (mk_graph_params p) globals)
     242  (* = graph (joint_statement (mk_graph_params p) globals *)
     243  (required: identifier_set LabelTag)
     244  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
     245  (generated: codeT (mk_lin_params p) globals)
     246  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
     247  (visiting: list label)
     248  (gen_length : ℕ)
     249  (n: nat)
     250  (entry : label)
     251  (g_prf : code_closed … g)
     252  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
     253  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
     254  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
     255    And (code_has_label … (rev ? generated) l)
     256    (∃s.And (And
     257      (lookup … g l = Some ? s)
     258      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     259      (opt_All ? (λnext.match lookup … visited next with
     260                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
     261                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
     262  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
     263  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
     264  (gen_length_prf : gen_length = length ? generated)
     265  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
     266                  (lookup … visited entry = Some ? 0))
     267  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
     268  on n
     269  : graph_visit_ret_type … g entry ≝
     270  match chop ? (λx.¬x∈visited) visiting
     271  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
     272  [ None ⇒ λeq_chop.
     273    let H ≝ chop_miss … eq_chop in
     274    mk_Sig … 〈visited, required, generated〉 ?
     275  | Some pr ⇒ λeq_chop.
     276    let vis_hd ≝ \fst pr in
     277    let vis_tl ≝ \snd pr in
     278    let H ≝ chop_hit ???? eq_chop in
     279    match n return λx.x = n → graph_visit_ret_type … g entry with
     280    [ O ⇒ λeq_n.⊥
     281    | S n' ⇒ λeq_n.
     282      (* add the label to the visited ones *)
     283      let visited' ≝ add … visited vis_hd gen_length in
     284      (* take l's statement *)
     285      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 
     286      (* translate it to its linear version *)
     287      let translated_statement ≝ graph_to_lin_statement p globals statement in
     288      (* add the translated statement to the code (which will be reversed later) *)
     289      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
     290      let required' ≝ stmt_explicit_labels … statement ∪ required in
     291      (* put successors in the visiting worklist *)
     292      let visiting' ≝ stmt_labels … statement @ vis_tl in
     293      (* finally, check the implicit successor *)
     294      (* if it has been already visited, we need to add a GOTO *)
     295      let add_req_gen ≝ match stmt_implicit_label … statement with
     296        [ Some next ⇒
     297          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
     298        | None ⇒ 〈0, ∅, [ ]〉
     299        ] in
     300      graph_visit ???
     301        (\snd (\fst add_req_gen) ∪ required')
     302        visited'
     303        (\snd add_req_gen @ generated')
     304        visiting'
     305        (\fst (\fst add_req_gen) + S(gen_length))
     306        n' entry g_prf ????????
     307    ] (refl …)
     308  ] (refl …).
     309whd
     310[ (* base case, visiting is all visited *)
     311  %[
     312    %[
     313      %[
     314        elim entry_prf
     315        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
     316          * #ABS elim (ABS I)
     317        | //
     318        ]
     319      | #l #l_req
     320        elim (required_prf1 … l_req) #G
     321        [ lapply (All_In … H G) #H >(notb_false ? H) %
     322        | assumption
     323        ]
     324      ]
     325    | assumption
     326    ]
     327   | #l #n #H elim (generated_prf1 … H)
     328      #H1 * #s ** #H2 #H3 #H4
     329      % [assumption] %{s} %
     330      [% assumption
     331      | @(opt_All_mp … H4) -l #l
     332        lapply (in_map_domain … visited l)
     333        elim (true_or_false (l∈visited)) #l_vis >l_vis
     334        normalize nodelta [ * #n' ] #EQlookup >EQlookup
     335        normalize nodelta *
     336        [ #EQn' % >EQn' %
     337        | #H %2{H}
     338        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
     339        ]
     340      ]
     341    ]
     342|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
     343(* first, close goals where add_gen_req plays no role *)
     344[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
     345|1: (* n = 0 absrud *)
     346  @(absurd … n_prf)
     347  @lt_to_not_le
     348  <eq_n
     349  lapply (add_size … visited vis_hd 0 (* dummy value *))
     350  >(notb_true … H3)
     351  whd in match (if ? then ? else ?);
     352  whd in match (? + ?);
     353  whd in match (lt ? ?);
     354  #EQ <EQ @subset_card @add_subset
     355  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
     356    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
     357  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
     358    generalize in match (opt_safe ???); #n #l_is_n
     359    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
     360    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
     361  ]
     362|6:
     363  @All_append
     364  [ @(g_prf … vis_hd) <opt_to_opt_safe %
     365  | >H2 in visiting_prf;
     366    #H' lapply (All_append_r … H') -H' * #_ //
     367  ]
     368|8:
     369  %2 elim entry_prf
     370  [ ** >H2 cases pre
     371    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
     372      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
     373    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
     374      >lookup_add_hit >eq_gen_length %
     375    ]
     376  | #lookup_entry cut (entry ≠ vis_hd)
     377    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
     378      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
     379      normalize nodelta >lookup_entry #ABS destruct(ABS)]
     380    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
     381  ]
     382|9:
     383  >commutative_plus
     384  >add_size >(notb_true … H3) normalize nodelta
     385  whd in match (? + ?);
     386  >commutative_plus
     387  change with (? ≤ S(?) + ?)
     388  >eq_n assumption
     389|*: (* where add_gen_req does matter, expand the three possible cases *)
     390  lapply (refl … add_req_gen)
     391  whd in ⊢ (???%→?);
     392  lapply (refl … (stmt_implicit_label … statement))
     393  (* BUG *)
     394  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     395  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     396  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     397  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     398  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     399  ]
     400  *[2,4,6,8,10: #next]
     401  #EQimpl
     402  whd in ⊢ (???%→?);
     403  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
     404    whd in ⊢ (???%→?);]
     405  #EQ_req_gen >EQ_req_gen
     406  (* these are the cases, reordering them *)
     407  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
     408  [1,2,3: #i >mem_set_union
     409    [ #H elim (orb_Prop_true … H) -H
     410      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
     411    |*: >mem_set_empty whd in match (false ∨ ?);
     412    ]
     413    >mem_set_union
     414    #H elim(orb_Prop_true … H) -H
     415    [1,3,5: (* i is an explicit successor *)
     416      #i_succ
     417      (* if it's visited it's ok *)
     418      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
     419      [1,3,5: %2 %
     420      |*: %
     421        @Exists_append_l
     422        whd in match (stmt_labels ???);
     423        @Exists_append_r
     424        @mem_list_as_set
     425        @i_succ
     426      ]
     427    |2,4,6: (* i was already required *)
     428      #i_req
     429      elim (required_prf1 … i_req)
     430      [1,3,5: >H2 #H elim (Exists_append … H) -H
     431        [1,3,5: (* i in preamble → i∈visited *)
     432          #i_pre %2 >mem_set_add @orb_Prop_r
     433          lapply (All_In … H1 i_pre)
     434          #H >(notb_false … H) %
     435        |*: *
     436          [1,3,5: (* i is vis_hd *)
     437            #eq_i >eq_i %2 @mem_set_add_id
     438          |*: (* i in vis_tl → i∈visiting' *)
     439            #i_post % @Exists_append_r assumption
     440          ]
     441        ]
     442      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
     443      ]
     444    ]
     445  |4,5,6:
     446    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
     447    whd in match (? @ ?); %
     448    [1,3,5:
     449      whd
     450      >graph_to_lin_labels
     451      change with (All ?? (stmt_explicit_labels ?? statement))
     452      whd in match required';
     453      generalize in match (stmt_explicit_labels … statement);
     454      #l @list_as_set_All
     455      #i >mem_set_union >mem_set_union
     456      #i_l @orb_Prop_r @orb_Prop_l @i_l
     457    |*: @(All_mp … required_prf2)
     458      * #l_opt #s @All_mp
     459      #l #l_req >mem_set_union @orb_Prop_r
     460      >mem_set_union @orb_Prop_r @l_req
     461    ]
     462  |7,8,9:
     463    #i whd in match visited';
     464    @(eq_identifier_elim … i vis_hd)
     465    [1,3,5: #EQi >EQi #pos
     466      >lookup_add_hit #EQpos cut (gen_length = pos)
     467        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
     468        -EQpos #EQpos <EQpos -pos
     469      %
     470      [1,3,5: whd in match (rev ? ?);
     471        >rev_append_def
     472        whd
     473        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     474          <associative_append >occurs_exactly_once_None]
     475        >occurs_exactly_once_Some_eq >eq_identifier_refl
     476        normalize nodelta
     477        @generated_prf2
     478        lapply (in_map_domain … visited vis_hd)
     479        >(notb_true … H3) normalize nodelta //
     480      |*: %{statement}
     481        %
     482        [1,3,5: %
     483          [1,3,5:
     484           change with (? = Some ? (opt_safe ???))
     485           @opt_safe_elim #s //
     486          |*: whd in match (rev ? ?);
     487            >rev_append_def
     488            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     489              <associative_append @nth_opt_append_hit_l ]
     490            >nth_opt_append_r
     491            >rev_length
     492            <gen_length_prf
     493            [1,3,5: <minus_n_n] %
     494          ]
     495        |*: >EQimpl whd [3: %]
     496          >mem_set_add in next_vis;
     497          @eq_identifier_elim
     498          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
     499            >lookup_add_hit
     500          |*: #NEQ >(lookup_add_miss … visited … NEQ)
     501            whd in match (false ∨ ?);
     502            #next_vis lapply(in_map_domain … visited next) >next_vis
     503            whd in ⊢ (% → ?); [ * #s ]
     504            #EQlookup >EQlookup
     505          ] whd
     506          [1,2: %2
     507            >rev_append >nth_opt_append_r
     508            >rev_length whd in match generated';
     509            whd in match (|? :: ?|); <gen_length_prf
     510            [1,3: <minus_n_n ] %
     511          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
     512            >EQimpl %
     513          ]
     514        ]
     515      ]
     516    |*:
     517      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
     518      #Hlookup elim (generated_prf1 … Hlookup)
     519      #G1 * #s ** #G2 #G3 #G4
     520      %
     521      [1,3,5: whd in match (rev ??);
     522        >rev_append_def whd
     523        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     524          <associative_append >occurs_exactly_once_None]
     525        >occurs_exactly_once_Some_eq
     526        >eq_identifier_false
     527        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
     528        normalize nodelta
     529        assumption
     530      |*: %{s}
     531        %
     532        [1,3,5: %
     533          [1,3,5: assumption
     534          |*: whd in match (rev ??); >rev_append_def
     535            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     536              <associative_append @nth_opt_append_hit_l ]
     537            @nth_opt_append_hit_l assumption
     538          ]
     539        |*: @(opt_All_mp … G4)
     540          #x
     541          @(eq_identifier_elim … x vis_hd) #Heq
     542          [1,3,5: >Heq
     543            lapply (in_map_domain … visited vis_hd)
     544            >(notb_true … H3)
     545           normalize nodelta #EQlookup >EQlookup normalize nodelta
     546           * #nth_opt_visiting #gen_length_eq
     547           >lookup_add_hit normalize nodelta %
     548           >gen_length_eq %
     549          |*: >(lookup_add_miss ?????? Heq)
     550            lapply (in_map_domain … visited x)
     551            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
     552            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
     553            [1,3,5: #G %{G}
     554            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
     555              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     556              <associative_append @nth_opt_append_hit_l ]
     557              @nth_opt_append_hit_l assumption
     558            |*: #G elim(absurd ?? Heq)
     559              (* BUG (but useless): -required -g -generated *)
     560               >H2 in G; #G
     561              lapply (refl … (nth_opt ? 0 pre))
     562              (* BUG *)
     563              [generalize in ⊢ (???%→?);
     564              |generalize in ⊢ (???%→?);
     565              |generalize in ⊢ (???%→?);
     566              ] *
     567              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
     568                change with (Some ? vis_hd = ? → ?)
     569                #EQvis_hd' destruct(EQvis_hd') %
     570              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
     571                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
     572                >x_vis * #ABS elim (ABS I)
     573              ]
     574            ]
     575          ]
     576        ]
     577      ]
     578    ]
     579  |10,11,12:
     580    #i whd in match visited';
     581    lapply (in_map_domain … visited' i)
     582    >mem_set_add
     583    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
     584    >eq_identifier_sym >i_vis_hd
     585    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
     586    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
     587    #_ #EQlookup >lookup_add_miss in EQlookup;
     588    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
     589    #EQlookup
     590    [1,2,3: @EQlookup %]
     591    whd in match (rev ??); >rev_append_def
     592    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     593              <associative_append >does_not_occur_None]
     594    >(does_not_occur_Some ?????? (i_vis_hd))
     595    @generated_prf2 assumption
     596  |13,14,15:
     597    whd in match generated'; normalize <gen_length_prf %
     598  ]
     599]
     600qed.
     601
     602(* CSC: The branch compression (aka tunneling) optimization is not implemented
     603   in Matita *)
     604definition branch_compress
     605  ≝ λp: graph_params.λglobals.λg:codeT p globals.
     606    λentry : Σl.code_has_label … g l.g.
    177607 
    178 definition graph_translate_no_fin :
    179   ∀src_g_pars : graph_params.
    180   ext_fin_instruction src_g_pars = void →
    181   ∀dst_g_pars : graph_params.
    182   ∀globals: list ident.
    183   (* type of allocatable registers (unit if not in RTLabs) *)
    184   (* function dictating the translation *)
    185   (label → joint_instruction src_g_pars globals →
    186     list (joint_instruction dst_g_pars globals)
    187     (* this can be added to allow redirections: × label *)) →
    188   (* initialized function definition with empty graph *)
    189   joint_internal_function globals dst_g_pars →
    190   (* source function *)
    191   joint_internal_function globals src_g_pars →
    192   (* destination function *)
    193   joint_internal_function globals dst_g_pars ≝
    194   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
    195     graph_translate src_g_pars dst_g_pars globals
    196       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     608lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
     609  code_closed … (branch_compress p globals g l).
     610#p#globals#g#l#H @H qed.
     611
     612lemma branch_compress_has_entry : ∀p,globals,g,l.
     613  code_has_label … (branch_compress p globals g l) l.
     614#p#globals#g*#l#l_prf @l_prf qed.
     615
     616definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
     617  map ??
     618    (λs. let 〈l_opt,x〉 ≝ s in
     619      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
     620     
     621lemma does_not_occur_filter_labels :
     622  ∀tag,A,test,id,c.
     623    does_not_occur ?? id (filter_labels tag A test c) =
     624      (does_not_occur ?? id c ∨ ¬ test id).
     625#tag #A #test #id #c elim c
     626[ //
     627| ** [2: #lbl] #s #tl #IH
     628  whd in match (filter_labels ????); normalize nodelta
     629  whd in match (does_not_occur ????) in ⊢ (??%%);
     630  [2: @IH]
     631  normalize in match (! l ← ? ; ?); >IH
     632  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     633  elim (test lbl) normalize nodelta
     634  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     635  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
     636  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     637  ]
     638]
     639qed.
     640
     641lemma occurs_exactly_once_filter_labels :
     642  ∀tag,A,test,id,c.
     643    occurs_exactly_once ?? id (filter_labels tag A test c) =
     644      (occurs_exactly_once ?? id c ∧ test id).
     645#tag #A #test #id #c elim c
     646[ //
     647| ** [2: #lbl] #s #tl #IH
     648  whd in match (filter_labels ????); normalize nodelta
     649  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
     650  [2: @IH]
     651  normalize in match (! l ← ? ; ?); >IH
     652  >does_not_occur_filter_labels
     653  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     654  elim (test lbl) normalize nodelta
     655  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     656  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
     657  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     658  ]
     659]
     660qed.
     661
     662lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
     663  nth_opt ? n (filter_labels tag A test instrs) =
     664  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
     665  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
     666#tag #A #test #instrs elim instrs
     667[ * [2: #n'] %
     668| * #lopt #s #tl #IH * [2: #n']
     669  whd in match (filter_labels ????); normalize nodelta
     670  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
     671]
     672qed.
     673
     674definition linearize_code:
     675 ∀p : unserialized_params.∀globals.
     676  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
     677  ∀entry : (Σl. code_has_label … g l).
     678    (Σc : codeT (mk_lin_params p) globals.
     679      code_closed … c ∧
     680      ∃ sigma : identifier_map LabelTag ℕ.
     681      lookup … sigma entry = Some ? 0 ∧
     682      ∀l,n.lookup … sigma l = Some ? n →
     683        ∃s. lookup … g l = Some ? s ∧
     684          opt_Exists ?
     685            (λls.let 〈lopt, ts〉 ≝ ls in
     686              opt_All ? (eq ? l) lopt ∧
     687              ts = graph_to_lin_statement … s ∧
     688              opt_All ?
     689                (λnext.Or (lookup … sigma next = Some ? (S n))
     690                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     691                (stmt_implicit_label … s)) (nth_opt … n c))
     692
     693 λp,globals,g,g_prf,entry_sig.
     694    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
     695    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
     696    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
     697    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
     698      (entry_sig) g_prf ????????
     699    with
     700    [ mk_Sig triple H ⇒
     701      let sigma ≝ \fst (\fst triple) in
     702      let required ≝ \snd (\fst triple) in
     703      let crev ≝ \snd triple in
     704      let lbld_code ≝ rev ? crev in
     705      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
     706[ (* done later *)
     707| #i >mem_set_empty *
     708| %
     709|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
     710| #l #_ %
     711| % [2: %] @(pi2 … entry_sig')
     712| %
     713| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
     714| >commutative_plus change with (? ≤ |g|) %
     715]
     716lapply (refl … triple)
     717generalize in match triple in ⊢ (???%→%); **
     718#visited #required #generated #EQtriple
     719>EQtriple in H ⊢ %; normalize nodelta ***
     720#entry_O #req_vis #labels_in_req #sigma_prop
     721% >EQtriple
     722[ (* code closed *)
     723  @All_map
     724  [2: @All_rev
     725    @(All_mp … labels_in_req) #ls #H @H
     726  |1: (* side-effect close *)
     727  |3: * #lopt #s @All_mp
     728    #lbl #lbl_req whd in match (code_has_label ????);
     729    >occurs_exactly_once_filter_labels
     730    @andb_Prop [2: assumption]
     731    lapply (in_map_domain … visited lbl)
     732    >(req_vis … lbl_req) * #n #eq_lookup
     733    elim (sigma_prop ?? eq_lookup) #H #_ @H
     734  ]
     735]
     736%{visited} % [assumption]
     737#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
     738#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     739% [2: % [ assumption ] |]
     740>nth_opt_filter_labels in ⊢ (???%);
     741>nth_opt_is_stmt
     742whd in match (! 〈lopt, s〉 ← Some ??; ?);
     743whd
     744whd in match (! lbl0 ← Some ??; ?);
     745% [ % [ elim (lbl ∈ required) ] % ]
     746whd
     747lapply (refl … (stmt_implicit_label … stmt))
     748generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
     749#eq_impl_lbl normalize nodelta [2: %]
     750>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
     751[ %{H}
     752| %2 >nth_opt_filter_labels >H
     753  whd in match (! 〈lopt, s〉 ← ?; ?);
     754  whd in match (! lbl0 ← ?; ?);
     755  %
     756]
     757qed.
     758
     759definition graph_linearize :
     760  ∀p : unserialized_params.
     761  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
     762    Σfout : joint_closed_internal_function globals (mk_lin_params p).
     763      ∃sigma : identifier_map LabelTag ℕ.
     764        let g ≝ joint_if_code ?? (pi1 … fin) in
     765        let c ≝ joint_if_code ?? (pi1 … fout) in
     766        let entry ≝ joint_if_entry ?? (pi1 … fin) in
     767         lookup … sigma entry = Some ? 0 ∧
     768          ∀l,n.lookup … sigma l = Some ? n →
     769            ∃s. lookup … g l = Some ? s ∧
     770              opt_Exists ?
     771                (λls.let 〈lopt, ts〉 ≝ ls in
     772                  opt_All ? (eq ? l) lopt ∧
     773                  ts = graph_to_lin_statement … s ∧
     774                  opt_All ?
     775                    (λnext.Or (lookup … sigma next = Some ? (S n))
     776                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     777                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
     778  λp,globals,f_sig.
     779  mk_Sig ?? (match f_sig with
     780  [ mk_Sig f f_prf ⇒ 
     781  mk_joint_internal_function globals (mk_lin_params p)
     782   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
     783   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
     784   (joint_if_stacksize ?? f)
     785   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
     786   (mk_Sig ?? it I) (mk_Sig ?? it I)
     787  ]) ?.
     788elim f_sig
     789normalize nodelta #f_in #f_in_prf
     790elim (linearize_code ?????)
     791#f_out * #f_out_closed #H assumption
     792qed.
     793
    197794 
    198795
  • src/joint/semanticsUtils_paolo.ma

    r1641 r1882  
    2121(******************************** GRAPHS **************************************)
    2222
    23 definition graph_pointer_of_label0:
    24  pointer → label → Σp:pointer. ptype p = Code ≝
    25  λoldpc,l.
    26   mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    28 // qed.
    29 
    30 definition graph_pointer_of_label :
    31   ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
    32     res (Σp:pointer. ptype p = Code) ≝
    33  λ_.λ_.λ_.λoldpc,l.
    34   OK ? (graph_pointer_of_label0 oldpc l).
     23definition graph_pointer_of_label : cpointer → label → res cpointer ≝
     24  λoldpc,l.
     25  return (mk_pointer Code
     26   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer).
     27% qed.
    3528
    3629definition graph_label_of_pointer: pointer → res label ≝
    3730 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    38 
    39 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    40  But I can't use it directly because this one uses a concrete definition of
    41  pointer_of_label and it is used to istantiate the more_sem_params record
    42  where the abstract version is declared as a field. Is there a better way
    43  to organize the code? *)
    44 definition graph_succ_p: label → address → res address ≝
    45  λl,old.
    46   do ptr ← pointer_of_address old ;
    47   let newptr ≝ graph_pointer_of_label0 ptr l in
    48   address_of_pointer newptr.
    4931
    5032definition graph_fetch_statement:
     
    5335 ∀globals.
    5436  genv globals pars →
    55   state sem_pars
     37  cpointer
    5638  res (joint_statement pars globals) ≝
    57  λpars,sem_pars,globals,ge,st.
    58   do p ← code_pointer_of_address (pc … st) ;
     39 λpars,sem_pars,globals,ge,p.
    5940  do f ← fetch_function … ge p ;
    6041  do l ← graph_label_of_pointer p;
     
    7152      pars
    7253      g_pars
    73       graph_succ_p
    74       (graph_pointer_of_label ?)
    75       (graph_fetch_statement ? ?)
     54      graph_pointer_of_label
     55      (λ_.λ_.graph_pointer_of_label)
     56      (graph_fetch_statement ? g_pars)
    7657    ).
    7758   
    7859(******************************** LINEAR **************************************)
    79 
    80 definition lin_succ_p: unit → address → res address :=
    81  λ_.λaddr. addr_add addr 1.
    82 
     60check mk_pointer
     61definition lin_succ_p: cpointer → unit → res cpointer :=
     62 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
     63[%| cases ptr //] qed.
    8364
    8465axiom BadLabel: String.
     
    8667definition lin_pointer_of_label:
    8768 ∀pars : lin_params.
    88  ∀globals. genv globals pars → pointer → label →
    89   res (Σp:pointer. ptype p = Code) ≝
     69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝
    9070 λpars,globals,ge,old,l.
    9171  do fn ← fetch_function … ge old ;
     
    9777     (joint_if_code … pars fn)) ;
    9878  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    99 // qed.
     79% qed.
    10080
    10181definition lin_fetch_statement:
     
    10383 ∀sem_pars : sem_state_params.
    10484 ∀globals.
    105  genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
    106  λpars,sem_pars,globals,ge,st.
    107   do ppc ← pointer_of_address (pc … st) ;
     85 genv globals pars → cpointer → res (joint_statement pars globals) ≝
     86 λpars,sem_pars,globals,ge,ppc.
    10887  do fn ← fetch_function … ge ppc ;
    10988  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
     
    123102      lin_succ_p
    124103      (lin_pointer_of_label ?)
    125       (lin_fetch_statement ? ?)
     104      (lin_fetch_statement ? g_pars)
    126105    ).
    127106   
    128 
     107definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
     108  λp,globals,stp.match stp with
     109  [ COND _ _ ⇒ false
     110  | CALL_ID _ _ _ ⇒ false
     111  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
     112    match ext_step_labels … c' with
     113    [ nil ⇒ true
     114    | _ ⇒ false
     115    ]
     116  | _ ⇒ true
     117  ].
     118
     119definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
     120  λp,globals,stp.match stp with
     121  [ sequential _ _ ⇒ false
     122  | _ ⇒ true
     123  ].
     124
     125inductive s_block (p : params) (globals : list ident) : Type[0] ≝
     126  | Skip : s_block p globals
     127  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
     128  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
     129  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.
     130
     131include "utilities/bind_new.ma".
     132
     133definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
     134
     135definition Bcons ≝ λp : params.λglobals.
     136    λs : Σs.bool_to_Prop (step_unbranching p globals s).
     137    λB : Block p globals.
     138    ! b ← B ; return Cons ?? s b.
     139
     140interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
     141
     142let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
     143  match b1 with
     144  [ Skip ⇒ true
     145  | FinStep _ ⇒ false
     146  | FinStmt _ ⇒ false
     147  | Cons _ tl ⇒ is_unbranching ?? tl
     148  ].
     149
     150let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
     151  match b1 with
     152  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
     153  | bnew f ⇒ ∀x.Is_unbranching … (f x)
     154  ].
     155
     156let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
     157  match b1 return λx.is_unbranching ?? x → ? with
     158  [ Skip ⇒ λ_.b2
     159  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
     160  | _ ⇒ Ⓧ
     161  ].
     162
     163definition s_block_append ≝
     164  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
     165  match b1 with
     166  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].
     167
     168definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
     169  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
     170  λp,globals. ?.
     171* #b elim b -b
     172[ #b #H @bret @b @H
     173| #f #IH #H @bnew #x @(IH x) @H
     174]
     175qed.
     176
     177lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
     178#p #globals * #b elim b
     179[ //
     180| #f #IH #H @bnew_proper
     181  #x @IH
     182]
     183qed.
     184 
     185definition Block_append ≝
     186  λp,globals.λB : Σb.Is_unbranching … b.λB'.
     187  ! b1 ← Is_to_is_unbr … B;
     188  ! b2 ← B';
     189  return s_block_append p globals b1 b2.
     190
     191definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
     192
     193let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
     194    s_block p globals ≝
     195  match l  with
     196  [ nil ⇒ Skip ??
     197  | cons hd tl ⇒
     198    If step_unbranching … hd then with prf do
     199      Cons ?? hd (step_list_to_s_block ?? tl)
     200    else with prf do
     201      FinStep ?? hd
     202  ]. [assumption | >prf % ] qed.
     203 
     204definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
     205  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).
     206
     207record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
     208  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
     209  ; genv_rel : genv globals p1 → genv globals p2 → Prop
     210  ; pc_rel : cpointer → cpointer → Prop
     211  ; st_rel : state p1 → state p2 → Prop
     212  ; stmt_rel : joint_statement p1 globals → Block
     213  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
     214  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
     215  }.
     216 
     217(* move *)
     218definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
     219 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
     220  match pty return λpty. ? → pty = XData → ? with
     221   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
     222   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
     223[@(pi2 … p) |6: // |7: %] destruct (abs)
     224qed.
     225
     226definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
     227cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     228lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     229%{«mk_pointer ? (mk_block ? z) H o,I»}
     230% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
     231qed.
     232
     233definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
     234  λp1,p2,R,st1,st2.
     235    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
     236    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
     237    sp_rel p1 p2 R
     238      (safe_address_of_xdata_pointer (sp … st1))
     239      (safe_address_of_xdata_pointer (sp … st2)) ∧
     240    isp_rel p1 p2 R
     241      (safe_address_of_xdata_pointer (isp … st1))
     242      (safe_address_of_xdata_pointer (isp … st2)) ∧
     243    sp_rel p1 p2 R
     244      (safe_address_of_xdata_pointer (sp … st1))
     245      (safe_address_of_xdata_pointer (sp … st2)) ∧
     246    carry … st1 = carry … st2 ∧
     247    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
     248    mem_rel p1 p2 R (m … st1) (m … st2).
     249elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
     250elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
     251assumption
     252qed.
     253 elim st2
     254-st1 -st2 #st2 ** #good_pc2 # ∧
     255    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     256    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     257    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     258
     259
     260
  • src/joint/semantics_paolo.ma

    r1709 r1882  
    1212
    1313definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
     14definition cpointer ≝ Σp.ptype p = Code.
     15definition xpointer ≝ Σp.ptype p = XData.
     16unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     17unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
    1418
    1519record sem_state_params : Type[1] ≝
     
    1721 ; empty_framesT: framesT
    1822 ; regsT : Type[0]
    19  ; empty_regsT: address → regsT (* Stack pointer *)
     23 ; empty_regsT: xpointer → regsT (* Stack pointer *)
    2024 }.
    2125 
    2226record state (semp: sem_state_params): Type[0] ≝
    2327 { st_frms: framesT semp
    24  ; pc: address
    25  ; sp: pointer
    26  ; isp: pointer
     28 ; sp: xpointer
     29 ; isp: xpointer
    2730 ; carry: beval
    2831 ; regs: regsT semp
    2932 ; m: bemem
    3033 }.
    31  
     34
     35record state_pc (semp : sem_state_params) : Type[0] ≝
     36  { st_no_pc :> state semp
     37  ; pc : cpointer
     38  }.
     39
    3240definition set_m: ∀p. bemem → state p → state p ≝
    33  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    3442
    3543definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    36  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    37 
    38 definition set_sp: ∀p. pointer → state p → state p ≝
    39  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    40 
    41 definition set_isp: ∀p. pointer → state p → state p ≝
    42  λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     45
     46definition set_sp: ∀p. ? → state p → state p ≝
     47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     48
     49definition set_isp: ∀p. ? → state p → state p ≝
     50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    4351
    4452definition set_carry: ∀p. beval → state p → state p ≝
    45  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    46 
    47 definition set_pc: ∀p. address → state p → state p ≝
    48  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     54
     55definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     57
     58definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     59 λp,s,st. mk_state_pc … s (pc … st).
    4960
    5061definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    51  λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    5263
    5364axiom BadProgramCounter : String.
     
    5768 ∀globals.
    5869  genv globals pars →
    59   pointer →
     70  cpointer →
    6071  res (joint_internal_function … pars) ≝
    6172 λpars,globals,ge,p.
     
    6576  [ Internal def' ⇒ OK … def'
    6677  | External _ ⇒ Error … [MSG BadProgramCounter]].
    67  
     78
     79inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
     80  | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
     81  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
     82  | Proceed  : step_flow p globals. (* go to implicit successor *)
     83
     84inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
     85  | SRedirect : label → stmt_flow p globals
     86  | SProceed : succ p → stmt_flow p globals
     87  | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
     88  | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
     89  | SEnd  : stmt_flow p globals. (* end flow *)
     90
     91
    6892record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    6993  { st_pars :> sem_state_params
     
    82106  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    83107  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    84   ; fetch_ra: state st_pars →
    85       res ((state st_pars) × address)
    86 
    87   ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
     108  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     109
     110  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    88111  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    89   ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
     112  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
    90113   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    91114     type of arguments. To be fixed using a dependent type *)
     
    94117  ; fetch_external_args: external_function → state st_pars →
    95118      res (list val)
    96   ; set_result: list val → state st_pars →
    97       res (state st_pars)
     119  ; set_result: list val → state st_pars → res (state st_pars)
    98120  ; call_args_for_main: call_args uns_pars
    99121  ; call_dest_for_main: call_dest uns_pars
     
    111133  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
    112134  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
    113   λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
     135  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
    114136
    115137definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     
    126148definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
    127149definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    128 definition pair_reg_move : ?→?→?→?→res ?
     150definition pair_reg_move : ?→?→?→?→?
    129151  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
    130152    ! r ← pair_reg_move_ ? p (regs ? st) pm;
    131     return (set_regs ? r st).
    132 
     153    return set_regs ? r st.
     154
     155 
    133156axiom BadPointer : String.
    134 
     157 
    135158(* this is preamble to all calls (including tail ones). The optional argument in
    136159   input tells the function whether it has to save the frame for internal
    137160   calls.
    138    the first element of the triple is the label at the start of the function
    139    in case of an internal call, or None in case of an external one.
     161   the first element of the triple is the entry point of the function if
     162   it is an internal one, or false in case of an external one.
    140163   The actual update of the pc is left to later, as it depends on
    141164   serialization and on whether the call is a tail one. *)
    142 definition eval_call_block_preamble:
     165definition eval_call_block:
    143166 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    144   genv globals p → state p' → block → call_args p → option ((call_dest p) × address)
    145     IO io_out io_in ((option label)×trace×(state p')) ≝
    146  λglobals,p,p',ge,st,b,args,dest_ra.
     167  genv globals p → state p' → block → call_args p → call_dest p
     168    IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
     169 λglobals,p,p',ge,st,b,args,dest.
    147170  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    148171    match fd with
    149172    [ Internal fn ⇒
    150       let st ≝ match dest_ra with
    151         [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
    152         | None ⇒ st
    153         ] in
    154       ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    155               args st ;
    156       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    157       let l' ≝ joint_if_entry … fn in
    158       let st ≝ set_regs p' regs st in
    159       return 〈Some label l', E0, st〉
     173      return 〈Init … (block_id b) fn args dest, E0, st〉
    160174    | External fn ⇒
    161175      ! params ← fetch_external_args … p' fn st : IO ???;
     
    167181      let vs ≝ [mk_val ? evres] in
    168182      ! st ← set_result … p' vs st : IO ???;
    169       return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     183      return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    170184      ].
    171185
    172186axiom FailedStore: String.
    173187
    174 definition push: ∀p. state p → beval → res (state p) ≝
     188definition push: ∀p.state p → beval → res (state p) ≝
    175189 λp,st,v.
    176   let isp ≝ isp … st in
    177   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    178   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    179   OK … (set_m … m (set_isp … isp st)).
    180 
    181 definition pop: ∀p. state p → res (state p × beval) ≝
     190  let isp' ≝ isp ? st in
     191  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
     192  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
     193  return set_m … m (set_isp … isp'' st).
     194  normalize elim (isp p st) //
     195qed.
     196
     197definition pop: ∀p. state p → res ((state p ) × beval) ≝
    182198 λp,st.
    183   let isp ≝ isp ? st in
    184   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    185   let ist ≝ set_isp … isp st in
    186   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    187   OK ? 〈st,v〉.
    188 
    189 definition save_ra : ∀p. state p → address → res (state p) ≝
     199  let isp' ≝ isp ? st in
     200  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
     201  let ist ≝ set_isp … isp'' st in
     202  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
     203  OK ? 〈ist,v〉.
     204  normalize elim (isp p st) //
     205qed.
     206 
     207definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    190208 λp,st,l.
    191   let 〈addrl,addrh〉 ≝ l in
    192   do st ← push … st addrl;
    193   push … st addrh.
    194 
    195 definition load_ra : ∀p.state p → res (state p × address) ≝
     209  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
     210  ! st' ← push … st addrl;
     211  push … st' addrh.
     212
     213definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
    196214 λp,st.
    197   do 〈st,addrh〉 ← pop … st;
    198   do 〈st,addrl〉 ← pop … st;
    199   OK ? 〈st, 〈addrl,addrh〉〉.
    200 
     215  do 〈st',addrh〉 ← pop … st;
     216  do 〈st'',addrl〉 ← pop … st';
     217  do pr ← code_pointer_of_address 〈addrh, addrl〉;
     218  return 〈st'', pr〉.
     219
     220definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
     221  match flow with
     222  [ SProceed _ ⇒ False
     223  | SInit _ _ _ _ _ ⇒ False
     224  | _ ⇒ True
     225  ].
    201226
    202227(* parameters that need full params to have type of functions,
    203    but are still independent of serialization
    204    Paolo: the first element returned by exec extended is None if flow is
    205    left to regular sequential one, otherwise a label.
    206    The address input is the address of the next statement, to be provided to
    207    accomodate extensions that make calls. *)
     228   but are still independent of serialization *)
    208229record more_sem_genv_params (pp : params) : Type[1] ≝
    209230  { msu_pars :> more_sem_unserialized_params pp
    210231  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    211   ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
    212       state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
    213   ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
    214       state msu_pars → IO io_out io_in (trace × (state msu_pars))
     232  (* change of pc must be left to *_flow execution *)
     233  ; exec_extended: ∀globals.genv globals pp → ext_step pp →
     234      state msu_pars →
     235      IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
     236  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
     237      state msu_pars →
     238      IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
    215239  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    216240  }.
    217  
    218241
    219242(* parameters that are defined by serialization *)
    220243record more_sem_params (pp : params) : Type[1] ≝
    221244  { msg_pars :> more_sem_genv_params pp
    222   ; succ_pc: succ pp → address → res address
    223   ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
    224   ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
     245  ; offset_of_point : code_point pp → offset
     246  ; point_of_offset : offset → option (code_point pp)
     247  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
     248  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
    225249  }.
     250
     251definition pointer_of_point : ∀p.more_sem_params p →
     252  cpointer→ code_point p → cpointer ≝
     253  λp,msp,ptr,pt.
     254    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
     255[ elim ptr #ptr' #EQ <EQ @pok
     256| %] qed.
     257
     258axiom BadOffsetForCodePoint : String.
     259
     260definition point_of_pointer :
     261  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
     262  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
     263    (point_of_offset p msp (poff ptr)).
     264
     265lemma point_of_pointer_of_point :
     266  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
     267#p #msp #ptr #pt normalize
     268>point_of_offset_of_point %
     269qed.
     270
     271lemma pointer_of_point_block :
     272  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
     273/ by refl/
     274qed.
     275
     276lemma pointer_of_point_uses_block :
     277  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
     278#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     279        ** #ty2 #bl2 #H2 #o2 #EQ2
     280#pt #EQ3 destruct normalize //
     281qed.
     282
     283lemma pointer_of_point_of_pointer :
     284  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     285    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
     286    pointer_of_point p msp ptr2 pt = ptr1.
     287#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     288        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
     289destruct
     290lapply (offset_of_point_of_offset p msp o1)
     291normalize
     292elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
     293#pt' #EQ #EQ' destruct %
     294qed.
     295
     296
     297axiom ProgramCounterOutOfCode : String.
     298axiom PointNotFound : String.
     299axiom LabelNotFound : String.
     300
     301definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     302  genv globals p → cpointer → res (joint_statement p globals) ≝
     303  λp,msp,globals,ge,ptr.
     304  ! pt ← point_of_pointer ? msp ptr ;
     305  ! fn ← fetch_function … ge ptr ;
     306  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     307
     308definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     309  genv globals p → cpointer → label → res cpointer ≝
     310  λp,msp,globals,ge,ptr,lbl.
     311  ! fn ← fetch_function … ge ptr ;
     312  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     313            (point_of_label … (joint_if_code … fn) lbl) ;
     314  return pointer_of_point ? msp ptr pt.
     315
     316definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     317  cpointer → succ p → res cpointer ≝
     318  λp,msp,ptr,nxt.
     319  ! curr ← point_of_pointer p msp ptr ;
     320  return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
    226321
    227322record sem_params : Type[1] ≝
     
    230325  }.
    231326
    232 definition address_of_label: ∀globals. ∀p:sem_params.
     327(* definition address_of_label: ∀globals. ∀p:sem_params.
    233328  genv globals p → pointer → label → res address ≝
    234329 λglobals,p,ge,ptr,l.
    235330  do newptr ← pointer_of_label … p ? ge … ptr l ;
    236   OK … (address_of_code_pointer newptr).
     331  OK … (address_of_code_pointer newptr). *)
    237332
    238333definition goto: ∀globals. ∀p:sem_params.
    239   genv globals p → label → state p → res (state p) ≝
     334  genv globals p → label → state_pc p → res (state_pc p) ≝
    240335 λglobals,p,ge,l,st.
    241   ! oldpc ← pointer_of_address (pc … st);
    242   ! newpc ← address_of_label … ge oldpc l ;
    243   OK (state p) (set_pc … newpc st).
     336  ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
     337  return set_pc … newpc st.
    244338
    245339(*
     
    248342*)
    249343
    250 definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
     344definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
    251345 λp,l,st.
    252   ! l' ← succ_pc … p l (pc … st) ;
    253   OK … (set_pc … l' st).
     346 ! nw ← succ_pc ? p … (pc ? st) l ;
     347 return set_pc … nw st.
    254348
    255349axiom MissingSymbol : String.
    256350axiom FailedLoad : String.
    257351axiom BadFunction : String.
    258 
    259 definition eval_call_block:
     352axiom SuccessorNotProvided : String.
     353
     354(* the optional point must be given only for calls *)
     355definition eval_step :
    260356 ∀globals.∀p:sem_params. genv globals p → state p →
    261   block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    262  λglobals,p,ge,st,b,args,dest,ra.
    263  ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
    264  ! new_pc ← match next with
    265   [ Some lbl ⇒
    266     let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    267     address_of_label globals p ge pointer_in_fn lbl
    268   | None ⇒ return ra
    269   ] ;
    270  let st ≝ set_pc … new_pc st in
    271  return 〈tr, st〉.
    272 % qed.
    273 
    274 definition eval_call_id:
    275  ∀globals.∀p:sem_params. genv globals p → state p →
    276   ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    277  λglobals,p,ge,st,id,args,dest,ra.
    278   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
    279   eval_call_block … ge st b args dest ra.
    280 
    281 
    282 (* defining because otherwise typechecker stalls *)
    283 definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
    284   ∀i : ident.member i (eq_identifier SymbolTag) globals
    285      →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
    286      λglobals,p,ge,st,ident,prf,ldest,hdest,l.
    287      let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
    288      ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
    289      ! st ← dpl_store … ldest laddr st;
    290      ! st ← dph_store … hdest haddr st;
    291      ! st ← next … p l st ;
    292      return 〈E0, st〉.
    293   [ cases addr //
    294   | (* TODO: to prove *)
    295     elim daemon
    296   ] qed.
    297 
    298 (* defining because otherwise typechecker stalls *)
    299 definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
    300   acc_a_reg p → succ p → res (trace × (state p)) ≝
    301   λglobals,p,ge,st,dst,l.
    302         ! 〈st,v〉 ← pop p st;
    303         ! st ← acca_store p p dst v st;
    304         ! st ← next p l st ;
    305         return 〈E0, st〉.
    306 
    307 (* defining because otherwise typechecker stalls *)
    308 definition eval_sequential :
    309  ∀globals.∀p:sem_params. genv globals p → state p →
    310   joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
    311  λglobals,p,ge,st,seq,l.
     357  joint_step p globals →
     358  IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
     359 λglobals,p,ge,st,seq.
    312360  match seq with
    313361  [ extension c ⇒
    314     ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
    315     ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
    316     ! st ← match next_pc with
    317       [ None ⇒ next … p l st
    318       | Some lbl ⇒ goto … ge lbl st
    319       ] ;
    320     return 〈tr, st〉
     362    exec_extended … ge c st
    321363  | COST_LABEL cl ⇒
    322     ! st ← next … p l st ;
    323     return 〈Echarge cl, st〉
     364    return 〈Proceed ??, Echarge cl, st〉
    324365  | COMMENT c ⇒
    325     ! st ← next … p l st ;
    326     return 〈E0, st〉
     366    return 〈Proceed ??, E0, st〉
    327367  | LOAD dst addrl addrh ⇒
    328368    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    331371    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    332372    ! st ← acca_store p … dst v st ;
    333     ! st ← next … p l st ;
    334     return 〈E0, st〉
     373    return 〈Proceed ??, E0, st〉
    335374  | STORE addrl addrh src ⇒
    336375    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    339378    ! v ← acca_arg_retrieve … st src;
    340379    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    341     let st ≝ set_m … m' st in
    342     ! st ← next … p l st ;
    343     return 〈E0, st〉
     380    return 〈Proceed ??, E0, set_m … m' st〉
    344381  | COND src ltrue ⇒
    345382    ! v ← acca_retrieve … st src;
    346383    ! b ← bool_of_beval v;
    347384    if b then
    348      ! st ← goto … p ge ltrue st ;
    349      return 〈E0, st〉
     385      return 〈Redirect ?? ltrue, E0, st〉
    350386    else
    351      ! st ← next … p l st ;
    352      return 〈E0, st〉
     387      return 〈Proceed ??, E0, st〉
    353388  | ADDRESS ident prf ldest hdest ⇒
    354     eval_address … ge st ident prf ldest hdest l
     389    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     390    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
     391    ! st' ← dpl_store … ldest laddr st;
     392    ! st'' ← dph_store … hdest haddr st';
     393    return 〈Proceed ??, E0, st''〉
    355394  | OP1 op dacc_a sacc_a ⇒
    356395    ! v ← acca_retrieve … st sacc_a;
     
    358397    let v' ≝ BVByte (op1 eval op v) in
    359398    ! st ← acca_store … dacc_a v' st;
    360     ! st ← next … l st ;
    361     return 〈E0, st〉
     399    return 〈Proceed ??, E0, st〉
    362400  | OP2 op dacc_a sacc_a src ⇒
    363401    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    369407      let v' ≝ BVByte v' in
    370408      let carry ≝ beval_of_bool carry in
    371     ! st ← acca_store … dacc_a v' st;
    372       let st ≝ set_carry … carry st in
    373     ! st ← next … l st ;
    374     return 〈E0, st〉
     409    ! st' ← acca_store … dacc_a v' st;
     410      let st'' ≝ set_carry … carry st' in
     411    return 〈Proceed ??, E0, st''〉
    375412  | CLEAR_CARRY ⇒
    376     ! st ← next … l (set_carry … BVfalse st) ;
    377     return 〈E0, st
     413    let st' ≝ set_carry … BVfalse st in
     414    return 〈Proceed ??, E0, st'
    378415  | SET_CARRY ⇒
    379     ! st ← next … l (set_carry … BVtrue st) ;
    380     return 〈E0, st
     416    let st' ≝ set_carry … BVtrue st in
     417    return 〈Proceed ??, E0, st'
    381418  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    382419    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    387424    let v1' ≝ BVByte v1' in
    388425    let v2' ≝ BVByte v2' in
    389     ! st ← acca_store … dacc_a_reg v1' st;
    390     ! st ← accb_store … dacc_b_reg v2' st;
    391     ! st ← next … l st ;
    392     return 〈E0, st〉
     426    ! st' ← acca_store … dacc_a_reg v1' st;
     427    ! st'' ← accb_store … dacc_b_reg v2' st';
     428    return 〈Proceed ??, E0, st''〉
    393429  | POP dst ⇒
    394     eval_pop … ge st dst l
     430    ! 〈st',v〉 ← pop p st;
     431    ! st'' ← acca_store p p dst v st';
     432    return 〈Proceed ??, E0, st''〉
    395433  | PUSH src ⇒
    396434    ! v ← acca_arg_retrieve … st src;
    397435    ! st ← push … st v;
    398     ! st ← next … l st ;
    399     return 〈E0, st〉
     436    return 〈Proceed ??, E0, st〉
    400437  | MOVE dst_src ⇒
    401438    ! st ← pair_reg_move … st dst_src ;
    402     ! st ← next … l st ;
    403     return 〈E0, st〉
     439    return 〈Proceed ??, E0, st〉
    404440  | CALL_ID id args dest ⇒
    405     ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    406     eval_call_id … ge st id args dest ra
     441    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     442    eval_call_block … ge st b args dest
    407443  ].
     444  [ cases addr //
     445  | (* TODO: to prove *)
     446    elim daemon
     447  ] qed.
     448
     449definition eval_step_flow :
     450 ∀globals.∀p:sem_params.step_flow p globals →
     451  succ p → stmt_flow p globals ≝
     452 λglobals,p,cmd,nxt.
     453 match cmd with
     454 [ Redirect l ⇒ SRedirect … l
     455 | Init id fn args dest ⇒ SInit … id fn args dest nxt
     456 | Proceed ⇒ SProceed … nxt
     457 ].
    408458
    409459definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
    410   state p → IO io_out io_in (trace × (state p)) ≝
    411  λglobals,p,ge,st.
    412   ! s ← fetch_statement … ge st : IO ???;
    413   match s return λ_.IO io_out io_in (trace × (state p)) with
    414     [ GOTO l ⇒
    415        ! st ← goto … ge l st ;
    416        return 〈E0, st〉
    417     | RETURN ⇒
     460  state p → joint_statement … p globals →
     461  IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
     462 λglobals,p,ge,st,s.
     463  match s with
     464    [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
     465    | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
     466    | sequential seq l ⇒
     467      ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
     468      return 〈eval_step_flow … flow l, tr, st〉
     469    | extension_fin c ⇒
     470      ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
     471      return 〈pi1 … flow, tr, st〉
     472    ].
     473
     474definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     475  state p → (Σs : joint_statement … p globals.no_seq … s) →
     476  IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
     477 λglobals,p,ge,st,s_sig.
     478  match s_sig with
     479  [ mk_Sig s s_prf ⇒
     480    match s return λx.no_seq p globals x → ? with
     481    [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
     482    | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
     483    | sequential seq l ⇒ Ⓧ
     484    | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
     485    ] s_prf
     486  ]. % qed.
     487
     488let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
     489  (v2 : IO O I B) on v1 : Prop ≝
     490  match v1 with
     491  [ Value x ⇒
     492    match v2 with
     493    [ Value y ⇒
     494      P x y
     495    | _ ⇒ False
     496    ]
     497  | Wrong _ ⇒
     498    match v2 with
     499    [ Wrong _ ⇒ True
     500    | _ ⇒ False
     501    ]
     502  | Interact o1 f1 ⇒
     503    match v2 with
     504    [ Interact o2 f2 ⇒
     505      ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
     506    | _ ⇒ False
     507    ]
     508  ]. <prf @i qed.
     509
     510definition IORel ≝ λO,I.
     511  mk_MonadRel (IOMonad O I) (IOMonad O I)
     512    (rel_io O I) ???.
     513[//
     514|#X #Y #Z #W #relin #relout #m elim m
     515  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
     516    #f1 #f2 #G' whd %{(refl …)} #i
     517    @(IH … (G i) f1 f2 G')
     518  | #v * [#o #f * | #v' | #e *]
     519    #Pvv' #f #g #H normalize @H @Pvv'
     520  | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
     521  ]
     522| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
     523  [1,4,7: #o' #f' [2,3: *]
     524    normalize * #prf destruct(prf) normalize #G
     525    % [%] normalize #i @IH @G
     526  |2,5,8: #v' [1,3: *]
     527    @H
     528  |*: #e' [1,2: *] //
     529  ]
     530]
     531qed.
     532
     533lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
     534  reflexive ? (m_rel ?? (IORel O I) ?? rel).
     535#O #I #X #rel #H #m elim m
     536[ #o #f #IH whd %[%] #i normalize @IH
     537| #v @H
     538| #e %
     539]
     540qed.
     541
     542lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
     543  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
     544  ∀m,n,o.
     545  m_rel ?? (IORel O I) … rel1 m n →
     546  m_rel ?? (IORel O I) … rel2 n o →
     547  m_rel ?? (IORel O I) … rel3 m o.
     548#O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
     549[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
     550  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
     551| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
     552  @H
     553| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
     554]
     555qed.
     556
     557lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
     558  ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
     559  ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
     560                  m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
     561#M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
     562@(mr_bind … H) @G qed.
     563
     564lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
     565  m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
     566#M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
     567qed.
     568
     569lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
     570  pi1 ?? s1 = s2 →
     571  m_rel ?? (IORel ??) ??
     572    (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
     573      \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
     574    (eval_statement_no_seq globals p ge st s1)
     575    (eval_statement globals p ge st s2).
     576#globals #p #ge #st * * [#s #n | #lbl || #c ]*
     577#s2 #EQ destruct(EQ)
     578whd in match eval_statement;
     579whd in match eval_statement_no_seq;
     580normalize nodelta
     581[1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
     582<(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
     583@(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
     584#x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
     585qed.
     586
     587definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     588  state p → Z → joint_internal_function globals p → call_args p →
     589  res (state_pc p) ≝
     590  λglobals,p,ge,st,id,fn,args.
     591    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     592              args st ;
     593    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
     594    let l' ≝ joint_if_entry … fn in
     595    let st' ≝ set_regs p regs st in
     596    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
     597    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     598    return mk_state_pc ? st' pc. % qed.
     599
     600definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
     601  state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
     602  λglobals,p,ge,st,flow.
     603  match flow with
     604  [ SRedirect l ⇒ goto … ge l st
     605  | SProceed nxt ⇒ next ? nxt st
     606  | SInit id fn args dest nxt ⇒
     607    ! ra ← succ_pc ? p … (pc … st) nxt ;
     608    let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
     609    do_call ?? ge st' id fn args
     610  | STailInit id fn args ⇒
     611    do_call … ge st id fn args
     612  | SEnd ⇒
     613    ! 〈st,ra〉 ← fetch_ra … st ;
     614    ! st' ← pop_frame … ge st;
     615    return mk_state_pc ? st' ra
     616  ].
     617
     618definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     619  state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
     620    IO io_out io_in (state_pc p) ≝
     621  λglobals,p,ge,st,id,flow_sig.
     622  match flow_sig with
     623  [ mk_Sig flow prf ⇒
     624    match flow return λx.flow_no_seq p globals x → ? with
     625    [ SRedirect l ⇒ λ_.
     626      ! newpc ← pointer_of_label ? p … ge
     627        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
     628      return mk_state_pc … st newpc
     629    | STailInit id fn args ⇒ λ_.
     630      do_call … ge st id fn args
     631    | SEnd ⇒ λ_.
    418632      ! 〈st,ra〉 ← fetch_ra … st ;
    419       ! st ← pop_frame … ge st;
    420       return 〈E0,set_pc … ra st〉
    421    | sequential seq l ⇒ eval_sequential … ge st seq l
    422    | extension_fin c ⇒ exec_fin_extended … ge c st
    423    ].
     633      ! st' ← pop_frame … ge st;
     634      return mk_state_pc ? st' ra
     635    | _ ⇒ Ⓧ
     636    ] prf
     637  ]. % qed.
     638
     639lemma pointer_of_label_eq_with_id :
     640∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
     641  block_id (pblock ptr1) = block_id (pblock ptr2) →
     642  pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
     643#g #p #ge
     644** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
     645** #ty2 * #r2 #id2 #H2 inversion H2
     646[1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
     647qed.
     648
     649
     650lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
     651  ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
     652  pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
     653    (eval_stmt_flow_no_seq g p ge st id s1) =
     654    (eval_stmt_flow g p ge st s2).
     655#g#p#ge#st#id'
     656**[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
     657#s2 #EQ #EQ' destruct(EQ)
     658whd in match eval_stmt_flow_no_seq; normalize nodelta
     659whd in match eval_stmt_flow; normalize nodelta
     660[2,3: %]
     661whd in match goto; normalize nodelta
     662whd in match set_pc; normalize nodelta
     663>pointer_of_label_eq_with_id [% | >EQ' % |]
     664qed.
     665
     666definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     667  state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
     668  λglobals,p,ge,st.
     669  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
     670  ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
     671  let st ≝ set_no_pc … st_npc st in
     672  ! st ← eval_stmt_flow … ge st flow;
     673  return 〈tr, st〉.
    424674
    425675definition is_final: ∀globals:list ident. ∀p: sem_params.
    426   genv globals p → address → state p → option int ≝
     676  genv globals p → cpointer → state_pc p → option int ≝
    427677 λglobals,p,ge,exit,st.res_to_opt ? (
    428   do s ← fetch_statement … ge st;
     678  do s ← fetch_statement ? p … ge (pc … st);
    429679  match s with
    430680   [ RETURN ⇒
    431681      do 〈st,ra〉 ← fetch_ra … st;
    432       if eq_address ra exit then
     682      if eq_pointer ra exit then
    433683       do vals ← read_result … ge st ;
    434684       Word_of_list_beval vals
     
    436686       Error ? [ ]
    437687   | _ ⇒ Error ? [ ]]).
    438 
     688 
    439689record evaluation_parameters : Type[1] ≝
    440690 { globals: list ident
    441691 ; sparams:> sem_params
    442  ; exit: address
     692 ; exit: cpointer
    443693 ; genv2: genv globals sparams
    444694 }.
    445695
    446696definition joint_exec: trans_system io_out io_in ≝
    447   mk_trans_system … evaluation_parameters (λG. state G)
     697  mk_trans_system … evaluation_parameters (λG. state_pc G)
    448698   (λG.is_final (globals G) G (genv2 G) (exit G))
    449    (λG.eval_statement (globals G) G (genv2 G)).
     699   (λG.eval_state (globals G) G (genv2 G)).
    450700
    451701definition make_global :
     
    457707 let b ≝ mk_block Code (-1) in
    458708 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    459  let addr ≝ address_of_code_pointer ptr in
    460709  (λp. mk_evaluation_parameters
    461710    (prog_var_names … p)
    462711    (mk_sem_params … pars)
    463     addr
     712    ptr
    464713    (globalenv Genv … p)
    465714  ).
     
    470719definition make_initial_state :
    471720 ∀pars: sem_params.
    472  ∀p: joint_program … pars. res (state pars) ≝
     721 ∀p: joint_program … pars. res (state_pc pars) ≝
    473722λpars,p.
    474723  let sem_globals ≝ make_global pars p in
     
    480729  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
    481730  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    482   do sp ← address_of_pointer spp ;
    483731  let main ≝ prog_main … p in
    484   let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    485   let trace_state ≝
    486    eval_call_id … pars ge st0 main (call_args_for_main … pars)
    487     (call_dest_for_main … pars) (exit sem_globals) in
    488   match trace_state with
    489   [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
    490   | Wrong msg ⇒ Error … msg
    491   | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    492   ].
    493 [3: % | cases ispb | cases spb] * #r #off #E >E %
     732  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
     733  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     734  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
     735  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     736  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
     737  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
     738  match main_fd with
     739  [ Internal fn ⇒
     740    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     741  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     742  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
    494743qed.
    495744
Note: See TracChangeset for help on using the changeset viewer.