Ignore:
Timestamp:
Dec 10, 2012, 8:11:35 PM (7 years ago)
Author:
piccolo
Message:

completed isFinal and fetchStatementSigmaCommute. Fixed exit definition and sigma_pc in semantics.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2548 r2551  
    1818include "joint/semanticsUtils.ma".
    1919
     20axiom globalenv_no_minus_one :
     21 ∀F,V,i,p.
     22  find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?. 
     23
     24lemma fetch_internal_function_no_minus_one :
     25  ∀F,V,i,p,bl.
     26  block_id (pi1 … bl) = -1 →
     27  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
     28    bl = Error … [MSG BadFunction].
     29 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     30 whd in match fetch_internal_function;
     31  whd in match fetch_function; normalize nodelta
     32  >globalenv_no_minus_one
     33  cases (symbol_for_block ???) normalize //
     34qed.
     35   
    2036lemma bind_option_inversion_star:
    2137  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     
    224240  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) →
    225241    label → option ℕ.
    226    
     242
    227243definition sigma_pc_opt:
    228244 ∀p,p'.∀graph_prog.
     
    233249  let pars ≝ make_sem_graph_params p p' in
    234250  let ge ≝ globalenv_noinit … prog in
    235   ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
    236   ! lin_point ← sigma fd (point_of_pc pars pc) ;
    237   return pc_of_point
    238   (make_sem_lin_params ? p') (pc_block pc) lin_point.
     251  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
     252    return pc
     253  else
     254    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
     255    ! lin_point ← sigma fd (point_of_pc pars pc) ;
     256    return pc_of_point
     257    (make_sem_lin_params ? p') (pc_block pc) lin_point.
    239258
    240259definition well_formed_pc:
     
    448467%
    449468[2: whd in ⊢ (???%);
    450   cut (∀X,a,b.a = b → Some X a = Some X b) [ // ]
    451   #aux @aux
     469  @eq_f
    452470  @mem_ext_eq [2: % ]
    453471  #b @if_elim
     
    724742    (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    725743      ext i (\fst (linearise_int_fun … fn)))
    726 }.
    727 (* TO BE ADAPTED AS ABOVE
    728744; setup_call_commute :
    729   ∀ n , parsT, call_args , st1 , st2 , prf1.
    730   setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
    731   ∃prf2.
    732   setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    733   return (sigma_state p p' graph_prog sigma gsss st2 prf2)
     745  ∀ n , parsT, call_args.
     746  preserving … res_preserve …
     747    (sigma_state … gsss)
     748    (sigma_state … gsss)
     749    (setup_call ?? (p' ?) n parsT call_args)
     750    (setup_call ?? (p' ?) n parsT call_args)
    734751; fetch_external_args_commute : (* TO BE CHECKED *)
    735752  ∀ex_fun,st1,prf1,call_args.
     
    737754  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
    738755; set_result_commute :
    739   ∀ l , call_dest , st1 , st2 , prf1.
    740   set_result ?? (p' ?) l call_dest st1 = return st2 →
    741   ∃prf2.
    742   set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    743   return (sigma_state p p' graph_prog sigma gsss st2 prf2) 
     756  ∀ l , call_dest.
     757  preserving … res_preserve …
     758    (sigma_state … gsss)
     759    (sigma_state … gsss)
     760    (set_result ?? (p' ?) l call_dest)
     761    (set_result ?? (p' ?) l call_dest) 
    744762; read_result_commute :
    745763  let lin_prog ≝ linearise p graph_prog in
    746764  ∀stack_sizes.
    747   ∀call_dest , st1 , prf1, l1.
    748   read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    749     call_dest st1 = return l1 →
    750   ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
    751   read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    752     call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 
     765  ∀call_dest.
     766  preserving … res_preserve …
     767    (sigma_state … gsss)
     768    (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf)
     769    (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes))
     770     call_dest)
     771    (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     772     call_dest)
    753773; pop_frame_commute :
    754774  let lin_prog ≝ linearise p graph_prog in
    755   ∀stack_sizes.
    756   ∀ st1 , prf1, curr_id , curr_fn ,st2.
    757   pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    758             curr_id curr_fn st1 = return st2 →
    759  ∃prf2.
    760  let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
    761  let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
    762   pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    763             curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    764             return mk_state_pc ? st2' pc'
     775  ∀stack_sizes, curr_id , curr_fn.
     776  preserving … res_preserve …
     777    (sigma_state … gsss)
     778    (λst : state_pc ?.λprf.
     779      mk_state_pc …
     780        (sigma_state … gsss st (proj2 ?? prf))
     781        (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf)))
     782  (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     783            curr_id curr_fn)
     784  (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     785            curr_id (\fst (linearise_int_fun … curr_fn)))
    765786}.
    766 *)
    767 
    768 
    769 
    770 
    771787
    772788lemma store_commute :
     
    855871 @prog_if_of_function_transform % qed.
    856872*)
    857 lemma sigma_pblock_eq_lemma :
     873lemma pc_block_sigma_commute :
    858874∀p,p',graph_prog.
    859875let lin_prog ≝ linearise p graph_prog in
     
    863879 pc_block pc.
    864880 #p #p' #graph_prog #sigma #pc #prf
    865  whd in match sigma_pc; normalize nodelta
    866  @opt_safe_elim #x #H @('bind_inversion H) -H * #i #fn #_
    867  #H @('bind_inversion H) -H #n #_ whd in ⊢ (??%?→?);
     881 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     882 @opt_safe_elim #x
     883 @if_elim #_
     884 [2: #H @('bind_inversion H) -H * #i #fn #_
     885   #H @('bind_inversion H) -H #n #_ ]
     886 whd in ⊢ (??%?→?);
    868887 #EQ destruct %
    869888qed.
     
    11111130 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
    11121131 good_local_sigma p globals graph_code entry lin_code sigma →
     1132 code_closed … lin_code →
    11131133 sigma lbl = return pt →
    11141134 ∀stmt.
     
    11231143               (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧
    11241144                  ((sigma nxt = Some ? (S pt)) ∨
    1125                    (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt)))
     1145                   (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧
     1146                    point_of_label … lin_code nxt = sigma nxt) )
    11261147             | COND a ltrue ⇒
    11271148               (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧
    11281149               sigma nxt = Some ? (S pt)) ∨
    1129                (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt))
     1150               (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧
     1151                point_of_label … lin_code nxt = sigma nxt)
    11301152             ]
    11311153 | FCOND abs _ _ _ ⇒ Ⓧabs   
    11321154 ]. 
    11331155 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
    1134  * #_ #lin_stmt_spec #prf
     1156 ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf
    11351157elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec
    11361158#All_succs_in #next_spec
    11371159#stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ)
    11381160% [assumption]
    1139 //
     1161cases stmt in next_spec; -stmt
     1162[ * [ #s | #a #lbl ] #nxt | #s | * ]
     1163normalize nodelta
     1164[ * #H #G %{H}
     1165  cases G -G #G
     1166  [ %1{G} ]
     1167| * [ #H %1{H} ] #G
     1168| //
     1169] %2 %{G}
     1170  lapply (refl …  (point_of_label … lin_code nxt))
     1171  change with (If ? then with prf do ? else ?) in ⊢ (???%→?);
     1172  @If_elim <(lin_code_has_label … (mk_lin_params p))
     1173  [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ]
     1174  * #H cases (H ?) -H
     1175  lapply (lin_code_closed … G) ** [2: #_ * ] //
    11401176qed.
    11411177 
     
    11981234    @opt_safe_elim #pc'
    11991235  ]
    1200   whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
    1201   >point_of_pc_of_point
    1202   >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) %
     1236  whd in match sigma_pc_opt; normalize nodelta
     1237  @eqZb_elim #Hbl normalize nodelta
     1238  [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn;
     1239  |*: >fetchfn >m_return_bind
     1240    >point_of_pc_of_point
     1241    >EQsigma
     1242  ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    12031243]
    12041244qed.
     
    12151255qed.
    12161256
     1257lemma point_of_pc_sigma_commute :
     1258 ∀p,p',graph_prog.
     1259 let lin_prog ≝ linearise p graph_prog in
     1260 ∀sigma,pc,f,fn,n.
     1261  ∀prf : well_formed_pc p p' graph_prog sigma pc.
     1262 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
     1263 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
     1264 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     1265#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
     1266whd in match sigma_pc; normalize nodelta
     1267@opt_safe_elim #pc' whd in match sigma_pc_opt;
     1268normalize nodelta @eqZb_elim #Hbl
     1269[ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch;
     1270  whd in ⊢ (???%→?); #ABS destruct(ABS) ]
     1271>EQfetch >m_return_bind >EQsigma
     1272whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1273@point_of_offset_of_point 
     1274qed.
     1275
    12171276lemma graph_succ_pc :
    12181277  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
     
    12291288  fetch_statement (make_sem_graph_params p p') …
    12301289    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    1231   All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
     1290(*  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
    12321291      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
    12331292      pc_of_label (make_sem_lin_params p p') …
     
    12351294          (pc_block pc)
    12361295          lbl = return sigma_pc … prf)
    1237     (stmt_explicit_labels … stmt) ∧
     1296    (stmt_explicit_labels … stmt) ∧ *)
    12381297  match stmt with
    12391298  [  sequential s nxt ⇒
     
    12841343inversion(sigma_pc_opt p p' graph_prog sigma pc)
    12851344[#ABS @⊥ >ABS in wfprf; * #H @H %]
    1286 #lin_pc #lin_pc_spec
    1287 whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec;
    1288 @('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn
    1289 #EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) -H
     1345#lin_pc
     1346whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta  in ⊢ (%→?);
     1347@eqZb_elim #Hbl
     1348[ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ]
     1349normalize nodelta >fetchfn >m_return_bind
     1350#H @('bind_inversion H) -H
    12901351#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
    1291 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt)
    1292 [@lin_pt_spec|] * #H1 #H2 %
    1293 [ -H2 @(All_mp … (All_append_r H1) #lab #lab_spec
    1294   whd in match well_formed_pc; normalize nodelta
    1295   whd in match sigma_pc_opt; normalize nodelta >fetchfn
    1296   >m_return_bind whd in match point_of_pc; whd in match pc_of_point;
    1297   normalize nodelta >point_of_offset_of_point
    1298   cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %]
    1299   #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?));
    1300   % #ABS destruct(ABS)
    1301 ] lapply H2
     1352lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt)
     1353[@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 (* #H2 %
     1354[ @In_All
     1355  #lab #lab_in
     1356  lapply (All_In ??? lab H1 ?)
     1357  [ @Exists_append_r assumption ]
     1358  inversion (sigma graph_fun lab) [#_ * #ABS @⊥ @ABS %]
     1359  #lin_pt #EQsigma #_
     1360  %
     1361  [ @hide_prf whd %
     1362  | whd in match sigma_pc; normalize nodelta
     1363    @opt_safe_elim #pc_lin
     1364  ] whd in match sigma_pc_opt;
     1365  normalize nodelta >(eqZb_false … Hbl) >fetchfn normalize nodelta
     1366  >m_return_bind >point_of_pc_of_point >EQsigma
     1367  #EQ whd in EQ : (??%?); destruct(EQ)
     1368  whd in match pc_of_label; normalize nodelta
     1369  >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1370  inversion (point_of_label ????)
     1371  [2: #lin_pt' #EQ lapply (all_labels_in … EQ) >EQsigma
     1372    #EQ' destruct % ]
     1373  change with (If ? then with prf do ? else ? = ? → ?)   
     1374  @If_elim <(lin_code_has_label … (mk_lin_params p))
     1375  [ #_ whd in ⊢ (??%?→?); #EQ destruct ]
     1376  #ABS cases (absurd ?? ABS)
     1377  lapply (pi2 … (\fst (linearise_int_fun … graph_fun)) … )
     1378  [2:
     1379  normalize nodelta
     1380 
     1381  >m_return_bind whd in ⊢ (?(??%?));
     1382    % #ABS destruct(ABS)
     1383   
     1384      >(eqZb_false … Hbl) normalize nodelta >fetchfn
     1385    >m_return_bind >point_of_pc_of_point inversion(sigma graph_fun lab) in lab_spec;
     1386    [ #_ * #ABS @⊥ @ABS %] #linear_pt #linear_pt_spec #_ >m_return_bind
     1387    whd in match pc_of_label; normalize nodelta
     1388    >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1389
     1390] lapply H2 *)
    13021391cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    13031392#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
    1304 >sigma_pblock_eq_lemma
     1393>pc_block_sigma_commute
    13051394>(fetch_internal_function_transf … fetchfn) >m_return_bind
     1395>(point_of_pc_sigma_commute … fetchfn lin_pt_spec)
    13061396[ %
    1307    [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta
    1308      @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta
    1309     >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point
    1310     >(proj1 … H3) >m_return_bind //
    1311    |
    1312    %
    1313       [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt;
    1314         normalize nodelta lapply fetchfn
    1315         whd in match fetch_internal_function; normalize nodelta
    1316         #H4 @('bind_inversion H4) #x #x_spec
    1317         >x_spec >m_return_bind #EQ >EQ >m_return_bind
    1318         whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc;
    1319         whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
    1320         cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
    1321         cases all_labels_spec #Z #_ #sn
    1322         whd in match (point_of_succ ???);
    1323         >(opt_to_opt_safe … Z) % #ABS whd in ABS : (??%?); destruct(ABS)
    1324       | cases(proj2 … H3)
    1325         [ #Z %1 whd in match sigma_pc; normalize nodelta
    1326           @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta
    1327           >lin_pc_spec #EQ destruct(EQ)
    1328           @opt_safe_elim #pc2 >fetchfn >m_return_bind >graph_succ_pc
    1329           >point_of_pc_of_point
    1330           >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ)
    1331           whd in match succ_pc;
    1332           whd in match point_of_pc; whd in match point_of_succ; normalize nodelta
     1397   [ >(proj1 … H3) %
     1398   | % [ @hide_prf %
     1399     | change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?);
     1400       @opt_safe_elim #pc1
     1401     ] whd in match sigma_pc_opt;
     1402        normalize nodelta >(eqZb_false … Hbl) >fetchfn
     1403        >m_return_bind
     1404        >graph_succ_pc >point_of_pc_of_point
     1405        cases(proj2 … H3)
     1406        [1,3: #EQ >EQ
     1407        |*: * cases all_labels_spec #Z #_ #sn
     1408          >(opt_to_opt_safe … Z) #EQpoint_of_label
     1409        ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1410        [ %1
     1411          whd in match (point_of_succ ???) ;
     1412          whd in match point_of_pc; normalize nodelta
     1413          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     1414          @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind
     1415          >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1416          whd in match succ_pc; whd in match point_of_pc; normalize nodelta
    13331417          >point_of_offset_of_point %
    1334         | #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta
    1335           #H @('bind_inversion H) -H * #x1 #x2 #x_spec
    1336           lapply(fetch_function_transf ???? graph_prog
    1337             (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec)
    1338           #HH
    1339           <sigma_pblock_eq_lemma in HH; [2:@wfprf|||||] #HH >HH >m_return_bind
    1340           cases x2 normalize nodelta [#g_fun | #xxx] #EQ whd in EQ : (??%%); destruct(EQ)
    1341           >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta
    1342           whd in match pc_of_point; normalize nodelta  >point_of_offset_of_point
    1343           whd in match sigma_pc; normalize nodelta
    1344           @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
    1345           >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?);
    1346           destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
    1347            >Z >m_return_bind %
    1348          ]
     1418        | %2 whd in match (pc_block ?); >pc_block_sigma_commute
     1419          >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1420          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     1421          @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta
     1422          #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind
     1423          whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct
     1424          whd in match point_of_pc; whd in match succ_pc; normalize nodelta
     1425          whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1426          whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
     1427          >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta
     1428           >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1429           >EQpoint_of_label %
     1430        ]
     1431   ]
     1432 | % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta
     1433      >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn
     1434      >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta
     1435      whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
     1436      >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_
     1437      >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)]
     1438   cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind
     1439      [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     1440       @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2
     1441       >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind
     1442       >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc;
     1443       normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
     1444       >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ
     1445       whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ
     1446       whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point %
     1447      |%2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label;
     1448       normalize nodelta >(fetch_internal_function_transf … fetchfn)
     1449       >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE
     1450       >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind
     1451       normalize in ⊢ (??%?);
     1452       whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     1453       @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?);
     1454       >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc;
     1455       normalize nodelta whd in match point_of_pc; whd in match pc_of_point;
     1456       normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H;
     1457       [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind
     1458       #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta %
    13491459      ]
    1350    ]
    1351    | cases H3
    1352       [ * #Z1 #Z2 %1 % [ @hide_prf  whd in match well_formed_pc;
    1353         whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
    1354         >graph_succ_pc >point_of_pc_of_point
    1355         >Z2 % #ABS whd in ABS : (??%?); destruct(ABS)
    1356       ] %
    1357       [ whd in match sigma_pc; normalize nodelta
    1358         @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
    1359         >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?);
    1360         destruct(EQ) whd in match point_of_pc; normalize nodelta
    1361         >point_of_offset_of_point >Z1 >m_return_bind %
    1362       | whd in match sigma_pc; normalize nodelta
    1363        @opt_safe_elim #line_pc
    1364        @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta
    1365        >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc;
    1366        normalize nodelta  >point_of_offset_of_point >Z2 >m_return_bind
    1367        #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind
    1368        #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc;
    1369        normalize nodelta >point_of_offset_of_point %
    1370        ]
    1371        | #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind
    1372          @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
    1373          >fetchfn >m_return_bind >lin_pt_spec >m_return_bind
    1374          #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta
    1375          >point_of_offset_of_point >Z >m_return_bind %
    1376         ]
    1377    | whd in match sigma_pc; normalize nodelta @opt_safe_elim
    1378      #line_pc whd in match sigma_pc_opt; normalize nodelta  >fetchfn >m_return_bind
    1379       >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ)
    1380       whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
    1381       >H3 >m_return_bind %
    1382    ]
    1383    qed.
    1384 
    1385 lemma point_of_pc_sigma_commute :
    1386  ∀p,p',graph_prog.
    1387  let lin_prog ≝ linearise p graph_prog in
    1388  ∀sigma,pc,f,fn,n.
    1389   ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1390  fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
    1391  sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
    1392  point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
    1393 #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
    1394 whd in match sigma_pc; normalize nodelta
    1395 @opt_safe_elim #pc' whd in match sigma_pc_opt;
    1396 normalize nodelta >EQfetch >m_return_bind >EQsigma
    1397 whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1398 @point_of_offset_of_point
    1399 qed.
     1460  | >H3 >m_return_bind %
     1461]
     1462qed. 
     1463
     1464
     1465lemma res_eq_from_opt : ∀A,m,a.
     1466res_to_opt A m = return a → m = return a.
     1467#A #m #a  cases m #x normalize #EQ destruct(EQ) %
     1468qed.
     1469
    14001470
    14011471definition linearise_status_rel:
     
    14031473 let lin_prog ≝ linearise p graph_prog in
    14041474 ∀stack_sizes.
    1405  ∀sigma,gss.
     1475 ∀sigma. ∀ gss : good_state_sigma p p' graph_prog sigma.
    14061476 good_sigma p graph_prog sigma →
    14071477   status_rel
     
    14181488    (* sim_final ≝ *) ?.
    14191489#st1 #st2 * #prf #EQ2
    1420 %
     1490% [2: cases daemon]
     1491>EQ2
    14211492whd in ⊢ (%→%);
    14221493#H lapply (opt_to_opt_safe … H)
    1423 @opt_safe_elim -H
    1424 #res #_
    1425 #H cases daemon (*
     1494@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
     1495#H lapply(res_eq_from_opt ??? H) -H
    14261496#H  @('bind_inversion H) -H
    1427 * #f #stmt
    1428 whd in match fetch_statement; normalize nodelta
    1429 #H @('bind_inversion H) -H *
    1430 #id #int_f
    1431 whd in match fetch_internal_function; normalize nodelta
    1432 #H @('bind_inversion H) -H * #id1 #int_f1
    1433 whd in match fetch_function; normalize nodelta
    1434 #H lapply(opt_eq_from_res ???? H) -H
    1435 #H @('bind_inversion H) -H #id2
    1436 whd in match symbol_for_block; normalize nodelta
    1437 whd in match option_map; normalize nodelta
    1438 cases (find ?? (symbols ? ?) ?) normalize nodelta
    1439 [1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ)
    1440 #H @('bind_inversion H) -H #int_f2 whd in match find_funct_ptr;
    1441 normalize nodelta cases(block_region (pc_block (pc ? ?)))
    1442 normalize nodelta [1,3: #ABS destruct(ABS)]
    1443 cases(block_id (pc_block (pc ??))) normalize nodelta
    1444 [1,2,4,5: [2,4: #pos] #ABS destruct(ABS)]
    1445 #pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ)
    1446 cases int_f1 in int_f2_spec; normalize nodelta
    1447 [2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1448 #int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1449 #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H
    1450 #stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1451 cases (stmt) in stmt1_spec; normalize nodelta
    1452 [1,3,4,6: [1,3: #js #jsucc #_ | 2,4: #a #b #c #d #_] #ABS whd in ABS : (???%);
    1453  destruct(ABS)]
    1454 #fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta
    1455 [1,3,4,6: [1,3: #l #_|2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)]
    1456 #STMT_SPEC #H @('bind_inversion H) -H #state_pc #state_pc_sepc
    1457 #H @('bind_inversion H) -H #succ_pc whd in match next_of_pc; normalize nodelta
    1458 #H @('bind_inversion H) -H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta
    1459 #H @('bind_inversion H) -H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta
    1460 #H @('bind_inversion H) -H * #id6 #int_f6 whd in match fetch_function; normalize nodelta
    1461 #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id7
    1462 whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta
    1463 cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)]
    1464 #sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) -H #int_f7
    1465 whd in match find_funct_ptr; normalize nodelta
    1466 cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)]
    1467 cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)]
    1468 #pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec;
    1469 normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1470 #int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1471 #H @('bind_inversion H) -H #stmt2 #H lapply(opt_eq_from_res ???? H) -H
    1472 #stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1473 cases int_f4 in stmt2_spec; normalize nodelta
    1474 [2,3,5,6:
    1475 
    1476 xxxxxxxxxxxxxx
    1477 *)
     1497** #id #int_f #stmt
     1498#stmt_spec lapply(fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
     1499cases stmt in stmt_spec; -stmt normalize nodelta
     1500[1,3: [ #a #b #_| #a #b #c #d #e] #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1501#fin_step cases(fin_step) -fin_step normalize nodelta
     1502[1,3: [#l| #a #b #c] #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
     1503#fetch_graph_spec #fetch_lin_spec
     1504#H >fetch_lin_spec >m_return_bind normalize nodelta
     1505@('bind_inversion H) -H #state_pc #state_pc_spec
     1506elim(pop_frame_commute
     1507  p p' graph_prog sigma gss ? id int_f ? (hide_prf … (proj2 … prf)) … state_pc_spec)
     1508#wf_state_pc normalize nodelta #sigma_state_pc_commute >sigma_state_pc_commute
     1509>m_return_bind @eq_program_counter_elim normalize nodelta
     1510[2: #_ #EQ whd in EQ : (???%); destruct(EQ)] #state_pc_spec #H
     1511@eq_program_counter_elim normalize nodelta
     1512[2: * #ABS @⊥ @ABS whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
     1513    @opt_safe_elim #next_pc @eqZb_elim normalize nodelta >state_pc_spec
     1514    [2: * #ABS1 @⊥ @ABS1 normalize %] #_ #EQ whd in EQ : (??%?); destruct(EQ) %
     1515|   #_ @('bind_inversion H) -H #list_val #list_val_spec 
     1516elim(read_result_commute p p' graph_prog sigma gss ? ? ? ? ? list_val_spec)
     1517[2: @hide_prf @(proj2 … prf)] #wf_lm #EQ >EQ -EQ >m_return_bind
     1518whd in match Word_of_list_beval in ⊢ (% → ?); normalize nodelta
     1519#H @('bind_inversion H) -H * #b1 #l1 #b1_l1_spec #H
     1520cases list_val in list_val_spec wf_lm b1_l1_spec; -list_val normalize nodelta
     1521[ #_ #l #ABS whd in ABS : (???%); destruct(ABS)]
     1522#b2 #l2 #b2_l2_spec #wf_b2_l2 #H1 @('bind_inversion H1) -H1
     1523#bt whd in match Byte_of_val; normalize nodelta
     1524cases (b2) in b2_l2_spec wf_b2_l2; -b2 normalize nodelta
     1525[1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (???%); destruct(ABS)]
     1526#by #by_l2_spec #wf_by_l2 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%);
     1527destruct(EQ) @('bind_inversion H) -H * #by1 #l3
     1528cases l1 in by_l2_spec wf_by_l2; -l1 normalize nodelta [ #_ #a #ABS whd in ABS : (???%); destruct(ABS)]
     1529#val #l1 #b1_val_l1_spec #wf_b1_val_l1 #H @('bind_inversion H) -H #by1
     1530cases val in b1_val_l1_spec wf_b1_val_l1; -val
     1531[1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] whd in match Byte_of_val; normalize nodelta
     1532#ABS whd in ABS : (???%); destruct(ABS)]
     1533#by2 #b1_by2_l1_spec #wf_b1_by2_l1 whd in match Byte_of_val; normalize nodelta
     1534#EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)
     1535#H @('bind_inversion H) -H * #by2 #l2
     1536cases(l3) in b1_by2_l1_spec wf_b1_by2_l1; -l3 normalize nodelta
     1537[#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
     1538#val #l1 #b1_by1_val_l1_spec #wf_b1_by1_val_l1 #H @('bind_inversion H) -H
     1539#by3 cases val in b1_by1_val_l1_spec wf_b1_by1_val_l1; -val normalize nodelta
     1540[1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (??%%); destruct(ABS)] 
     1541#by3 #b1_by1_by3_l1_spec #wf_b1_by1_by3_l1 #EQ whd in EQ : (???%); destruct(EQ)
     1542#EQ whd in EQ : (???%); destruct(EQ) #H @('bind_inversion H) -H *
     1543#by3 #l1 cases l2 in  b1_by1_by3_l1_spec  wf_b1_by1_by3_l1; -l2 normalize nodelta
     1544[#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
     1545#val #l2 #_ #wf_b1_by1_by2_val #H @('bind_inversion H) -H #by4
     1546cases val in wf_b1_by1_by2_val; -val normalize nodelta
     1547[1,2,3,5,6,7: [|| #a #b #c |#p | #p #p'|#p #pa] #a #ABS whd in ABS : (???%); destruct(ABS)]
     1548#by5 #wf_list #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)  cases l1 in wf_list; -l1 normalize nodelta [2: #val #l #a #ABS whd in ABS : (???%); destruct(ABS)]
     1549#wf_list #EQ whd in EQ : (???%); destruct(EQ)
     1550@opt_safe_elim #l #H normalize in H; destruct(H) normalize % #ABS destruct(ABS)
    14781551qed.
    14791552
Note: See TracChangeset for help on using the changeset viewer.