Changeset 2203


Ignore:
Timestamp:
Jul 17, 2012, 6:57:40 PM (8 years ago)
Author:
campbell
Message:

A general result about simulations of executions.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/Cexec.ma

    r2176 r2203  
    551551definition clight_fullexec : fullexec io_out io_in ≝
    552552  mk_fullexec ??? clight_exec make_global make_initial_state.
     553
     554
     555(* A few lemmas about the semantics. *)
     556
     557lemma cl_step_not_final : ∀ge,s1,tr,s2.
     558  exec_step ge s1 = OK … 〈tr,s2〉 →
     559  is_final s1 = None ?.
     560#ge * //
     561#r #tr #s2 #E
     562whd in E:(??%%);
     563destruct
     564qed.
     565
     566(* If you can step in Clight, then you aren't in a final state.  Hence we can
     567   give nicer constructors for plus. *)
     568lemma cl_plus_one : ∀ge,s1,tr,s2.
     569  exec_step ge s1 = OK … 〈tr,s2〉 →
     570  plus … clight_exec ge s1 tr s2.
     571#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
     572qed.
     573
     574lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
     575    exec_step ge s1 = OK … 〈tr,s2〉 →
     576    plus … clight_exec ge s2 tr' s3 →
     577    plus … clight_exec ge s1 (tr⧺tr') s3.
     578#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
     579qed.
     580

  • src/Clight/labelSimulation.ma

    r2202 r2203  
    314314.
    315315
    316 (* TODO: this (or something like it) ought to be elsewhere. *)
    317 inductive plus (ge:genv) : state → trace → state → Prop ≝
    318 | plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
    319 | plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
    320 
    321316(* Some details are invariant under labelling. *)
    322317lemma label_function_return : ∀f.
    … …  
    653648  state_with_labels_partial s1 s1' →
    654649  exec_step ge s1 = Value … 〈tr,s2〉 →
    655    ∃tr',s2'. plus ge' s1' tr' s2' ∧
     650   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    656651             trace_with_extra_labels tr tr' ∧
    657652             state_with_labels s2 s2'.
    … …  
    669664      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    670665      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
    671         % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
     666        % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    672667        | // ] | /3/ ]
    673668      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    … …  
    676671      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
    677672      whd in EX:(??%%); destruct
    678       % [ % [ @plus_one @refl | // ] | /3/ ]
     673      % [ % [ @cl_plus_one @refl | // ] | /3/ ]
    679674    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    680675      whd in EX:(??%%); destruct
    681       % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
     676      % [ 2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
    682677    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    683678      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
    … …  
    685680      normalize in EXbrem; destruct
    686681      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
    687       [ % [ 2: % [ 2: % [ % [ @plus_one
     682      [ % [ 2: % [ 2: % [ % [ @cl_plus_one
    688683        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    689684        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
    … …  
    691686        | // ]
    692687        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
    693       | % [ 2: % [ 2: % [ % [ @plus_succ [
     688      | % [ 2: % [ 2: % [ % [ @cl_plus_succ [
    694689        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    695690           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
    696691           whd in ⊢ (??%?); @refl
    697692        | skip | skip
    698         | 5: @plus_succ [ 4: @refl | skip | skip
    699         | 5: @plus_one @refl | skip ] | skip ]
     693        | 5: @cl_plus_succ [ 4: @refl | skip | skip
     694        | 5: @cl_plus_one @refl | skip ] | skip ]
    700695        | <(E0_right tr) @twel_app /2/ ]
    701696        | /3/ ] | skip ] | skip ]
    … …  
    703698    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    704699      whd in EX:(??%?); destruct
    705       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     700      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]
    706701    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    707702      whd in EX:(??%?); destruct
    708       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     703      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    709704    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    710705      whd in EX:(??%?); destruct
    711       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     706      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    712707    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    713708      whd in EX:(??%?); destruct
    714       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     709      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    715710    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    716711      whd in EX:(??%?);
    717712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    718713      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
    719         %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
     714        %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    720715        @refl | // ] | /4/ ] | skip ]
    721716      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    722717      ]
    723718    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    724       % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
     719      % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ]| skip ]| skip ]
    725720    ]
    726721  | * #a1 #ty1 #a2 #EX
    … …  
    734729    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
    735730    % [2: % [2: % [ % [
    736       @plus_one whd in ⊢ (??%?);     
     731      @cl_plus_one whd in ⊢ (??%?);     
    737732      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
    738733      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
    … …  
    757752    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
    758753    % [2,4: % [2,4: % [1,3: % [1,3:
    759       @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
     754      @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
    760755      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
    761756      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
    … …  
    766761    whd in EX:(??%%); destruct
    767762    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    768     %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
     763    %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
    769764  | #a #st1 #st2 #EX
    770765    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    … …  
    777772    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
    778773    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    779     % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
     774    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9:
    780775      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    781776      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    782777      whd in ⊢ (??%?); @refl
    783778    | 1,2,6,7: skip
    784     | 5,10: @plus_one @refl
     779    | 5,10: @cl_plus_one @refl
    785780    | *: skip
    786781    ]
    … …  
    797792    >shift_fst
    798793    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    799     % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
    800       | 5,10: @plus_succ [ 4,9:
     794    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
     795      | 5,10: @cl_plus_succ [ 4,9:
    801796      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    802797      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    803798      whd in ⊢ (??%?); @refl
    804799    | 1,2,6,7: skip
    805     | 5: @plus_one @refl
    806     | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     800    | 5: @cl_plus_one @refl
     801    | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    807802    | *: skip
    808803    ]
    … …  
    815810    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
    816811    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
    817     % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
    818       | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
     812    % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip
     813      | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ]
    819814      | /2/ ] | /4/ ] | skip ] | skip ]
    820815  | #st1 #a #st2 #st #EX
    … …  
    829824      normalize in EX; destruct
    830825      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    831       % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
    832       | 5,10: @plus_succ [ 4,9:
     826      % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
     827      | 5,10: @cl_plus_succ [ 4,9:
    833828      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    834829      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    835830      whd in ⊢ (??%?); @refl
    836831      | 1,2,6,7: skip
    837       | 5: @plus_one @refl
    838       | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     832      | 5: @cl_plus_one @refl
     833      | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    839834      | *: skip
    840835      ]
    … …  
    842837      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
    843838    | whd in EX:(??%%); destruct
    844       % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
     839      % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one
    845840        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
    846841        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
    … …  
    861856    whd in match (label_statement ??);
    862857    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
    863     [1,11,13: @plus_one @refl | 2,12,14: //
    864     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    865     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    866     | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
    867     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    868     ]| *: /3/ ]|*: skip]|*: skip ]
     858    [1,11,13: @cl_plus_one @refl | 2,12,14: //
     859    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     860    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     861    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/
     862    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     863    ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ]
    869864  | #EX inversion KL
    870865    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    … …  
    881876    whd in match (label_statement ??);
    882877    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
    883       [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
     878      [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ]
    884879      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
    885880    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    … …  
    887882      normalize in EX; destruct
    888883      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
    889       % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
     884      % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5:
    890885        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    891886      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    892887      whd in ⊢ (??%?); @refl
    893       | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     888      | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    894889      | // | <(E0_right tr) @twel_app /2/
    895890      ]
    … …  
    911906    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
    912907    whd in EX:(??%%); destruct
    913     % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
     908    % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one
    914909      whd in ⊢ (??%?);
    915910      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
    … …  
    927922    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    928923    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    929     % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
     924    % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
    930925      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
    931926      ]|skip ]| skip ]
    … …  
    934929    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
    935930    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
    936     %[2: %[2: %[ %[ @plus_succ
    937       [ 4: @refl | 5: @plus_one @refl | *: skip ]
     931    %[2: %[2: %[ %[ @cl_plus_succ
     932      [ 4: @refl | 5: @cl_plus_one @refl | *: skip ]
    938933      | /2/ ] | /3/ ] |skip ]| skip ]
    939934  | #l #EX
    … …  
    946941      cases (label_find_label_fn … KL F)
    947942      #u' * #cs * #k1' * #F' #K'
    948       % [2: %[2: %[ %[ @plus_succ
    949         [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
     943      % [2: %[2: %[ %[ @cl_plus_succ
     944        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ]
    950945        | /2/ ] | /3/ ] | skip ] | skip ]
    951946    ]
    952947  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    953     % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
     948    % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
    954949  ]
    955950| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    … …  
    959954  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    960955  [ % [2: % [2: % [ % [
    961     @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     956    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    962957                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    963                |5: @plus_one @refl | *: skip ]
    964     | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
     958               |5: @cl_plus_one @refl | *: skip ]
     959    | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ]
    965960  | % [2: % [2: % [ % [
    966     @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     961    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    967962                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    968     | 5: @plus_succ [4: @refl
    969     | 5: @plus_one @refl | *: skip ] | *: skip ]
     963    | 5: @cl_plus_succ [4: @refl
     964    | 5: @cl_plus_one @refl | *: skip ] | *: skip ]
    970965    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
    971966  ]
    … …  
    973968  whd in EX:(??%%); destruct
    974969  % [2: % [2: % [ % [
    975     @plus_succ [4: % | 5: @plus_one % | *: skip ]
     970    @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
    976971    | /2/ ]| /4/ ]| skip ]| skip ]
    977972| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
    … …  
    981976  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
    982977  [ % [2: % [2: % [ % [
    983     @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     978    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    984979                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    985     | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
     980    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl
    986981    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
    987982  | % [2: % [2: % [ % [
    988     @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     983    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    989984                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    990     | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
    991     | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
     985    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl
     986    | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
    992987    ]
    993988  ]
    … …  
    1000995    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
    1001996    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
    1002     % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
     997    % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
    1003998      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
    1004     | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
     999    | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
    10051000  | #id #tys #ty #args #k #k' #m #K #EX
    10061001    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
    … …  
    10131008    | *: normalize #A try #B try #C destruct
    10141009    ]
    1015     % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
     1010    % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
    10161011  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
    10171012    [ #EX whd in EX:(??%?); destruct
    1018       % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
     1013      % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
    10191014    | * * #b #o #ty #EX
    10201015      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
    10211016      whd in EX:(??%%); destruct
    1022       % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
     1017      % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
    10231018    ]
    10241019  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
    … …  
    10341029  state_with_labels s1 s1' →
    10351030  (exec_step ge s1 = Value … 〈tr,s2〉 →
    1036    ∃tr',s2'. plus ge' s1' tr' s2' ∧
     1031   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    10371032             trace_with_extra_labels tr tr' ∧
    10381033             state_with_labels s2 s2').
    … …  
    10481043    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    10491044    #tr' * #s2' * * #P #T #S
    1050     % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
     1045    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
    10511046(* but for LScase it's just like the cases in step_with_labels_partial *)
    10521047  | #sz #i #s #ls #k #k' #e #m #K #EX
    … …  
    10551050    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
    10561051    whd in EX:(??%?); destruct
    1057     % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
     1052    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
    10581053  ]   
    10591054] qed.
    … …  
    11881183
    11891184
    1190 lemma not_wrong_init : ∀p.
    1191   not_wrong state (exec_inf … clight_fullexec p) →
    1192   ∃s. make_initial_state … p = OK ? s.
    1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
    1194 cases (make_initial_state p)
    1195 [ /2/
    1196 | normalize #m #NW @⊥
    1197   inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
    1198 ] qed.
    11991185
    12001186lemma final_related : ∀s1,s2.
    … …  
    12041190[ #s1y #s2y * //
    12051191| //
    1206 ] qed.
    1207 
    1208 lemma plus_not_final : ∀ge,s,tr,s'.
    1209   plus ge s tr s' →
    1210   is_final s = None ?.
    1211 #ge #s0 #tr0 #s0' *
    1212 [ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
    1213 lapply (refl ? (is_final s1))
    1214 cases (is_final s1) in ⊢ (???% → %);
    1215 //
    1216 #r cases s1 in EX ⊢ %;
    1217 #H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
    1218 [ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
    1219 destruct
    1220 normalize in H10;
    1221 destruct
    1222 qed.
    1223 
    1224 lemma plus_exec : ∀ge,s,tr,s'.
    1225   plus ge s tr s' →
    1226   is_final s' = None ? →
    1227   steps state tr
    1228     (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1229     (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
    1230 #ge #s0 #tr0 #s0' #P elim P
    1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
    1232   whd in ⊢ (???%?);
    1233   whd in match (is_final ?????); >NF
    1234   %2
    1235 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
    1236   >exec_inf_aux_unfold >EX1
    1237   whd in ⊢ (???%?);
    1238   whd in match (is_final ?????); >(plus_not_final … P2)
    1239   %3 @IH //
    1240 ] qed.
    1241 
    1242 lemma plus_exec_final : ∀ge,s,tr,s',r.
    1243   plus ge s tr s' →
    1244   is_final s' = Some ? r →
    1245   ∃tr'. steps state tr
    1246           (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1247           (e_stop … tr' r s').
    1248 #ge #s0 #tr0 #s0' #r #P elim P
    1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
    1250   %{tr} whd in ⊢ (???%?);
    1251   whd in match (is_final ?????); >F
    1252   %1
    1253 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
    1254   cases (IH … F)
    1255   #tr' #S' %{tr'}
    1256   >exec_inf_aux_unfold >EX1
    1257   whd in ⊢ (???%?);
    1258   whd in match (is_final ?????); >(plus_not_final … P2)
    1259   %3 @S'
    12601192] qed.
    12611193
    … …  
    12781210  #tr2 * #s2' * * #PL #TWL #S'
    12791211  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
    1280   cases (plus_exec_final ????? PL F2)
     1212  cases (plus_final … clight_fullexec … PL F2)
    12811213  #tr2' #S2
    12821214  @(swl_stop … S2 TWL)
    … …  
    12861218  cases (step_with_labels … RG … S EX1)
    12871219  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
    1288   @(swl_steps … (plus_exec … EX2 ?))
    1289   [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
     1220  @(swl_steps … (plus_exec … clight_fullexec … EX2 ?))
     1221  [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
    12901222  | //
    12911223  | (* Manual rewrite to prevent guardedness condition getting upset. *)
    … …  
    13301262#p
    13311263#NW
    1332 cases (not_wrong_init p NW)
    1333 #s1 #I1
     1264cases (not_wrong_init clight_fullexec p NW)
     1265whd in ⊢ (% → ??%? → ?); #s1 #I1
    13341266cases (initial_state_in_simulation … I1)
    13351267#s2 * #I2

  • src/common/Executions.ma

    r2202 r2203  
    1111| steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'.
    1212
     13(* Go from individual steps to part of an execution trace. *)
     14lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'.
     15  plus … FE gl s tr s' →
     16  is_final … FE gl s' = None ? →
     17  steps (state … gl) tr
     18    (exec_inf_aux … FE gl (step … FE gl s))
     19    (exec_inf_aux … FE gl (step … FE gl s')).
     20#FE #gl #s0 #tr0 #s0' #P elim P
     21[ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold
     22  whd in ⊢ (???%?); >NF2
     23  %2
     24| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3
     25  >EX1 >exec_inf_aux_unfold
     26  whd in ⊢ (???%?); >(plus_not_final … P2) /3/
     27] qed.
     28
     29lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r.
     30  plus … FE gl s tr s' →
     31  is_final … FE gl s' = Some ? r →
     32  ∃tr'. steps (state … gl) tr
     33    (exec_inf_aux … FE gl (step … FE gl s))
     34    (e_stop … tr' r s').
     35#FE #gl #s0 #tr0 #s0' #r #P elim P
     36[ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold
     37  whd in ⊢ (??(λ_.???%?)); >F2
     38  %{tr} %1
     39| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3
     40  >EX1 >exec_inf_aux_unfold
     41  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
     42  cases (IH F3) #tr'' #S' %{tr''} /2/
     43] qed.
     44
    1345(* In some places we do not consider wrong executions. *)
    1446
    … …  
    1850| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).
    1951
     52lemma not_wrong_not_wrong : ∀state,m.
     53  ¬ (not_wrong state (e_wrong … m)).
     54#state #m % #NW inversion NW
     55#A #B #C #D #E destruct
     56qed.
     57
     58lemma not_wrong_steps : ∀state,e,e',tr.
     59  steps state tr e e' →
     60  not_wrong state e →
     61  not_wrong state e'.
     62#state #e0 #e0' #tr0 #S elim S
     63[ //
     64| #tr #s #e #NW inversion NW
     65  #A #B #C #D #E try #F destruct //
     66| #tr #s #e #tr' #e' #S' #IH #NW @IH
     67  inversion NW
     68  #A #B #C #D #E try #F destruct //
     69] qed.
     70
     71lemma not_wrong_init : ∀FE,p.
     72  not_wrong ? (exec_inf … FE p) →
     73  ∃s. make_initial_state … p = OK ? s.
     74#FE #p whd in ⊢ (??% → ?);
     75cases (make_initial_state ??? p)
     76[ /2/
     77| normalize #m #NW @⊥
     78  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
     79] qed.
     80
     81
    2082(* One execution is simulated by another, but possibly using a different number
    21    of steps. *)
     83   of steps.  Note that we have to allow for several steps at the end to make
     84   the trace match up. *)
    2285
    23 coinductive simulates (state:Type[0]) : execution state io_out io_in → execution state io_out io_in → Prop ≝
    24 | sim_stop : ∀tr,tr',r,s1,s2,e1,e2.
    25     steps state tr e1 (e_stop … tr' r s1) →
    26     steps state tr e2 (e_stop … tr' r s2) →
    27     simulates state e1 e2
     86coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
     87| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
     88    steps S1 tr e1 (e_stop … tr1 r s1) →
     89    steps S2 tr e2 (e_stop … tr2 r s2) →
     90    simulates S1 S2 e1 e2
    2891| sim_steps : ∀tr,e1,e1',e2,e2'.
    29     steps state tr e1 e1' →
    30     steps state tr e2 e2' →
    31     simulates state e1' e2' →
    32     simulates state e1 e2
     92    steps S1 tr e1 e1' →
     93    steps S2 tr e2 e2' →
     94    simulates S1 S2 e1' e2' →
     95    simulates S1 S2 e1 e2
    3396| sim_interact : ∀o,k1,k2.
    34     (∀i. simulates state (k1 i) (k2 i)) →
    35     simulates state (e_interact … o k1) (e_interact … o k2).
     97    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
     98    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).
    3699
     100
     101(* Result for lifting simulations on states to simulations on execution traces.
     102   At the time of writing this hasn't been used in anger yet...
     103   
     104   This probably isn't the best route for the stages of the compiler that have
     105   results in terms of structured traces, but it should be good for the
     106   front-end.
     107 *)
     108
     109let corec build_cofix_simulation
     110  (FS1,FS2:fullexec io_out io_in)
     111  (g1:global … FS1) (g2:global … FS2)
     112  (SIM:state … g1 → state … g2 → Prop)
     113  (s1:state … g1) (s2:state … g2)
     114  (NF:is_final … FS1 g1 s1 = None ?)
     115  (S:SIM s1 s2)
     116  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
     117  (SIM_GOOD: ∀x,y. SIM x y →
     118         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
     119         is_final … FS1 g1 x = None ? →
     120         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
     121  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
     122: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
     123lapply (SIM_GOOD … S NW NF)
     124* #tr * #s1' * #s2' * #P1 * #P2 #S'
     125lapply (refl ? (is_final … FS1 g1 s1'))
     126cases (is_final … s1') in ⊢ (???% → ?);
     127[ #NF1
     128  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
     129  [ @(plus_exec … P1) //
     130  | @(plus_exec … P2) <SIM_FINAL //
     131  | @(not_wrong_steps … (plus_exec … P1 …)) //
     132  | //
     133  ]
     134| #r #F1
     135  cases (plus_final … P1 F1) #tr1' #S1
     136  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
     137  @(sim_stop … S1 S2)
     138] qed.
     139
     140theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
     141  ∀p1:program … FE1.  ∀p2:program … FE2.
     142  let g1 ≝ make_global … p1 in
     143  let g2 ≝ make_global … p2 in
     144  ∀SIM: state … g1 → state … g2 → Prop.
     145  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
     146             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
     147  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
     148  ∀SIM_GOOD: ∀x,y. SIM x y →
     149         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
     150         is_final … FE1 g1 x = None ? →
     151         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
     152  let e1 ≝ exec_inf … FE1 p1 in
     153  let e2 ≝ exec_inf … FE2 p2 in
     154  not_wrong … e1 →
     155  simulates … e1 e2.
     156
     157#FE1 #FE2 #p1 #p2
     158letin g1 ≝ (make_global … p1)
     159letin g2 ≝ (make_global … p2)
     160#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
     161#NW
     162cases (not_wrong_init … p1 NW)
     163#s1 #I1
     164cases (SIM_INIT … I1) #s2 * #I2 #S
     165whd in NW:(??%) ⊢ (???%%);
     166>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
     167change with g1 in match (make_global … p1);
     168change with g2 in match (make_global … p2);
     169
     170>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
     171lapply (SIM_FINAL … S)
     172lapply (refl ? (is_final … s1))
     173cases (is_final … s1) in ⊢ (???% → %);
     174[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
     175  <F2 whd in ⊢ (? → ???%%); #NW
     176  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
     177  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
     178| #r #F1 #F2 #NW whd in ⊢ (???%%);
     179  >exec_inf_aux_unfold whd in ⊢ (???%%);
     180  <F2 whd in ⊢ (???%%);
     181  @(sim_stop … (steps_stop …) (steps_stop …))
     182] qed.
     183

  • src/common/SmallstepExec.ma

    r2202 r2203  
    1919         repeat n' ?? exec g s1
    2020].
     21
     22(* We take care here to check that we're not at the final state.  It is not
     23   necessarily the case that a success step guarantees this (e.g., because
     24   there may be no way to stop a processor, so an infinite loop is used
     25   instead). *)
     26inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
     27| plus_one : ∀s1,tr,s2.
     28    is_final … TS ge s1 = None ? →
     29    step … TS ge s1 = OK … 〈tr,s2〉 →
     30    plus … ge s1 tr s2
     31| plus_succ : ∀s1,tr,s2,tr',s3.
     32    is_final … TS ge s1 = None ? →
     33    step … TS ge s1 = OK … 〈tr,s2〉 →
     34    plus … ge s2 tr' s3 →
     35    plus … ge s1 (tr⧺tr') s3.
     36
     37lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
     38  plus O I FE gl s tr s' →
     39  is_final … FE gl s = None ?.
     40#O #I #FE #gl #s0 #tr0 #s0' * //
     41qed.
    2142
    2243let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
Note: See TracChangeset for help on using the changeset viewer.