Changeset 2300 for src/RTLabs


Ignore:
Timestamp:
Aug 21, 2012, 7:00:43 PM (7 years ago)
Author:
campbell
Message:

Cut out some dead ends and add some comments to the last commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2299 r2300  
    22802280
    22812281
    2282 (* We still need to link tal_unrepeating to our definition of cost soundness.
    2283 
    2284    First, let's link unrepeating to our PCs and successors. *)
    2285 
    2286 definition RTLabs_pc_lookup : ∀ge. RTLabs_pc → option statement ≝
    2287 λge,pc.
    2288 match pc with
    2289 [ rapc_state b l ⇒
    2290   match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
    2291     match fd with [ Internal f ⇒ lookup ?? (f_graph f) l | _ ⇒ None ? ] ]
    2292 | _ ⇒ None ?
    2293 ].
    2294 
    2295 definition genv_lookup : ∀ge. block → label → option statement ≝
    2296 λge,b,l.
    2297   match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
    2298     match fd with [ Internal f ⇒ lookup ?? (f_graph f) l | _ ⇒ None ? ] ]
    2299 .
    2300 
    2301 inductive good_pc_list (ge:genv) : option block → list (as_pc (RTLabs_status ge)) → Prop ≝
    2302 | g_pc_end : ∀pc,b.
    2303     good_pc_list ge b [pc]
    2304 | g_pc_step : ∀b,l1,st,l2,tl.
    2305     genv_lookup ge b l1 = Some ? st →
    2306     l2 ∈ successors st →
    2307     good_pc_list ge (Some ? b) (rapc_state b l2::tl) →
    2308     good_pc_list ge (Some ? b) (rapc_state b l1::rapc_state b l2::tl)
    2309 | g_pc_call : ∀b,l1,st,l2,b',tl.
    2310     genv_lookup ge b l1 = Some ? st →
    2311     l2 ∈ successors st →
    2312     good_pc_list ge (Some ? b) (rapc_call (Some ? l2) b'::tl) →
    2313     good_pc_list ge (Some ? b) (rapc_state b l1::rapc_call (Some ? l2) b'::tl)
    2314 | g_pc_cret : ∀b,l,b',tl.
    2315     good_pc_list ge (Some ? b) (rapc_state b l::tl) →
    2316     good_pc_list ge (Some ? b) (rapc_call (Some ? l) b'::rapc_state b l::tl)
    2317 | g_pc_return : ∀b,l1,st,caller.
    2318     genv_lookup ge b l1 = Some ? st →
    2319     successors st = [ ] →
    2320     good_pc_list ge (Some ? b) [rapc_state b l1; rapc_ret caller]
    2321 .
    2322 
     2282
     2283
     2284
     2285(* We still need to link tal_unrepeating to our definition of cost soundness. *)
     2286
     2287
     2288(* Extract the "current" function from a state. *)
    23232289definition state_fn : ∀ge. RTLabs_status ge → option block ≝
    23242290λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
     
    23272293  | _ ⇒  Some ? h ] ].
    23282294
    2329 (* After returning from a function we're either in the final state, or we're
    2330    back in the caller at the correct instruction. *)
    2331 
    2332 lemma pc_after_return : ∀ge,pre,post,CL,ret,callee.
    2333   as_after_return (RTLabs_status ge) «pre,CL» post →
    2334   as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
    2335   match ret with
    2336   [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
    2337   | Some retl ⇒
    2338     ∃fn. state_fn … pre = Some ? fn ∧
    2339          state_fn … post = Some ? fn ∧
    2340          as_pc_of (RTLabs_status ge) post = rapc_state fn retl
    2341   ].
    2342 #ge #pre #post #CL #ret #callee #AF
    2343 cases pre in CL AF ⊢ %;
    2344 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
    2345     cases (lookup_present ???? (next_ok f)) in CL;
    2346     normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
    2347   | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
    2348   | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
    2349   | #r #S #M #CL normalize in CL; destruct
    2350   ]
    2351 cases post
    2352 * [ #postf #postfs #postm * [*] #fn' #S' #M'
    2353   | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
    2354   | 2,6: #A #B #C #D #E #F #G *
    2355   | 3,7: #A #B #C #D #E #F *
    2356   | #r #S' #M' #AF whd in AF; destruct
    2357   | #r #S' #M'
    2358   ]
    2359 #AF #PC normalize in PC; destruct whd
    2360 [ %{fn'} cases AF * #A #B #C destruct % [ % % | whd in ⊢ (??%?); >A % ]
    2361 | % #E normalize in E; destruct
    2362 ] qed.
     2295(* Some results to invert the classification of states *)
    23632296
    23642297lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge.
     
    23932326[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | #fn #l %{fn} %{l} % ]
    23942327qed.
    2395 
    2396 lemma tal_not_final : ∀ge,fl,s1,s2.
    2397   ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
    2398   RTLabs_is_final (Ras_state … s1) = None ?.
    2399 #ge #flx #s1x #s2x *
    2400 [ #s1 #s2 * #tr * #EX #NX #CL #CS
    2401 | #s1 #s2 * #tr * #EX #NX #CL
    2402 | #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
    2403 | #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
    2404 | #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
    2405 ] @(step_not_final … EX)
    2406 qed.
    2407 
    2408 lemma State_not_callreturn : ∀f,fs,m,cl.
    2409   RTLabs_classify (State f fs m) = cl →
    2410   match cl with
    2411   [ cl_return ⇒ False
    2412   | cl_call ⇒ False
    2413   | _ ⇒ True
    2414   ].
    2415 #f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
    2416 cases (lookup_present … (next_ok f)) //
    2417 qed.
    2418 
    2419 (* TODO: move *)
    2420 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
    2421   Exists S (λy. y = x) l →
    2422   x ∈ l.
    2423 #S #x #l elim l
    2424 [ //
    2425 | #h #t #IH
    2426   normalize lapply (eqb_true … x h)
    2427   cases (x==h) *
    2428   [ #E #_ >(E (refl ??)) //
    2429   | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
    2430             | #H @IH @H
    2431             ]
    2432   ]
    2433 ] qed.
    2434 
    2435 (* invert traces ending in a return *)
    2436 
    2437 lemma tal_return : ∀ge,fl,s1,s2.
    2438   as_classifier (RTLabs_status ge) s1 cl_return →
    2439   ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
    2440   ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
    2441 #ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
    2442 [ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
    2443   whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
    2444 | #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
    2445   %{EX} %{CL} % %
    2446 | #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
    2447   whd in CL CL'; >CL in CL'; #E destruct
    2448 | #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
    2449   whd in CL CL'; >CL in CL'; #E destruct
    2450 | #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
    2451   whd in CL CL'; >CL in CL'; #E destruct
    2452 ] qed.
    2453 
    2454 let rec tal_pc_list_succs ge fl s1 s2
    2455   (tal: trace_any_label (RTLabs_status ge) fl s1 s2)
    2456   on tal : good_pc_list ge (state_fn … s1) (tal_pc_list (RTLabs_status ge) fl s1 s2 tal) ≝
    2457 ?.
    2458 cases tal
    2459 [ #s1' #s2' #EX #CL #CS whd in ⊢ (???%); @g_pc_end
    2460 | #s1' #s2' #EX #CL @g_pc_end
    2461 | #pre #start #final #EX #CL #AF #tlr #CS @g_pc_end
    2462 | #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
    2463   whd in ⊢ (???%); lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC
    2464   [ cases (pc_after_return … AF PC) #fn' * * #SF #SF' #PC'
    2465     lapply (tal_pc_list_succs … tal')
    2466     cases (tal_pc_list_start … tal')
    2467     #tl' #E >E >PC' >SF' #IH >SF @g_pc_cret @IH
    2468   | cases (pc_after_return … AF PC) >(tal_not_final … tal') #SF'
    2469     cases (SF' ?) %
    2470   ]
    2471 | #fl' #pre #init #end #EX #tal' #CL #CS
    2472   whd in ⊢ (???%);
    2473   lapply (tal_pc_list_succs … tal')
    2474   cases (tal_pc_list_start … tal')
    2475   #tl' #E >E #IH
    2476   inversion (eval_preserves_ext … EX)
    2477   [ #ge' #f #f' #fs #m #m' * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct
    2478     cases EX #tr * #EV #NX
    2479     cases (eval_successor … EV)
    2480     [ * #CL' cases (State_not_callreturn … CL')
    2481     | * #l * #AS #SC
    2482       @(g_pc_step … (lookup_present … (next_ok f)))
    2483       [ whd in ⊢ (??%?); cases M #FFP #M >FFP
    2484         whd in ⊢ (??%?); //
    2485       | whd in AS:(??%?); destruct @Exists_memb @SC
    2486       | assumption
    2487       ]
    2488     ]
    2489   | #ge' #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct
    2490     cases EX #tr * #EV #NX
    2491     cases (eval_successor … EV)
    2492     [ * #CL' normalize in CL'; destruct
    2493     | * #l * #AS #SC
    2494       @(g_pc_call … (lookup_present … (next_ok f)))
    2495       [ whd in ⊢ (??%?); cases M #FFP #M >FFP
    2496         whd in ⊢ (??%?); //
    2497       | whd in AS:(??%?); destruct @Exists_memb @SC
    2498       | assumption
    2499       ]
    2500     ]
    2501   | #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #_ destruct
    2502     normalize in CL; destruct
    2503   | #ge' #f #fs #m #rtv #dst #m' #fn * [2: #fn' #S ] #M #M' #E1 #E2 #E3 #_ destruct
    2504     cases EX #tr * #EV #NX
    2505     cases (eval_successor … EV)
    2506     [ 1,3: * #CL' #SC
    2507       cases (tal_return … tal') [2,4: % ]
    2508       #EX' * #CL'' * #FL #TAL' destruct whd in E:(??%%); destruct
    2509       @(g_pc_return … (lookup_present … (next_ok f)))
    2510       [ 1,3: whd in ⊢ (??%?); cases M #FFP #M >FFP
    2511         whd in ⊢ (??%?); //
    2512       | 2,4: whd in AS:(??%?); destruct @SC
    2513       ]
    2514     | *: * #l * whd in ⊢ (??%% → ?); #E destruct
    2515     ]
    2516   | #ge' #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #_ destruct
    2517     normalize in CL; destruct
    2518   | #ge' #r #dst #m #M #M' #E1 #E2 #E3 #_ destruct
    2519     normalize in CL; destruct
    2520   ]
    2521 ] qed.
    2522 
    2523 let rec labels_of_pcs (l:list RTLabs_pc) : list label ≝
    2524 match l with
    2525 [ nil ⇒ [ ]
    2526 | cons h t ⇒
    2527   match h with
    2528   [ rapc_state _ l ⇒ [l]
    2529   | rapc_call l _ ⇒ match l with [ Some l ⇒ [l] | None ⇒ [ ]]
    2530   | _ ⇒ [ ]
    2531   ] @ labels_of_pcs t
    2532 ].
    2533 
    2534 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
    2535 | gl_end : bad_label_list g head head
    2536 | gl_step : ∀l1,l2,H.
    2537     l2 ∈ successors (lookup_present … g l1 H) →
    2538     ¬ is_cost_label (lookup_present … g l1 H) →
    2539     bad_label_list g head l2 →
    2540     bad_label_list g head l1.
    2541 
    2542 inductive pc_label : RTLabs_pc → label → Prop ≝
    2543 | pl_state : ∀fn,l. pc_label (rapc_state fn l) l
    2544 | pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
    2545 
    2546 discriminator option.
    2547 
    2548 lemma pc_label_eq : ∀pc,l1,l2.
    2549   pc_label pc l1 →
    2550   pc_label pc l2 →
    2551   l1 = l2.
    2552 #pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
    2553 qed.
    2554 
    2555 lemma pc_label_call_eq : ∀l,fn,l'.
    2556   pc_label (rapc_call (Some ? l) fn) l' →
    2557   l = l'.
    2558 #l #fn #l' #PC inversion PC
    2559 #a #b #E1 #E2 #E3 destruct
    2560 %
    2561 qed.
    2562 
    2563 
    2564 inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
    2565 | gf : ∀b,fn.
    2566     find_funct_ptr … ge b = Some ? (Internal ? fn) →
    2567     graph_fn ge (Some ? b) (f_graph … fn).
    2568 
    2569 lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
    2570   graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →
    2571   g = f_graph (func f).
    2572 #ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
    2573 inversion G
    2574 #b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
    2575 %
    2576 qed.
    2577 
    2578 lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
    2579   let s ≝ mk_RTLabs_state ge (State f fs m) S M in
    2580   ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
    2581   actual_successor s' = Some ? l →
    2582   state_fn ge s = state_fn ge (next_state ge s s' tr EV).
    2583 #ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
    2584 change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
    2585 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))
    2586 [ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
    2587 | #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
    2588 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
    2589 | #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
    2590   >H33 in AS; normalize #AS destruct
    2591 | #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
    2592 | #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
    2593 ] qed.
    2594 
    2595 lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
    2596   as_after_return (RTLabs_status ge) «pre,CL» post →
    2597   as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
    2598   match ret with
    2599   [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
    2600   | Some retl ⇒
    2601     state_fn … pre = state_fn … post ∧
    2602     pc_label (as_pc_of (RTLabs_status ge) post) retl
    2603   ].
    2604 #ge #pre #post #CL #ret #callee #AF
    2605 cases pre in CL AF ⊢ %;
    2606 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
    2607     cases (lookup_present ???? (next_ok f)) in CL;
    2608     normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
    2609   | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
    2610   | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
    2611   | #r #S #M #CL normalize in CL; destruct
    2612   ]
    2613 cases post
    2614 * [ #postf #postfs #postm * [*] #fn' #S' #M'
    2615   | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
    2616   | 2,6: #A #B #C #D #E #F #G *
    2617   | 3,7: #A #B #C #D #E #F *
    2618   | #r #S' #M' #AF whd in AF; destruct
    2619   | #r #S' #M'
    2620   ]
    2621 #AF #PC normalize in PC; destruct whd
    2622 [ cases AF * #A #B #C destruct % [ % | normalize >A // ]
    2623 | % #E normalize in E; destruct
    2624 ] qed.
    26252328
    26262329lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge.
     
    26442347] qed.
    26452348
     2349lemma State_not_callreturn : ∀f,fs,m,cl.
     2350  RTLabs_classify (State f fs m) = cl →
     2351  match cl with
     2352  [ cl_return ⇒ False
     2353  | cl_call ⇒ False
     2354  | _ ⇒ True
     2355  ].
     2356#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
     2357cases (lookup_present … (next_ok f)) //
     2358qed.
     2359
     2360(* And some about traces *)
     2361
     2362lemma tal_not_final : ∀ge,fl,s1,s2.
     2363  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     2364  RTLabs_is_final (Ras_state … s1) = None ?.
     2365#ge #flx #s1x #s2x *
     2366[ #s1 #s2 * #tr * #EX #NX #CL #CS
     2367| #s1 #s2 * #tr * #EX #NX #CL
     2368| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
     2369| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
     2370| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
     2371] @(step_not_final … EX)
     2372qed.
     2373
     2374(* invert traces ending in a return *)
     2375
     2376lemma tal_return : ∀ge,fl,s1,s2.
     2377  as_classifier (RTLabs_status ge) s1 cl_return →
     2378  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     2379  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
     2380#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
     2381[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
     2382  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
     2383| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
     2384  %{EX} %{CL} % %
     2385| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
     2386  whd in CL CL'; >CL in CL'; #E destruct
     2387| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
     2388  whd in CL CL'; >CL in CL'; #E destruct
     2389| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
     2390  whd in CL CL'; >CL in CL'; #E destruct
     2391] qed.
     2392
     2393(* TODO: move *)
     2394lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
     2395  Exists S (λy. y = x) l →
     2396  x ∈ l.
     2397#S #x #l elim l
     2398[ //
     2399| #h #t #IH
     2400  normalize lapply (eqb_true … x h)
     2401  cases (x==h) *
     2402  [ #E #_ >(E (refl ??)) //
     2403  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
     2404            | #H @IH @H
     2405            ]
     2406  ]
     2407] qed.
     2408
     2409(* We aim to extract a loop without a cost label to contradict the reappearance
     2410   of a pc within a trace_any_label.  This data structure represents the tail
     2411   of a loop purely in terms of the RTLabs function body graph. *)
     2412
     2413inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
     2414| gl_end : bad_label_list g head head
     2415| gl_step : ∀l1,l2,H.
     2416    l2 ∈ successors (lookup_present … g l1 H) →
     2417    ¬ is_cost_label (lookup_present … g l1 H) →
     2418    bad_label_list g head l2 →
     2419    bad_label_list g head l1.
     2420
     2421(* We need to link the pcs, states of the semantics with the labels and graphs
     2422   of the syntax. *)
     2423
     2424inductive pc_label : RTLabs_pc → label → Prop ≝
     2425| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
     2426| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
     2427
     2428discriminator option.
     2429
     2430lemma pc_label_eq : ∀pc,l1,l2.
     2431  pc_label pc l1 →
     2432  pc_label pc l2 →
     2433  l1 = l2.
     2434#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
     2435qed.
     2436
     2437lemma pc_label_call_eq : ∀l,fn,l'.
     2438  pc_label (rapc_call (Some ? l) fn) l' →
     2439  l = l'.
     2440#l #fn #l' #PC inversion PC
     2441#a #b #E1 #E2 #E3 destruct
     2442%
     2443qed.
     2444
     2445inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
     2446| gf : ∀b,fn.
     2447    find_funct_ptr … ge b = Some ? (Internal ? fn) →
     2448    graph_fn ge (Some ? b) (f_graph … fn).
     2449
     2450lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
     2451  graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →
     2452  g = f_graph (func f).
     2453#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
     2454inversion G
     2455#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
     2456%
     2457qed.
     2458
     2459lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
     2460  let s ≝ mk_RTLabs_state ge (State f fs m) S M in
     2461  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
     2462  actual_successor s' = Some ? l →
     2463  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
     2464#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
     2465change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
     2466inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))
     2467[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
     2468| #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
     2469| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
     2470| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
     2471  >H33 in AS; normalize #AS destruct
     2472| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
     2473| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
     2474] qed.
     2475
     2476lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
     2477  as_after_return (RTLabs_status ge) «pre,CL» post →
     2478  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
     2479  match ret with
     2480  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
     2481  | Some retl ⇒
     2482    state_fn … pre = state_fn … post ∧
     2483    pc_label (as_pc_of (RTLabs_status ge) post) retl
     2484  ].
     2485#ge #pre #post #CL #ret #callee #AF
     2486cases pre in CL AF ⊢ %;
     2487* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
     2488    cases (lookup_present ???? (next_ok f)) in CL;
     2489    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
     2490  | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
     2491  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
     2492  | #r #S #M #CL normalize in CL; destruct
     2493  ]
     2494cases post
     2495* [ #postf #postfs #postm * [*] #fn' #S' #M'
     2496  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
     2497  | 2,6: #A #B #C #D #E #F #G *
     2498  | 3,7: #A #B #C #D #E #F *
     2499  | #r #S' #M' #AF whd in AF; destruct
     2500  | #r #S' #M'
     2501  ]
     2502#AF #PC normalize in PC; destruct whd
     2503[ cases AF * #A #B #C destruct % [ % | normalize >A // ]
     2504| % #E normalize in E; destruct
     2505] qed.
     2506
    26462507lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l.
    26472508  actual_successor s = Some ? l →
     
    26562517
    26572518include alias "utilities/deqsets.ma".
     2519
     2520(* Build the tail of the "bad" loop using the reappearance of the original pc,
     2521   ignoring the rest of the trace_any_label once we see that pc. *)
    26582522
    26592523let rec tal_pc_loop_tail ge flX s1X s2X
     
    27192583] qed.
    27202584
    2721 (* For the first step just get a bound after the step; we don't care what it is,
     2585(* Some inversion lemmas on the bounds.
     2586
     2587   For the first step just get a bound after the step; we don't care what it is,
    27222588   just that it exists. *)
    27232589   
     
    27662632#g #l1 #l2 * /2/
    27672633qed.
     2634
     2635(* Show that a bad_label_list is incompatible with a bound on the number of
     2636   instructions to a cost label, by induction on the bound and the invariant
     2637   that none of the instructions involved are a cost label. *)
    27682638   
    27692639lemma loop_soundness_contradiction : ∀g,l1,l2,H1.
     
    27982668] qed.
    27992669
    2800      
     2670(* Combine the above results to show that the pc of a normal instruction
     2671   execution state can't be repeated within a trace_any_label. *)
    28012672
    28022673lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal.
     
    28452716] qed.
    28462717
    2847 lemma soundly_step : ∀ge,s1,s2.
    2848   soundly_labelled_ge ge →
    2849   as_execute (RTLabs_status ge) s1 s2 →
    2850   soundly_labelled_state (Ras_state … s1) →
    2851   soundly_labelled_state (Ras_state … s2).
    2852 #ge #s1 #s2 #GE * #tr * #EX #NX
    2853 @(soundly_labelled_state_step … GE … EX)
    2854 qed.
     2718(* We need a similar result for call states.  We'll do this by showing that
     2719   the state following the call state is a normal instruction state and using
     2720   the previous result. *)
    28552721
    28562722lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
     
    29092775qed.
    29102776
    2911 
    2912 
    2913 (* Show call case by reduction to the next step. *)
    2914 (*
    2915 lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
    2916   as_execute (RTLabs_status ge) s1 s1' →
    2917   as_after_return (RTLabs_status ge) «s1,CL» s2 →
    2918   as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 (tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX2 tal CL2 CS3) →
    2919   ∃s3,EX,CL',CS,tal'.
    2920     tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
    2921     bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
    2922 *)
    2923 
    29242777lemma cost_labels_are_other : ∀ge,s.
    29252778  as_costed (RTLabs_status ge) s →
     
    29972850| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
    29982851] qed.
     2852
     2853(* The main part of the proof is to walk down the trace_any_label and find the
     2854   repeated call state, then show that its successor appears as well. *)
    29992855
    30002856let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
     
    30482904  ]
    30492905] qed.
     2906
     2907(* Then we can start the proof by finding the original successor state... *)
    30502908
    30512909lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
     
    31012959qed.
    31022960
     2961(* And then we get our counterpart to no_loops_in_tal for calls: *)
     2962
    31032963lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
    31042964  ∀tal:trace_any_label (RTLabs_status ge) fl after final.
     
    31162976qed.
    31172977
    3118 
     2978(* Show that if a state is soundly labelled, then so are the states following
     2979   it in a trace. *)
     2980
     2981lemma soundly_step : ∀ge,s1,s2.
     2982  soundly_labelled_ge ge →
     2983  as_execute (RTLabs_status ge) s1 s2 →
     2984  soundly_labelled_state (Ras_state … s1) →
     2985  soundly_labelled_state (Ras_state … s2).
     2986#ge #s1 #s2 #GE * #tr * #EX #NX
     2987@(soundly_labelled_state_step … GE … EX)
     2988qed.
    31192989
    31202990let rec tlr_sound ge s1 s2
     
    31463016].
    31473017
     3018(* And join everything up to show that soundly labelled states give unrepeating
     3019   traces. *)
    31483020
    31493021let rec tlr_sound_unrepeating ge
Note: See TracChangeset for help on using the changeset viewer.