Ignore:
Timestamp:
Apr 25, 2013, 6:03:24 PM (6 years ago)
Author:
campbell
Message:

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3170 r3178  
    17471747#A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed.
    17481748
     1749lemma pair_as_elim:
     1750  ∀A,B,C: Type[0].
     1751  ∀p.
     1752  ∀T: ∀a:A. ∀b:B. 〈a,b〉 = p → C.
     1753  ∀P: A×B → C → Prop.
     1754    (∀lft, rgt. ∀E:〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt E)) →
     1755      P p (let 〈lft, rgt〉 as E ≝ p in T lft rgt E).
     1756#A #B #C * /2/
     1757qed.
     1758
     1759(* TODO: move *)
     1760lemma alloc_low_bound : ∀m,l,h,m',b.
     1761  alloc m l h = 〈m',b〉 →
     1762  low_bound m' b = l.
     1763* #contents #next #next_ok #l #h #m' #b #E
     1764whd in E:(??%%); destruct
     1765whd in ⊢ (??%?); >update_block_s
     1766%
     1767qed.
     1768
     1769lemma alloc_high_bound : ∀m,l,h,m',b.
     1770  alloc m l h = 〈m',b〉 →
     1771  high_bound m' b = h.
     1772* #contents #next #next_ok #l #h #m' #b #E
     1773whd in E:(??%%); destruct
     1774whd in ⊢ (??%?); >update_block_s
     1775%
     1776qed.
     1777
     1778(* Weaker version of Zlt_to_Zle *)
     1779lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y.
     1780#x #y #H
     1781@(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H
     1782qed.
     1783
     1784axiom unZoo : ∀off:Z.
     1785  off < Z_two_power_nat 16 →
     1786  Zoo (offset_of_Z off) = off.
     1787
     1788lemma le_to_Zle : ∀x,y:nat. le x y → Zle x y.
     1789#x #y #H @(le_ind ????? H)
     1790[ //
     1791| #m #H1 #H2 >Zsucc_pos @(transitive_Zle … (Zsucc_le m)) assumption
     1792] qed.
     1793
     1794lemma lt_to_Zlt : ∀x,y:nat. lt x y → Zlt x y.
     1795#x #y whd in ⊢ (% → ?); #H
     1796<(Zpred_Zsucc x) @Zle_to_Zlt
     1797<Zsucc_pos
     1798@le_to_Zle assumption
     1799qed.
     1800
     1801lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z.
     1802/2/
     1803qed.
     1804
     1805lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y.
     1806/2/
     1807qed.
     1808
     1809theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
     1810#n #m #p #Hle #Hlt lapply (Zlt_to_Zle … Hlt)
     1811@Zlt_to_Zle_to_Zlt @Zle_Zlt_Zsucc assumption
     1812qed.
     1813
     1814
     1815(* This roughly corresponds to lemma 69 of Leroy and Blazy *)
     1816(*
     1817lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame.
     1818∀Em. memory_inj Em cl_m cm_m →
     1819Z_of_nat stacksize < Z_two_power_nat 16 →
     1820alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 →
     1821∀L, cl_env, cl_m1.
     1822exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 →
     1823(∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧
     1824  match c with
     1825  [ Local ⇒ True
     1826  | Stack off ⇒
     1827    le O off ∧ le (sizeof ty + off) stacksize ∧
     1828    (∀v',off',t'. v≠v' → lookup' vartypes v' = return 〈Stack off',t'〉 → le (off' + sizeof t') off ∨ le (off + sizeof ty) off')
     1829  | Global _ ⇒ False
     1830  ]) →
     1831∃Em'. memory_inj Em' cl_m1 cm_m1 ∧
     1832  embedding_compatible Em Em' ∧
     1833  ∀v. Exists … (λx.\fst x = v) L →
     1834  ∃b,c,t. lookup … cl_env v = Some ? b ∧
     1835    lookup' vartypes v = return 〈c,t〉 ∧
     1836    match c with
     1837    [ Local ⇒ Em' b = None ?
     1838    | Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉
     1839    | Global _ ⇒ False
     1840    ].
     1841#vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L
     1842cut (block_implementable_bv cm_m1 cm_frame)
     1843[ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % //
     1844  cases stacksize // ] #cm_bi
     1845lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi)
     1846lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid
     1847cut (∀b:block. ∀delta':offset.
     1848    Em b=Some (block×offset) 〈cm_frame,delta'〉 →
     1849    ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 →
     1850    high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off)
     1851      ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta')
     1852[ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V
     1853  @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ]
     1854
     1855generalize in match Em; -Em generalize in match empty_env; elim L
     1856[ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc
     1857  whd in cl_alloc:(??%%); destruct #H
     1858  %{Em} % [ % [ @Inj | // ] | #v * ]
     1859| * #v #ty #tl #IH
     1860  #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1
     1861  whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H
     1862  cases (H v ty ?) [2: %1 % ] *
     1863  [ #r * #L *
     1864  | #off * #L * * #off_low #off_high #other
     1865    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)
     1867    | cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U
     1868      [ /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) | // ]
     1874          ]
     1875        ]
     1876      ]
     1877    | >unZoo
     1878        [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc)
     1879*)
    17491880(*
    17501881lemma lset_inclusion_Exists :
     
    17901921   subtrace corresponding to a measurable Clight subtrace.
    17911922 *)
    1792 (* WIP
     1923(* WIP
     1924include "common/ExtraMonads.ma".
     1925
    17931926lemma clight_cminor_call :
    17941927    ∀g,g'.
     
    18311964      whd in STEP1:(??%%); destruct ]
    18321965  -cl_fd
     1966  (* and the Cminor one must be Internal *)
     1967  @('bind_inversion Htranslate) #cm_f #Htranslate' #E
     1968  whd in E:(??%%); destruct
     1969
     1970  (* Invert function translation *)
     1971  (* NB: if you want to examine the proof state in here, you probably want to
     1972     turn off the pretty printer - it doesn't cope well with a large proof
     1973     term. *)
     1974  @('bind_inversion Htranslate') * * #lbls #Ilbls #ul #Hbuild_label_env
     1975  whd in ⊢ (??%? → ?);
     1976  @pair_as_elim #vartypes #stacksize #Hcharacterise
     1977  letin uv ≝ (mk_tmpgen ?? [ ] ??) #H
     1978  @('bind_inversion H) -H #s0 #Htranslate_statement #H
     1979  @('bind_inversion H) -H * * #fgens #s1 #Is #Halloc_params
     1980  letin cm_params ≝ (map ??? (fn_params cl_f))
     1981  whd in ⊢ (??%? → ?);
     1982  letin cm_vars ≝ (map ??? (?@fn_vars cl_f)) #H
     1983  @('bind_inversion H) -H #D #Hcheck_distinct_env
     1984  whd in ⊢ (??%% → ?); generalize in ⊢ (??(??(???????%))? → ?);
     1985  (* It's safe to use the pretty printer again. *)
     1986  #cm_Sinv #H destruct
    18331987
    18341988  (* Invert Clight STEP1 *) 
     
    18361990  cases (bindIO_inversion ??????? STEP1) -STEP1 #cl_m2 * #BIND #STEP1
    18371991  whd in STEP1:(??%%); destruct
     1992
     1993  whd whd in ⊢ (??%?);
     1994  @pair_elim #cm_m1 #cm_frame #CM_ALLOC
     1995
     1996 (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f)
     1997We need to build an extended memory injection to reflect the new allocations;
     1998then the bind functions put the correct local variables in;
     1999then after execution the appropriate number of Cminor steps the stored values
     2000match.
     2001
     2002Oh, and there are the locals too.
     2003
     2004
     2005alloc_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〉) →
     2009exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 →
     2010alloc 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
     2021translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f →
     2022All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
     2023exec_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» ∧
     2026 
     2027
    18382028*)
    18392029
Note: See TracChangeset for help on using the changeset viewer.