Changeset 2338 for src/Clight


Ignore:
Timestamp:
Sep 26, 2012, 10:17:32 AM (7 years ago)
Author:
campbell
Message:

Use much nicer definition for making several steps in the labelling
simulation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2319 r2338  
    648648  state_with_labels_partial s1 s1' →
    649649  exec_step ge s1 = Value … 〈tr,s2〉 →
    650    ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    651              trace_with_extra_labels tr tr' ∧
    652              state_with_labels s2 s2'.
     650  ∃n. after_n_steps (S n) … clight_exec ge' s1'
     651  (λtr',s2'.
     652     trace_with_extra_labels tr tr' ∧
     653     state_with_labels s2 s2').
    653654
    654655(* General plan is like the expressions result, except that we do case analysis
     
    660661[ #g #f #us #s #k #k' #e #m #KL cases s
    661662  [ #EX inversion KL
    662     [ #E1 #E2 #_ destruct %{tr}
     663    [ #E1 #E2 #_ destruct
    663664      whd in EX:(??%?);
    664665      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    665       [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
    666         % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    667         | // ] | /3/ ]
     666      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct
     667        %{0} whd whd in ⊢ (??%?);
     668        >label_function_return >E whd % /3/
    668669      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    669670      ]
    670     | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    671       %{(State (\fst (label_function g f)) (\fst (label_statement s0 u)) k0' e m)}
    672       whd in EX:(??%%); destruct
    673       % [ % [ @cl_plus_one @refl | // ] | /3/ ]
    674     | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    675       whd in EX:(??%%); destruct
    676       % [ 2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
     671    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
     672      whd in EX:(??%%); destruct /4/
     673    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0}
     674      whd in EX:(??%%); destruct whd /4/
    677675    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    678       cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
    679       cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
    680       normalize in EXbrem; destruct
     676      cases (bindIO_inversion ??????? EX) -EX * #ve #tre * #EXe #EX
     677      cases (bindIO_inversion ??????? EX) -EX * * #EXb #EX
     678      normalize in EX; destruct
    681679      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
    682       [ % [ 2: % [ 2: % [ % [ @cl_plus_one
    683         whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    684         whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
    685         whd in ⊢ (??%?); @refl
    686         | // ]
    687         | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
    688       | % [ 2: % [ 2: % [ % [ @cl_plus_succ [
    689         4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    690            whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
    691            whd in ⊢ (??%?); @refl
    692         | skip | skip
    693         | 5: @cl_plus_succ [ 4: @refl | skip | skip
    694         | 5: @cl_plus_one @refl | skip ] | skip ]
    695         | <(E0_right tr) @twel_app /2/ ]
    696         | /3/ ] | skip ] | skip ]
     680      [ %{0} whd
     681        whd in ⊢ (??%?); >EXe'
     682        whd in ⊢ (??%?); >label_expr_type >EXb
     683        whd % /4/
     684      | %{2} whd
     685        whd in ⊢ (??%?); >EXe'
     686        whd in ⊢ (??%?); >label_expr_type >EXb
     687        whd % [ <(E0_right tr) @twel_app /2/ | /4/ ]
    697688      ]
    698689    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    699690      whd in EX:(??%?); destruct
    700       %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]
     691      %{0} whd /4/
    701692    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    702693      whd in EX:(??%?); destruct
    703       %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
     694      %{0} % /4/
    704695    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    705696      whd in EX:(??%?); destruct
    706       %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
     697      %{0} % /4/
    707698    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    708699      whd in EX:(??%?); destruct
    709       %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
     700      %{0} % /4/
    710701    | #u0 #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    711702      whd in EX:(??%?);
    712703      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    713704      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
    714         %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    715         @refl | // ] | /4/ ] | skip ]
     705        %{0} whd whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
     706        whd % /4/
    716707      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    717708      ]
    718709    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    719       % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ]| skip ]| skip ]
     710      %{0} % /4/
    720711    ]
    721712  | * #a1 #ty1 #a2 #EX
     
    724715    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
    725716    whd in EX:(??%%); destruct
    726     cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
    727     whd in match (label_statement ??);
    728     @label_gen_elim #ua1 @label_gen_elim #ua2
    729     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
    730     % [2: % [2: % [ % [
    731       @cl_plus_one whd in ⊢ (??%?);     
    732       >exec_lvalue_labelled >EX1' in ⊢ (??%?);
    733       whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
    734       whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
    735       @refl
    736     | @twel_app // ] | /3/ ] | skip ] | skip ]
     717    @blindly_label #u1 #u2
     718    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 u1) #tr1' * #EX1' #T1
     719    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 u2) #tr2' * #EX2' #T2
     720    %{0} whd
     721    whd in ⊢ (??%?); >exec_lvalue_labelled >EX1'
     722    whd in ⊢ (??%?); >EX2'
     723    whd in ⊢ (??%?); >label_expr_type >EX3
     724    whd % [ whd in ⊢ (??%); @twel_app // | /3/ ]
    737725  | * [2: * #er #tyr ] #ef #args #EX
    738726    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    743731    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
    744732    destruct
    745     whd in match (label_statement ??);
    746     whd in match (label_opt_expr ??);
    747     [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
    748     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
    749     @label_gen_elim #u1
    750     @label_gen_elim #u2
    751     cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
    752     [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
    753       cases (opt_find_funct … RG … EX3) #ux #EFF
    754       % [2,4: % [2,4: % [1,3: % [1,3:
    755       @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
    756       whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
    757       whd in ⊢ (??%?); [ >EFF in ⊢ (??%?); | >EFF in ⊢ (??%?); ]
    758       whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
    759       whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
    760       whd in ⊢ (??%?);
    761       @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
     733    @blindly_label #u1 #u2 #u3
     734    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1
     735    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u3) #tr2' * #EX2' #T2
     736    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 u1) #tr5' * #EX5' #T5 ]
     737    cases (opt_find_funct … RG … EX3) #ux #EFF
     738    %{0} whd
     739    whd in ⊢ (??%?); >EX1'
     740    whd in ⊢ (??%?); >EX2'
     741    whd in ⊢ (??%?); >EFF
     742    whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof >EX4
     743    whd in ⊢ (??%?); [ whd in match (label_opt_expr ??); @breakup_pair whd in ⊢ (??%?); >exec_lvalue_labelled >EX5' ]
     744    whd % [ 1,3: whd in ⊢ (??%); @twel_app /2/ | *: @swl_partial @swl_callstate /2/ ]
    762745  | #st1 #st2 #EX
    763746    whd in EX:(??%%); destruct
    764747    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    765     %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
     748    %{0} % /4/
    766749  | #a #st1 #st2 #EX
    767750    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    774757    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
    775758    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    776     % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9:
    777       whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    778       whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    779       whd in ⊢ (??%?); @refl
    780     | 1,2,6,7: skip
    781     | 5,10: @cl_plus_one @refl
    782     | *: skip
    783     ]
    784     | 2,4: <(E0_right tr) @twel_app /2/
    785     ]| 2,4: /3/ ] | *: skip ] | *: skip ]
     759    %{1} whd
     760    whd in ⊢ (??%?); >EX1'
     761    whd in ⊢ (??%?); >label_expr_type >EX2
     762    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
    786763  | #a #st #EX
    787764    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    794771    >shift_fst
    795772    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    796     % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
    797       | 5,10: @cl_plus_succ [ 4,9:
    798       whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    799       whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    800       whd in ⊢ (??%?); @refl
    801     | 1,2,6,7: skip
    802     | 5: @cl_plus_one @refl
    803     | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    804     | *: skip
    805     ]
    806     | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
    807     ]| 2,4: /4/ ] | *: skip ] | *: skip ]
     773    [ %{2} | %{3} ] whd
     774    whd in ⊢ (??%?); >EX1'
     775    whd in ⊢ (??%?); >label_expr_type >EX2
     776    whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/
    808777  | #a #st #EX
    809778    normalize in EX; destruct
     
    812781    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
    813782    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
    814     % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip
    815       | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ]
    816       | /2/ ] | /4/ ] | skip ] | skip ]
     783    %{2} % /4/
    817784  | #st1 #a #st2 #st #EX
    818785    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
     
    826793      normalize in EX; destruct
    827794      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    828       % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
    829       | 5,10: @cl_plus_succ [ 4,9:
    830       whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    831       whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    832       whd in ⊢ (??%?); @refl
    833       | 1,2,6,7: skip
    834       | 5: @cl_plus_one @refl
    835       | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    836       | *: skip
    837       ]
    838       | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
    839       ]| 2,4: /4/ ] | *: skip ] | *: skip ]
     795      [ %{2} | %{3} ] whd
     796      whd in ⊢ (??%?); >EX1'
     797      whd in ⊢ (??%?); >label_expr_type >EX2
     798      whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/
    840799    | whd in EX:(??%%); destruct
    841       % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one
    842         whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
    843         >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
    844       | skip ] | skip ]
     800      %{1} whd
     801      whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
     802      >Eskip' whd in ⊢ (??%?); % /4/
    845803    ]
    846804  | #EX inversion KL
     
    857815    ]
    858816    whd in match (label_statement ??);
    859     % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
    860     [1,11,13: @cl_plus_one @refl | 2,12,14: //
    861     | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
    862     | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
    863     | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/
    864     | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
    865     ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ]
     817    [ 1,6,7: %{0} % /3/
     818    | 2,3,5: %{2} % /3/
     819    | %{1} % /3/
     820    ]
    866821  | #EX inversion KL
    867822    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    877832    ]
    878833    whd in match (label_statement ??);
    879     [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
    880       [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ]
    881       | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
     834    [ 1,2,5,6,7: %{0} % /4/
     835    | 4: %{1} % /4/
    882836    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    883837      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    884838      normalize in EX; destruct
    885839      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
    886       % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5:
    887         whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    888       whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    889       whd in ⊢ (??%?); @refl
    890       | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    891       | // | <(E0_right tr) @twel_app /2/
    892       ]
    893       | /3/ | /3/ ] | *: skip ] | *: skip ]
     840      [ %{0} | %{2} ] whd
     841      whd in ⊢ (??%?); >EX1'
     842      whd in ⊢ (??%?); >label_expr_type >EX2
     843      whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/
    894844    ]
    895845  | * [2: #a ] #EX
     
    908858    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
    909859    whd in EX:(??%%); destruct
    910     % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one
    911       whd in ⊢ (??%?);
    912       [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
    913         whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    914       | >label_function_return >Ety in ⊢ (??%?);
    915       ] whd in ⊢ (??%?); @refl
    916       | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
     860    %{0} whd
     861    whd in ⊢ (??%?);
     862    [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
     863      whd in ⊢ (??%?); >EX1'
     864    | >label_function_return >Ety
     865    ] whd in ⊢ (??%?); % /4/
    917866  | #a #ls #EX
    918867    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    924873    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    925874    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    926     % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
    927       | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
    928       ]|skip ]| skip ]
     875    %{0} whd
     876    whd in ⊢ (??%?); >EX1' % //
     877    cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
    929878  | #l #st #EX
    930879    whd in EX:(??%?); destruct
    931880    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
    932881    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
    933     %[2: %[2: %[ %[ @cl_plus_succ
    934       [ 4: @refl | 5: @cl_plus_one @refl | *: skip ]
    935       | /2/ ] | /3/ ] |skip ]| skip ]
     882    %{1} % /3/
    936883  | #l #EX
    937884    whd in EX:(??%?);
     
    943890      cases (label_find_label_fn g … KL F)
    944891      #u' * #cs * #k1' * #F' #K'
    945       % [2: %[2: %[ %[ @cl_plus_succ
    946         [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ]
    947         | /2/ ] | /3/ ] | skip ] | skip ]
     892      %{1} whd
     893      whd in ⊢ (??%?); >F'
     894      % /3/
    948895    ]
    949896  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    950     % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
     897    %{0} % /3/
    951898  ]
    952899| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     
    955902  whd in EX:(??%%); destruct
    956903  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    957   [ % [2: % [2: % [ % [
    958     @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    959                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    960                |5: @cl_plus_one @refl | *: skip ]
    961     | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ]
    962   | % [2: % [2: % [ % [
    963     @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    964                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    965     | 5: @cl_plus_succ [4: @refl
    966     | 5: @cl_plus_one @refl | *: skip ] | *: skip ]
    967     | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
    968   ]
     904  [ %{1} | %{2} ] whd
     905  whd in ⊢ (??%?); >EX1'
     906  whd in ⊢ (??%?); >label_expr_type >EX2
     907  % [ 1,3: <(E0_right tr) ] /4/
    969908| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    970909  whd in EX:(??%%); destruct
    971   % [2: % [2: % [ % [
    972     @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
    973     | /2/ ]| /4/ ]| skip ]| skip ]
     910  %{1} % /4/
    974911| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
    975912  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    977914  whd in EX:(??%%); destruct
    978915  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
    979   [ % [2: % [2: % [ % [
    980     @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    981                     whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    982     | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl
    983     | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
    984   | % [2: % [2: % [ % [
    985     @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    986                     whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    987     | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl
    988     | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
    989     ]
    990   ]
     916  [ %{1} | %{2} ] whd
     917  whd in ⊢ (??%?); >EX1'
     918  whd in ⊢ (??%?); >label_expr_type >EX2
     919  % [1,3: <(E0_right tr) ] /4/
    991920| #u0 *
    992921  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
     
    997926    lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?);
    998927    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
    999     % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
    1000       whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
    1001     | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
     928    %{1} whd
     929    whd in ⊢ (??%?); >EX1
     930    whd in ⊢ (??%?); >EX2
     931    % /4/
    1002932  | #id #tys #ty #args #k #k' #m #K #EX
    1003933    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
     
    1010940    | *: normalize #A try #B try #C destruct
    1011941    ]
    1012     % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
     942    %{0} % /2/
    1013943  | 9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
    1014944    [ #EX whd in EX:(??%?); destruct
    1015       % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
     945      %{0} % /3/
    1016946    | * * #b #o #ty #EX
    1017947      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
    1018948      whd in EX:(??%%); destruct
    1019       % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
     949      %{0} whd whd in ⊢ (??%?); >EX1 % /3/
    1020950    ]
    1021951  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
     
    1024954| #r #EX whd in EX:(??%%); destruct
    1025955] qed.
    1026 
    1027956
    1028957theorem step_with_labels : ∀ge,ge'.
     
    1030959  ∀s1,s1',tr,s2.
    1031960  state_with_labels s1 s1' →
    1032   (exec_step ge s1 = Value … 〈tr,s2〉 →
    1033    ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    1034              trace_with_extra_labels tr tr' ∧
    1035              state_with_labels s2 s2').
     961  exec_step ge s1 = Value … 〈tr,s2〉 →
     962   ∃n. after_n_steps (S n) … clight_exec ge' s1'
     963   (λtr',s2'. trace_with_extra_labels tr tr' ∧
     964              state_with_labels s2 s2').
    1036965#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
    1037966[ #s1 #s1' @step_with_labels_partial //
     
    1044973    >shift_fst whd in match (seq_of_labeled_statement ?);
    1045974    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    1046     #tr' * #s2' * * #P #T #S
    1047     % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
     975    #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
     976    #trx #sx * /3/
    1048977(* but for LScase it's just like the cases in step_with_labels_partial *)
    1049978  | #sz #i #s #ls #k #k' #e #m #K #EX
     
    1052981    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
    1053982    whd in EX:(??%?); destruct
    1054     % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
     983    %{1} % /4/
    1055984  ]   
    1056985] qed.
     
    12111140  #EX1 #F1
    12121141  cases (step_with_labels … RG … S EX1)
    1213   #tr2 * #s2' * * #PL #TWL #S'
     1142  #n #A cases (after_inv clight_fullexec ???? A) #tr' * #s' * * #TWL #S'
    12141143  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
    1215   cases (plus_final … clight_fullexec … PL F2)
     1144  whd in match (is_final … s'); >F2 *
    12161145  #tr2' #S2
    12171146  @(swl_stop … S2 TWL)
     
    12201149  #EX1 #E1'
    12211150  cases (step_with_labels … RG … S EX1)
    1222   #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
    1223   @(swl_steps … (plus_exec … clight_fullexec … EX2 ?))
    1224   [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
    1225   | //
    1226   | (* Manual rewrite to prevent guardedness condition getting upset. *)
     1151  #n #AF cases (after_inv clight_fullexec ???? AF) #tr' * #s' * * #TWL #S'
     1152  whd in match (is_final … s'); lapply (refl ? (is_final s'))
     1153  cases (is_final s') in ⊢ (???% → %);
     1154  [ #NF #H whd in H; @(swl_steps … H) //
    12271155    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
    12281156    @build_exec // >E1' in NW1; //
     1157  | #r <(final_related … S') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
     1158    >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct
    12291159  ]
    12301160| #E1
Note: See TracChangeset for help on using the changeset viewer.