Changeset 3237


Ignore:
Timestamp:
Apr 30, 2013, 7:02:53 PM (4 years ago)
Author:
campbell
Message:

Some incomplete work on Clight -> Cminor call steps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3178 r3237  
    18121812qed.
    18131813
     1814lemma Zlt_to_not_Zle : ∀x,y:Z. x < y → y ≰ x.
     1815* [2,3: #p] * [2,3,5,6:#q] /2/
     1816@lt_to_not_le
     1817qed.
     1818
     1819lemma Zlt_to_Zleb_false : ∀x,y:Z. x < y → Zleb y x = false.
     1820#x #y #H
     1821lapply (Zleb_true_to_Zle y x) cases (Zleb ??) // #H'
     1822@⊥ @(absurd … (H' (refl ??)))
     1823@(Zlt_to_not_Zle … H)
     1824qed.
     1825
     1826
     1827lemma alloc_region : ∀m,l,h,m',b.
     1828  alloc m l h = 〈m',b〉 →
     1829  block_region b = XData.
     1830* #ct #n #nO  #l #h #m' #b #A whd in A:(??%%); destruct
     1831whd in ⊢ (??%?);
     1832>(Zlt_to_Zleb_false … nO) %
     1833qed.
     1834
     1835lemma alloc_other_high_bound : ∀m,l,h,m',b,b'.
     1836  b ≠ b' →
     1837  alloc m l h = 〈m',b〉 →
     1838  high_bound m b' = high_bound m' b'.
     1839* #contents #next #next_ok #l #h #m' #b #b' #NE #ALLOC
     1840whd in ALLOC:(??%%); destruct
     1841whd in ⊢ (??%%);
     1842>update_block_o //
     1843qed.
     1844
     1845lemma alloc_other_low_bound : ∀m,l,h,m',b,b'.
     1846  b ≠ b' →
     1847  alloc m l h = 〈m',b〉 →
     1848  low_bound m b' = low_bound m' b'.
     1849* #contents #next #next_ok #l #h #m' #b #b' #NE #ALLOC
     1850whd in ALLOC:(??%%); destruct
     1851whd in ⊢ (??%%);
     1852>update_block_o //
     1853qed.
     1854
     1855lemma alloc_vars_env : ∀v,L,env,m,env',m'.
     1856  All ? (λia. v ≠ \fst ia) L →
     1857  exec_alloc_variables env m L = 〈env',m'〉 →
     1858  lookup … env v = lookup … env' v.
     1859#v #L elim L
     1860[ #env #m #env' #m' #_ #A whd in A:(??%%); destruct %
     1861| * #id #ty #tl #IH
     1862  #env #m #env' #m' * #NE #D whd in ⊢ (??%% → ?);
     1863  cases (alloc ???) #m1 #b1 #A
     1864  <(IH … A)
     1865  >(lookup_add_miss … env v id) /2/
     1866] qed.
     1867
     1868lemma embedding_compatible_trans : ∀E1,E2,E3.
     1869  embedding_compatible E1 E2 →
     1870  embedding_compatible E2 E3 →
     1871  embedding_compatible E1 E3.
     1872#E1 #E2 #E3 #C1 #C2 #v
     1873cases (C1 v)
     1874[ /2/
     1875| #E >E @C2
     1876] qed.
    18141877
    18151878(* This roughly corresponds to lemma 69 of Leroy and Blazy *)
    1816 (*
     1879
    18171880lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame.
    18181881∀Em. memory_inj Em cl_m cm_m →
     
    18201883alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 →
    18211884∀L, cl_env, cl_m1.
     1885distinct_env … L →
    18221886exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 →
    18231887(∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧
     
    18351899    lookup' vartypes v = return 〈c,t〉 ∧
    18361900    match c with
    1837     [ Local ⇒ Em' b = None ?
     1901    [ Local ⇒ True (*Em' b = None ?*)
    18381902    | Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉
    18391903    | Global _ ⇒ False
    18401904    ].
    18411905#vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L
     1906(* Deal with Cminor allocation *)
    18421907cut (block_implementable_bv cm_m1 cm_frame)
    18431908[ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % //
     
    18451910lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi)
    18461911lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid
     1912
     1913(* Generalise *)
    18471914cut (∀b:block. ∀delta':offset.
    18481915    Em b=Some (block×offset) 〈cm_frame,delta'〉 →
    1849     ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 →
     1916    ∀v,off,ty.
     1917    Exists … (λx.x = 〈v,ty〉) L →
     1918    lookup' vartypes v = OK ? 〈Stack off, ty〉 →
    18501919    high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off)
    18511920      ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta')
    18521921[ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V
    18531922  @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ]
    1854 
    1855 generalize in match Em; -Em generalize in match empty_env; elim L
    1856 [ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc
     1923generalize in match Em; -Em
     1924generalize in match cl_m; -cl_m generalize in match empty_env;
     1925
     1926elim L
     1927[ #cl_env #cl_m #Em #_ #Inj #cl_env' #cl_m1 #_ #cl_alloc
    18571928  whd in cl_alloc:(??%%); destruct #H
    18581929  %{Em} % [ % [ @Inj | // ] | #v * ]
    18591930| * #v #ty #tl #IH
    1860   #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1
     1931  #cl_env #cl_m #Em #Hexisting #Inj #cl_env' #cl_m1 * #Hdistinct #Hdistinct'
    18611932  whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H
    18621933  cases (H v ty ?) [2: %1 % ] *
    18631934  [ #r * #L *
    18641935  | #off * #L * * #off_low #off_high #other
     1936    cut (off < Z_two_power_nat 16)
     1937    [ @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off))
     1938      [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/
     1939      | @(transitive_Zle … stacksize) [ <eq_plus_Zplus @le_to_Zle @off_high | /2/ ]
     1940      ]
     1941    ] #off_repr
    18651942    lapply (alloc_memory_inj_m1_to_m2 … (offset_of_Z off) cm_frame_valid … cm_bi … cl_alloc … Inj)
    1866     [ #b #delta' #NE #E @(Hexisting … E … L)
     1943    [ #b #delta' #NE #E @(Hexisting … E … L) % %
    18671944    | cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U
    18681945      [ /2/
    1869       | @(transitive_Zle … HIGH) >unZoo
    1870         [ <eq_plus_Zplus /2/
    1871         | @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off))
    1872           [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/
    1873           | @(transitive_Zlt … stacksize) [ <eq_plus_Zplus @(lt_to_Zlt … off_high) | // ]
     1946      | @(transitive_Zle … HIGH) >(unZoo … off_repr)
     1947        <eq_plus_Zplus /2/
     1948      ]
     1949    | >(unZoo … off_repr)
     1950      <eq_plus_Zplus >(alloc_high_bound … cm_alloc) @le_to_Zle @off_high
     1951    | >(alloc_low_bound … cm_alloc) //
     1952    | >(alloc_high_bound … cl_alloc) >(unZoo … off_repr)
     1953      @(Zle_to_Zlt_to_Zlt … stack_ok) <eq_plus_Zplus @le_to_Zle @off_high
     1954    | >(alloc_region … cl_alloc) >(alloc_region … cm_alloc) %
     1955    | % [ >(alloc_low_bound … cl_alloc) % //
     1956        | >(alloc_high_bound … cl_alloc) % [ @le_to_Zle // | @(Zle_to_Zlt_to_Zlt … stack_ok) @le_to_Zle /2/ ]
     1957        ]
     1958    | #Inj' lapply (IH … Inj' … cl_alloc' ?)
     1959      [ #v' #ty' #EX @(H v' ty') %2 @EX
     1960      | @Hdistinct'
     1961      | #b #delta' @eq_block_elim
     1962        [ #E1 #E2 whd in E2:(??%?); destruct #v' #off' #ty' #EX #L
     1963          cases (other … L)
     1964          [ #LE %2 >(unZoo … off_repr) >unZoo
     1965            [ >(alloc_low_bound … cl_alloc) <eq_plus_Zplus <eq_plus_Zplus @le_to_Zle >commutative_plus @LE
     1966            | @(Zle_to_Zlt_to_Zlt … off_repr) @le_to_Zle /2/
     1967            ]
     1968          | #LE %1 >(unZoo … off_repr) >unZoo
     1969            [ >(alloc_high_bound … cl_alloc) >sym_Zplus <eq_plus_Zplus <eq_plus_Zplus @le_to_Zle @LE
     1970            | cases (H v' ty')
     1971              [ #c >L * #E whd in E:(??%%); destruct
     1972                * * #_ #LE' #_
     1973                @(Zle_to_Zlt_to_Zlt … stack_ok) @le_to_Zle /2/
     1974              | %2 assumption
     1975              ]
     1976            ]
     1977          | cases (Exists_All … EX Hdistinct) * #v'' #ty'' * #E destruct //
    18741978          ]
     1979        | #NE #EM #v' #off' #ty' #EX
     1980          <(alloc_other_high_bound … NE cl_alloc) <(alloc_other_low_bound … NE cl_alloc)
     1981          @(Hexisting b delta' EM v' off' ty' ?)
     1982          %2 assumption
    18751983        ]
     1984      | * #Em' * * #Inj' #compat' #H'
     1985        %{Em'} % [ %
     1986        [ @Inj'
     1987        | #b' cases (compat' b')
     1988          [ @eq_block_elim [ #E destruct #E whd in E:(??%%); destruct
     1989            | #NE #E whd in E:(??%%); %1 @E
     1990            ]
     1991          | @eq_block_elim
     1992            [ #E destruct #_ %1 @(mi_freeblock … Inj) @(new_block_invalid_before_alloc … cl_alloc)
     1993            | #NE #E whd in E:(??%%); %2 @E
     1994            ]
     1995          ]
     1996       ]| #v' *
     1997          [ #E destruct %{cl_b} %{(Stack off)} %{ty} % [ %
     1998            [ <(alloc_vars_env … cl_alloc') // @Hdistinct
     1999            | assumption
     2000           ]| whd lapply (compat' cl_b) >eq_block_b_b *
     2001              #E whd in E:(??%%); [ destruct | <E % ]
     2002           ]
     2003          | @H'
     2004          ]
     2005       ]
     2006     ]
     2007   ]
     2008  | * #L *
     2009    cases (alloc_memory_inj_m1 … Inj cl_alloc)
     2010    #Inj2 #compat2
     2011    cases (IH … Inj2 … cl_alloc' ?)
     2012    [ #Em' * * #Inj' #compat' #H'
     2013      %{Em'} % [ %
     2014      [  @Inj'
     2015      |  /2/
     2016      ]| #v' *
     2017         [ #E destruct %{cl_b} %{Local} %{ty} % [ %   
     2018           [ <(alloc_vars_env … cl_alloc') // @Hdistinct
     2019           | assumption
     2020          ]| whd %
     2021          ]
     2022         | @H'
     2023         ]
    18762024      ]
    1877     | >unZoo
    1878         [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc)
    1879 *)
     2025    | #b #delta' @eq_block_elim
     2026      [ #E destruct #E whd in E:(??%%); destruct
     2027      | #NE #EM #v' #off' #ty' #EX
     2028        <(alloc_other_high_bound … NE cl_alloc) <(alloc_other_low_bound … NE cl_alloc)
     2029        @(Hexisting b delta' EM v' off' ty' ?)
     2030        %2 assumption
     2031      ]
     2032    | @Hdistinct'
     2033    | #v' #ty' #EX @H %2 assumption
     2034    ]
     2035  ]
     2036] qed.
     2037
    18802038(*
    18812039lemma lset_inclusion_Exists :
     
    19212079   subtrace corresponding to a measurable Clight subtrace.
    19222080 *)
    1923 (* WIP
     2081(* WIP  *)
    19242082include "common/ExtraMonads.ma".
     2083
     2084(* TODO: move *)
     2085lemma distinct_env_irr : ∀tag,A,B,l,f.
     2086  distinct_env tag B (map ?? (λv.〈\fst v, f (\snd v)〉) l) →
     2087  distinct_env tag A l.
     2088#tag #A #B #l #f elim l
     2089[ //
     2090| * #id #a #tl #IH
     2091  * #H1 #H2 %
     2092  [ -IH -H2 elim tl in H1 ⊢ %;
     2093    [ //
     2094    | * #id' #a' #tl' #IH * #NE #TL % /2/
     2095    ]
     2096  | @IH assumption
     2097  ]
     2098] qed.
     2099
     2100lemma distinct_snoc : ∀tag,A,id,a,l.
     2101  All ? (λia.id≠\fst ia) l →
     2102  distinct_env tag A l →
     2103  distinct_env tag A (l@[〈id,a〉]).
     2104#tag #A #id #a #l elim l
     2105[ #_ #_ % %
     2106| * #id' #a' #tl #IH * #NE #TL * #D1 #D2 %
     2107  [ @All_append [ assumption | % [ /2/ | % ] ]
     2108  | @IH [ @TL | @D2 ]
     2109  ]
     2110] qed.
     2111
     2112lemma distinct_env_sym : ∀tag,A,l1,l2.
     2113  distinct_env tag A (l1@l2) →
     2114  distinct_env tag A (l2@l1).
     2115#tag #A #l1 elim l1
     2116[ //
     2117| * #id #a #tl #IH #l2 * #D1 #D2 >append_cons @IH
     2118  <associative_append @distinct_snoc //
     2119] qed.
     2120
     2121
     2122
     2123lemma Exist_sym : ∀tag,A,L,id.
     2124  Exists (identifier tag × A) (λx. \fst x = id) L ↔ Exists ? (λx. id = \fst x) L.
     2125#tag #A #L #id elim L
     2126[ /2/
     2127| * #id' #a #tl #IH %
     2128  [ * [ #E %1 >E % | #H %2 @(proj1 … IH) @H ]
     2129  | * [ #E %1 >E % | #H %2 @(proj2 … IH) @H ]
     2130  ]
     2131] qed.
     2132
     2133lemma Exists_unpair : ∀tag,A,L,id,a.
     2134  Exists (identifier tag × A) (λx. x = 〈id,a〉) L → Exists ? (λx. \fst x = id) L.
     2135#tag #A #L #id #a elim L
     2136[ *
     2137| * #id' #a' #tl #IH * [ #E destruct %1 % | #H %2 @IH @H ]
     2138] qed.
     2139
     2140lemma characterise_vars_lookup : ∀globals,f,vartypes,stacksize,id,ty.
     2141  characterise_vars globals f = 〈vartypes, stacksize〉 →
     2142  distinct_env … (fn_params f @ fn_vars f) →
     2143  Exists ? (λx. x = 〈id,ty〉) (fn_params f @ fn_vars f) →
     2144  ∃c. match c with [Global _ ⇒ False | _ ⇒ True] ∧ lookup' vartypes id = OK ? 〈c,ty〉.
     2145#globals * #ret #args #vars #body
     2146whd in match (characterise_vars ??); elim (args@vars)
     2147[ #vartypes #stacksize #id #ty #_ #_ *
     2148| * #hd #ty #tl #IH
     2149  #vartypes #stacksize #id #ty'
     2150  whd in match (foldr ?????);
     2151  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
     2152  #vartypes' #stackspace' #IH
     2153  whd in ⊢ (??(match % with [_⇒?])? → ?);
     2154  cases (orb ??)
     2155  #E whd in E:(??%?); * #D1 #D2 destruct *
     2156  [ #E destruct %{(Stack stackspace')} % [ % ]
     2157    whd in match (lookup' ??); >lookup_add_hit //
     2158  | 3: #E destruct %{Local} % [ % ]
     2159    whd in match (lookup' ??); >lookup_add_hit //
     2160  | 2,4: #TL cases (IH … (refl ??) D2 TL) #c * #C #LC
     2161    %{c} %{C}
     2162    whd in match (lookup' ??) in LC ⊢ %; >lookup_add_miss try @LC
     2163    elim tl in D1 TL;
     2164    [1,3: #_ *
     2165    |*: * #id' #ty' #tl' #IH * #NE #D' *
     2166        [1,3: #E destruct /2/
     2167        |*: @IH @D'
     2168        ]
     2169    ]
     2170  ]
     2171] qed.   
     2172
     2173(* For showing that binding and storing parameters in memory works.
     2174
     2175lemma bind_and_store_equiv : ∀cl_ge,cm_ge,INV,cl_f,cm_f,cl_env,cm_env,cl_args,cm_args,cl_m1,cl_m2,cm_m,stackptr,Em,vartypes,lbls,uv,cl_s,s,fgens,s1,Is.
     2176  All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
     2177  exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 →
     2178  f_params cm_f = map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params cl_f) →
     2179  alloc_params vartypes lbls cl_s uv DoNotConvert (opttyp_of_type (fn_return cl_f)) (fn_params cl_f) s = return «〈fgens, s1〉, Is» →
     2180  memory_inj Em cl_m1 cm_m →
     2181  ∃cm_en,Hcm_args_present.
     2182    bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧
     2183    memory_matching Em cl_ge cm_ge cl_m2 cm_m cl_env cm_env INV stackptr vartypes ∧
     2184    ∀fInv,Inv,kInv,st. ∃n.
     2185    after_n_steps n ?? (pcs_exec cm_pre) cm_ge (State cm_f s1 cm_env fInv Inv cm_m stackptr Kend kInv st) (λs.cminor_normal s) (λtr,s'.
     2186      tr = E0 ∧
     2187      match s' with
     2188      [ State f' code en _ _ m sp' k' kInv' st' ⇒
     2189          memory_inj Em cl_m2 m ∧
     2190          f' = cm_f ∧ code = s1 ∧ en = cm_env ∧ sp' = stackptr ∧ k' = Kend ∧ st' = st
     2191      | _ ⇒ False
     2192      ]).
     2193
     2194(* Call simulation, not yet complete. *)
    19252195
    19262196lemma clight_cminor_call :
     
    19472217| #g #g' #INV #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #stmt_univ #tmpenv #Htmpenv #Em #HEm_tmp #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #CONT
    19482218  #CL whd in CL:(??%?); destruct
    1949 | #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #INJ #HEm_fn #cl_args #cm_args #Hargs
     2219| #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #Inj #HEm_fn #cl_args #cm_args #Hargs
    19502220  #CL #s2 #tr2 #s3 #tr3 #STEP1 #STEP2 #CS2
    19512221 
     
    19922262
    19932263  whd whd in ⊢ (??%?);
    1994   @pair_elim #cm_m1 #cm_frame #CM_ALLOC
    1995 
    1996  (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f)
    1997 We need to build an extended memory injection to reflect the new allocations;
    1998 then the bind functions put the correct local variables in;
    1999 then after execution the appropriate number of Cminor steps the stored values
    2000 match.
    2001 
    2002 Oh, and there are the locals too.
    2003 
    2004 
    2005 alloc_memory_inj_m2 shows that embedding is fine after the Cminor alloc
    2006 
    2007 ∀Em. memory_inj Em cl_m cm_m →
    2008 (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) →
    2009 exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 →
    2010 alloc cm_m O (f_stacksize cm_f) = 〈cm_m1,cm_frame〉 →
    2011 ∃Em'.
    2012   memory_inj Em' cl_m1 cm_m1 ∧
    2013   (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) ∧
    2014   (∀v,v'. value_eq Em v v' → value_eq Em' v v') ∧
    2015   (∀b1.∀delta. Em' b1=Some ? 〈cm_frame,delta〉 →
    2016              mem block b1 (blocks_of_env cl_env)).
    2017              
    2018   ∀b. Em b = Em' b ∨ (Em b = None ? ∧ ∃off. Em' b = Some ? 〈cm_frame,off〉).
    2019 
    2020 
    2021 translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f →
    2022 All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
    2023 exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 →
    2024 ∃cm_en,Hcm_args_present.
    2025   bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧
     2264  @pair_elim #cm_m1 #cm_frame #cm_alloc
    20262265 
    2027 
     2266  cut (distinct_env … (fn_params cl_f @ fn_vars cl_f))
     2267  [ whd in match cm_vars in D; <map_append in D; <associative_append
     2268    #D lapply (distinct_env_sym … D) <associative_append #D2
     2269    lapply (distinct_env_append_l … D2) #D3
     2270    lapply (distinct_env_sym … D3) >map_append #D4
     2271    @(distinct_env_irr … D4) ] #cl_distinct
     2272  lapply (alloc_vars_rel vartypes ????? Em Inj ? cm_alloc ??? cl_distinct (sym_eq … ALLOC) ?)
     2273  [ #v #ty #EX
     2274    cases (characterise_vars_lookup … (sym_eq … Hcharacterise) cl_distinct EX)
     2275    *
     2276    [ #r * *
     2277    | #off * #_ #L %{(Stack off)} %{L}
     2278      whd %
     2279      [ % // >commutative_plus @(characterise_vars_in_range … (sym_eq … Hcharacterise) … L)
     2280      | @(characterise_vars_disjoint … (sym_eq … Hcharacterise) … L)
     2281      ]
     2282    | * #_ #L %{Local} %{L} %
     2283    ]
     2284  | (* FIXME *) cases daemon
     2285  ]
     2286  * #Em' * * #Inj' #compat' #alloc_ok
     2287 
    20282288*)
    20292289
    2030 (*
    2031 lemma clight_cminor_call_return :
    2032   ∀g1, g2.
    2033   ∀INV:clight_cminor_inv g1 g2.
    2034   ∀s1,s1'.
    2035   clight_cminor_rel g1 g2 INV s1 s1' →
    2036   match Clight_classify s1 with
    2037   [ cl_call ⇒ true
    2038   | cl_return ⇒ true
    2039   | _ ⇒ false ] →
    2040   ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
    2041   ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
    2042     tr = tr' ∧
    2043     clight_cminor_rel g1 g2 INV s2 s2' ∧
    2044       (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
    2045   ).
    2046 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
    2047 inversion Hstate_rel
    2048 [ 1: (* normal *)
    2049   #cl_ge #cm_ge #INV' #cl_s
    2050   #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
    2051   #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
    2052   (* introduce everything *)
    2053   #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    2054   #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    2055   #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
    2056   #HE #HF #HG #HI #HJ #HK
    2057   @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
    2058   destruct (H1 H2)
    2059   @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
    2060   destruct (H3 H4 H5)
    2061   @False_ind @Hclight_class
    2062 | 5:
    2063   #cl_ge #cm_ge #INV' #cl_s
    2064   #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
    2065   #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
    2066   #cm_cond #cm_body #cm_stack #rettyp' #kInv
    2067   (* introduce everything *)
    2068   #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    2069   #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    2070   #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
    2071   #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
    2072   #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
    2073   @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
    2074   destruct (H1 H2)
    2075   @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
    2076   destruct (H3 H4 H5)
    2077   @False_ind @Hclight_class
    2078 | 2:
    2079   #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type
    2080   #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize
    2081   #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
    2082   #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
    2083   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2084   destruct (HA HB)
    2085   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
    2086   destruct (HC HD HE)
    2087   inversion Hcont_rel
    2088   [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
    2089     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2090     destruct (HA HB)
    2091     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2092     destruct (HC HD HE)
    2093     @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    2094     @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
    2095     destruct (HF HG HH HI HJ HK HL) #_
    2096     #s2 #tr
    2097     whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
    2098   | (* Kseq *)
    2099     #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
    2100     #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    2101     * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
    2102     #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
    2103     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2104     destruct (HA HB)
    2105     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2106     destruct (HC HD HE)
    2107     @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
    2108     @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
    2109     destruct (HF HG HH HI HJ HK HL) #_
    2110     #s2 #tr
    2111     whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
    2112   | (* *)
    2113     #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
    2114     #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
    2115     #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
    2116     #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
    2117     #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
    2118     (*     
    2119     * * * * #kHentry_declared * * * *
    2120     * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
    2121     #kHcont_inv #kHmklabels #kHeq_translate
    2122     #kHfind_label *) #kHcont_rel #_
    2123     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2124     destruct (HA HB)
    2125     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2126     destruct (HC HD HE)
    2127     @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    2128     @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    2129     @(jmeq_absorb ?????) #HL
    2130     destruct (HF HG HH HI HJ HK HL) #_
    2131     #s2 #tr
    2132     whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
    2133   ]   
    2134 | 3:
    2135   #cl_ge #cm_ge #INV' #alloc_type
    2136   #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ
    2137   #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh
    2138   #rettyp #cl_k #cm_k #fblock *
    2139   #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel
    2140   #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args
    2141   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2142   destruct (HA HB)
    2143   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2144   destruct (HC HD HE) #_
    2145   #s2 #tr whd in ⊢ ((??%?) → ?);
    2146   @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))
    2147     return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ?
    2148     with
    2149     [ mk_Prod new_cl_env cl_m_alloc ⇒ ?
    2150     ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))))
    2151   #Hexec_alloc_variables normalize nodelta
    2152   #Hstep
    2153   cases (bindIO_inversion ??????? Hstep) -Hstep
    2154   #cl_m_init * #Hexec_bind_parameters
    2155   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 
    2156   %{1} whd whd in ⊢ (??%?);
    2157   (* Alloc big chunk of data of size (f_stacksize cm_f) *)
    2158   @(match (alloc cm_m 0 (f_stacksize cm_f))
    2159     return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ?
    2160     with
    2161     [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ?
    2162     ] (refl ? (alloc cm_m 0 (f_stacksize cm_f))))
    2163   #H_cm_alloc normalize nodelta
    2164   (* Initialise CM /parameters/ *)
    2165 
    2166  
    2167   %{(S (times 3 (|fn_vars|)))} -Hclight_class
    2168   lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters)
    2169   elim cl_args in Hstate_rel Hexec_alloc;
    2170   [ #Hstate_rel whd in ⊢ ((??%%) → ?);
    2171 
    2172     whd in match (exec_bind_parameters ????);
    2173 
    2174   exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉
    2175    
    2176  
    2177   lapply (let_prod_as_inversion ?????? Hstep)
    2178     @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    2179     @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    2180     @(jmeq_absorb ?????) #HL
    2181     destruct (HF HG HH HI HJ HK HL) #_
    2182     #s2 #tr
    2183  
    2184  
    2185   #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
    2186   #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
    2187 ] qed.  *)
     2290
    21882291
    21892292lemma clight_cminor_normal :
Note: See TracChangeset for help on using the changeset viewer.