Changeset 2338


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.

Location:
src
Files:
3 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
  • src/common/Executions.ma

    r2206 r2338  
    4141  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
    4242  cases (IH F3) #tr'' #S' %{tr''} /2/
     43] qed.
     44
     45(* And similarly for after_n_steps *)
     46
     47lemma after_inv : ∀FE:fullexec io_out io_in.
     48 ∀n,g,P,s.
     49  after_n_steps (S n) … FE g s P →
     50  ∃tr,s'.
     51    P tr s' ∧
     52    match is_final ?? FE g s' with
     53    [ Some r ⇒ ∃tr'.
     54      steps ? tr (exec_inf_aux … FE g (step … FE g s))
     55                 (e_stop ??? tr' r s')
     56    | None ⇒
     57      steps ? tr (exec_inf_aux … FE g (step … FE g s))
     58                 (exec_inf_aux … FE g (step … FE g s'))
     59    ].
     60#FE #n #g #P
     61(* Rather nasty generalisation *)
     62#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
     63cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H | skip ]
     64generalize in match E0 in AW ⊢ %; generalize in match s; -s
     65elim n
     66[ #s #tr whd in ⊢ (% → %);
     67  cases (step … s) [ #o #K * | 3: #m * ]
     68  * #tr' #s' #AW %{tr'} %{s'} %{AW}
     69  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
     70  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
     71  | #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop
     72  ]
     73| #n' #IH #s #tr whd in ⊢ (% → ?);
     74  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
     75  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
     76  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
     77  cases (IH s1 ? AW1)
     78  #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'}
     79  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
     80  [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1
     81    @steps_steps >NF in H1; //
     82  | #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1
     83    >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1}
     84    @steps_steps @H1
     85  ]
    4386] qed.
    4487
  • src/common/SmallstepExec.ma

    r2203 r2338  
    1717[ O ⇒ Value ??? 〈E0, s〉
    1818| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
    19          repeat n' ?? exec g s1
     19         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
     20         Value ??? 〈t1⧺tn,sn〉
    2021].
    2122
     
    5152].
    5253
     54(* A third version of making several steps (!)
     55
     56   The idea here is to have a computational definition of reducing serveral
     57   steps then showing some property about the resulting trace and state.  By
     58   careful use of let rec we can ensure that reduction stops in a sensible
     59   way whenever the number of steps or the step currently being executed is
     60   not (reducible to) a value.
     61
     62   For example, we state a property to prove by something like
     63
     64     ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>)
     65
     66   then start reducing by giving the number of steps and reducing the
     67   definition
     68
     69     %{3} whd
     70
     71   and then whenever the reduction gets stuck, the currently reducing step is
     72   the third subterm, which we can reduce and unblock with (for example)
     73   rewriting
     74
     75     whd in ⊢ (??%?); >EXe'
     76
     77   and at the end reduce with whd to get the property as the goal.
     78
     79   There's an inversion-like result to get back the information contained in
     80   the proof in Executions.ma.
     81
     82  *)
     83
     84record await_value_stuff : Type[2] ≝ {
     85 avs_O : Type[0];
     86 avs_I : avs_O → Type[0];
     87 avs_exec : trans_system avs_O avs_I;
     88 avs_g : global ?? avs_exec
     89}.
     90
     91let rec await_value (avs:await_value_stuff)
     92 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
     93 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
     94match v with
     95[ Value ts ⇒ P (\fst ts) (\snd ts)
     96| _ ⇒ False
     97].
     98
     99let rec after_aux (avs:await_value_stuff)
     100  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
     101  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
     102on n : Prop ≝
     103match n with
     104[ O ⇒ P tr s
     105| S n' ⇒
     106  match is_final … s with
     107  [ None ⇒
     108    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
     109      after_aux avs n' s (tr ⧺ tr') P)
     110  | _ ⇒ False
     111  ]
     112].
     113
     114definition after_n_steps : nat →
     115 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
     116 state ?? exec g →
     117 (trace → state ?? exec g → Prop) → Prop ≝
     118λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
     119
     120lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
     121  (∀tr,s. P tr s → Q tr s) →
     122  ∀s.
     123  after_n_steps n O I exec g s P →
     124  after_n_steps n O I exec g s Q.
     125#n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n
     126[ normalize /2/
     127| #n' #IH #tr #s
     128  normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/
     129] qed.
     130
     131(* for joining a couple of these together *)
     132
     133lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
     134  after_n_steps m O I exec g s' Q →
     135  after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
     136  after_n_steps (n+m) O I exec g s P.
     137#n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
     138[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
     139  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
     140  generalize in match s; -s
     141  elim m
     142  [ #s #tr' whd in ⊢ (% → %); @H2
     143  | #m' #IH #s #tr' whd in ⊢ (% → %);
     144    cases (is_final … s) [2: #r * ]
     145    whd in ⊢ (% → %);
     146    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
     147| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
     148  cases (is_final … s) [2: #r * ]
     149  whd in ⊢ (% → %);
     150  cases (step O I exec g s) [1,3: normalize // ]
     151  * #tr1 #s1 whd in ⊢ (% → %); @IH @H
     152] qed.
     153
     154
    53155(* A (possibly non-terminating) execution.   *)
    54156coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.