Changeset 2200 for src


Ignore:
Timestamp:
Jul 17, 2012, 6:00:03 PM (8 years ago)
Author:
tranquil
Message:
  • updated joint semantics: generation of linear and graph semantics
  • opened two axioms in BitVectorZ
Location:
src
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/BitVectorZ.ma

    r1516 r2200  
    33include "ASM/BitVector.ma".
    44include "ASM/Arithmetic.ma".
     5include "utilities/binary/division.ma".
    56
    67let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
    … …  
    124125theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n.
    125126#n #bv normalize
    126 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
     127lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/
    127128qed.
    128129
    … …  
    150151| #t whd in ⊢ (?%?); //
    151152] qed.
     153
     154(* TODO *)
     155axiom Z_of_unsigned_bitvector_of_Z :
     156  ∀n,z.
     157  Z_of_unsigned_bitvector n (bitvector_of_Z n z) =
     158  modZ z (Z_two_power_nat n).
     159
     160axiom bitvector_of_Z_of_unsigned_bitvector :
     161  ∀n,bv.
     162  bitvector_of_Z n (Z_of_unsigned_bitvector n bv) = bv.

  • src/joint/linearise.ma

    r2182 r2200  
    11include "joint/TranslateUtils_paolo.ma".
     2include "utilities/hide.ma".
    23
    34definition graph_to_lin_statement :
    … …  
    1516#p#globals * [//] * //
    1617qed.
    17 
    18 definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
    19 definition hide_Prop : Prop → Prop ≝ λP.P.
    20 
    21 interpretation "hide proof" 'hide p = (hide_prf ? p).
    22 interpretation "hide Prop" 'hide p = (hide_Prop p).
    2318
    2419(* discard all elements passing test, return first element failing it *)

  • src/joint/semanticsUtils_paolo.ma

    r1882 r2200  
    11include "joint/semantics_paolo.ma".
    22include alias "common/Identifiers.ma".
     3include "utilities/hide.ma".
    34
    45(*** Store/retrieve on pseudo-registers ***)
    … …  
    2122(******************************** GRAPHS **************************************)
    2223
    23 definition 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.
     24definition bitvector_from_pos :
     25  ∀n.Pos → BitVector n ≝
     26  λn,p.bitvector_of_Z n (Zpred (pos p)).
    2827
    29 definition graph_label_of_pointer: pointer → res label ≝
    30  λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
     28definition pos_from_bitvector :
     29  ∀n.BitVector n → Pos ≝
     30  λn,v.
     31  match Zsucc (Z_of_unsigned_bitvector n v)
     32  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
     33  with
     34  [ OZ ⇒ λprf.⊥
     35  | pos x ⇒ λ_. x
     36  | neg x ⇒ λprf.⊥
     37  ] (refl …).
     38@hide_prf
     39elim v in prf;
     40[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
    3141
    32 definition graph_fetch_statement:
    33  ∀pars : graph_params.
    34  ∀sem_pars : sem_state_params.
    35  ∀globals.
    36   genv globals pars →
    37   cpointer →
    38   res (joint_statement pars globals) ≝
    39  λpars,sem_pars,globals,ge,p.
    40   do f ← fetch_function … ge p ;
    41   do l ← graph_label_of_pointer p;
    42   opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
     42lemma pos_pos_from_bitvector :
     43  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
     44#n #bv elim bv -n
     45[ %
     46| #n * #bv #IH [ % | @IH ]
     47]
     48qed.
     49
     50lemma bitvector_from_pos_from_bitvector :
     51  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
     52#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
     53>Zpred_Zsucc //
     54qed.
     55
     56lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
     57  (∀q,r.
     58    ppos m = natp_plus (natp_times q (ppos n)) r →
     59    natp_lt r n →
     60    P (〈q,r〉)) →
     61  P (divide m n).
     62#P #m #n #H
     63lapply (refl … (divide m n))
     64cases (divide ??) in ⊢ (???%→%);
     65#q #r #EQ elim (divide_ok … EQ) -EQ @H
     66qed.
     67
     68lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
     69  p < q → \snd (divide p q) = ppos p.
     70#p #q #H @divide_elim * [2: #quot ]
     71* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
     72@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
     73[ @(transitive_le … (quot*q)) ] /2 by /
     74qed.
     75
     76lemma pos_from_bitvector_from_pos :
     77  ∀n,p.
     78  p ≤ two_power_nat n →
     79  pos_from_bitvector n (bitvector_from_pos n p) = p.
     80#n #p #H
     81cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
     82[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
     83>pos_pos_from_bitvector
     84whd in match (bitvector_from_pos ??);
     85>Z_of_unsigned_bitvector_of_Z
     86cases p in H ⊢ %;
     87[ #_ %
     88|*: #p' #H
     89  whd in match (Zpred ?);
     90  whd in match (Z_two_power_nat ?);
     91  whd in ⊢ (??(?%)?);
     92  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
     93  whd
     94  <succ_pred_n try assumption % #ABS destruct(ABS)
     95]
     96qed.
     97
     98lemma pos_from_bitvector_max : ∀n,bv.
     99  pos_from_bitvector n bv ≤ two_power_nat n.
     100#n #bv
     101change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
     102>pos_pos_from_bitvector
     103@Zlt_to_Zle
     104@bv_Z_unsigned_max
     105qed.
     106
     107definition graph_offset_of_label : label → option offset ≝
     108  λl.let p ≝ word_of_identifier … l in
     109  if leb p (two_power_nat offset_size) then
     110    return mk_offset (bitvector_from_pos … p)
     111  else
     112    None ?.
     113
     114definition graph_label_of_offset: offset → label ≝
     115 λo.an_identifier ? (pos_from_bitvector ? (offv o)).
    43116
    44117definition make_sem_graph_params :
    … …  
    52125      pars
    53126      g_pars
    54       graph_pointer_of_label
    55       (λ_.λ_.graph_pointer_of_label)
    56       (graph_fetch_statement ? g_pars)
     127      graph_offset_of_label
     128      graph_label_of_offset
     129      ??
    57130    ).
    58    
     131whd in match graph_label_of_offset;
     132whd in match graph_offset_of_label;
     133whd in match word_of_identifier;
     134normalize nodelta * #x
     135@(leb_elim ? (two_power_nat ?)) normalize nodelta
     136[ #_ >bitvector_from_pos_from_bitvector %
     137| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
     138| #H whd >(pos_from_bitvector_from_pos … H) %
     139| #_ %
     140]
     141qed.
     142
    59143(******************************** LINEAR **************************************)
    60 check mk_pointer
    61 definition 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.
    64144
    65 axiom BadLabel: String.
     145definition lin_offset_of_nat : ℕ → option offset ≝
     146  λn.
     147  if leb (S n) (2^offset_size) then
     148    return mk_offset (bitvector_of_nat ? n)
     149  else
     150    None ?.
    66151
    67 definition lin_pointer_of_label:
    68  ∀pars : lin_params.
    69  ∀globals. genv globals pars → cpointer → label → res cpointer ≝
    70  λpars,globals,ge,old,l.
    71   do fn ← fetch_function … ge old ;
    72   do pos ←
    73    opt_to_res ? [MSG BadLabel]
    74     (position_of ?
    75       (λs. let 〈l',x〉 ≝ s in
    76         match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
    77      (joint_if_code … pars fn)) ;
    78   OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    79 % qed.
     152definition lin_nat_of_offset : offset → ℕ ≝
     153  λo.nat_of_bitvector ? (offv o).
    80154
    81 definition lin_fetch_statement:
    82  ∀pars : lin_params.
    83  ∀sem_pars : sem_state_params.
    84  ∀globals.
    85  genv globals pars → cpointer → res (joint_statement pars globals) ≝
    86  λpars,sem_pars,globals,ge,ppc.
    87   do fn ← fetch_function … ge ppc ;
    88   let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
    89   do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
    90   return (\snd found).
    91155
    92156definition make_sem_lin_params :
    … …  
    100164      pars
    101165      g_pars
    102       lin_succ_p
    103       (lin_pointer_of_label ?)
    104       (lin_fetch_statement ? g_pars)
     166      lin_offset_of_nat
     167      lin_nat_of_offset
     168      ??
    105169    ).
    106    
    107 definition 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 
    119 definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
    120   λp,globals,stp.match stp with
    121   [ sequential _ _ ⇒ false
    122   | _ ⇒ true
    123   ].
    124 
    125 inductive 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 
    131 include "utilities/bind_new.ma".
    132 
    133 definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
    134 
    135 definition 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 
    140 interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
    141 
    142 let 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 
    150 let 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 
    156 let 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 
    163 definition 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 
    168 definition 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
     170[ * ] #x
     171whd in match lin_offset_of_nat;
     172whd in match lin_nat_of_offset;
     173normalize nodelta
     174@leb_elim normalize nodelta #H
     175[ >bitvector_of_nat_inverse_nat_of_bitvector %
     176| @⊥ cases H #H @H -H -H //
     177| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
     178| %
    174179]
    175180qed.
    176 
    177 lemma 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 ]
    183 qed.
    184  
    185 definition 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 
    191 definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
    192 
    193 let 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  
    204 definition 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 
    207 record 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 *)
    218 definition 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)
    224 qed.
    225 
    226 definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
    227 cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
    228 lapply (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: % ]] % |*:]|*:]
    231 qed.
    232 
    233 definition 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).
    249 elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
    250 elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
    251 assumption
    252 qed.
    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

    r2186 r2200  
    308308record more_sem_params (pp : params) : Type[1] ≝
    309309  { msg_pars :> more_sem_genv_params pp
    310   ; offset_of_point : code_point pp → offset
    311   ; point_of_offset : offset → option (code_point pp)
    312   ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
    313   ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
     310  ; offset_of_point : code_point pp → option offset (* can overflow *)
     311  ; point_of_offset : offset → code_point pp
     312  ; point_of_offset_of_point :
     313    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
     314  ; offset_of_point_of_offset :
     315    ∀o.offset_of_point (point_of_offset o) = Some ? o
    314316  }.
    315317
     318axiom CodePointerOverflow : String.
     319
    316320definition pointer_of_point : ∀p.more_sem_params p →
    317   cpointer→ code_point p → cpointer ≝
     321  cpointer→ code_point p → res cpointer ≝
    318322  λp,msp,ptr,pt.
    319     mk_pointer (pblock ptr) (offset_of_point p msp pt).
     323  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
     324  return «mk_pointer (pblock ptr) o, ?».
    320325elim ptr #ptr' #EQ <EQ % qed.
    321326
    322 axiom BadOffsetForCodePoint : String.
    323 
    324327definition point_of_pointer :
    325   ∀p.more_sem_params p → cpointer → res (code_point p) ≝
    326   λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
    327     (point_of_offset p msp (poff ptr)).
     328  ∀p.more_sem_params p → cpointer → code_point p ≝
     329  λp,msp,ptr.point_of_offset p msp (poff ptr).
    328330
    329331lemma point_of_pointer_of_point :
    330   ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
    331 #p #msp #ptr #pt normalize
    332 >point_of_offset_of_point %
     332  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     333  pointer_of_point p msp ptr1 pt = return ptr2 →
     334  point_of_pointer p msp ptr2 = pt.
     335#p #msp #ptr1 #ptr2 #pt normalize
     336lapply (point_of_offset_of_point p msp pt)
     337cases (offset_of_point ???) normalize
     338[ * #ABS destruct(ABS)
     339| #o #EQ1 #EQ2 destruct %
     340]
    333341qed.
    334342
    335343lemma pointer_of_point_block :
    336   ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
    337 / by refl/
     344  ∀p,msp,ptr1,ptr2,pt.
     345  pointer_of_point p msp ptr1 pt = return ptr2 →
     346  pblock ptr2 = pblock ptr1.
     347#p #msp #ptr1 #ptr2 #pt normalize
     348cases (offset_of_point ???) normalize
     349[ #ABS destruct(ABS)
     350| #o #EQ destruct(EQ) %
     351]
    338352qed.
    339353
    … …  
    346360
    347361lemma pointer_of_point_of_pointer :
    348   ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
    349     pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
    350     pointer_of_point p msp ptr2 pt = ptr1.
     362  ∀p,msp.∀ptr1,ptr2 : cpointer.
     363    pblock ptr1 = pblock ptr2 →
     364    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
    351365#p #msp ** #b1 #o1 #EQ1
    352366        ** #b2 #o2 #EQ2
    353 #pt #EQ3
    354 destruct
    355 lapply (offset_of_point_of_offset p msp o1)
    356 normalize
    357 elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
    358 #pt' #EQ #EQ' destruct %
     367#EQ3 destruct
     368normalize >offset_of_point_of_offset normalize %
    359369qed.
    360 
    361370
    362371axiom ProgramCounterOutOfCode : String.
    … …  
    367376  genv globals p → cpointer → res (joint_statement p globals) ≝
    368377  λp,msp,globals,ge,ptr.
    369   ! pt ← point_of_pointer ? msp ptr ;
     378  let pt ≝ point_of_pointer ? msp ptr in
    370379  ! fn ← fetch_function … ge ptr ;
    371380  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
    … …  
    377386  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    378387            (point_of_label … (joint_if_code … fn) lbl) ;
    379   return (mk_pointer(mk_block Code (block_id (pblock ptr)))
    380     (offset_of_point p msp pt) : Σp.?). // qed.
     388  pointer_of_point p msp ptr pt.
    381389
    382390definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
    383391  cpointer → succ p → res cpointer ≝
    384392  λp,msp,ptr,nxt.
    385   ! curr ← point_of_pointer p msp ptr ;
    386   return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
     393  let curr ≝ point_of_pointer p msp ptr in
     394  pointer_of_point p msp ptr (point_of_succ p curr nxt).
    387395
    388396record sem_params : Type[1] ≝
    … …  
    564572    let st' ≝ set_regs p regs st in
    565573    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    566     let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     574    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
    567575    return mk_state_pc ? st' pc. % qed.
    568576
Note: See TracChangeset for help on using the changeset viewer.