source: etc/campbell/dev-notes/2011-07-28-envs.patch

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 12.7 KB
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    diff --git a/Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma b/Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma
    index c520cea..378c281 100644
    a b match op with 
    382382| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
    383383].
    384384
    385 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
    386   expr_vars ? e1 P →
    387   expr_vars ? e2 P →
     385lemma OK_eq : ∀A,x,y.OK A x = OK A y → x = y.
     386#A #x #y #E destruct (E) @refl
     387qed.
     388
     389lemma translate_binop_vars : ∀op,ty1,e1,ty2,e2,ty,e.
    388390  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
    389   expr_vars ? e P.
    390 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
     391  fv_expr ? e = fv_expr ? e1 ∪ fv_expr ? e2.
     392* #ty1 #e1 #ty2 #e2 #ty #e
    391393whd in ⊢ (??%? → ?)
    392394[ cases (classify_add ty1 ty2)
    393395  [ 3,4: #z ] whd in ⊢ (??%? → ?)
    394396  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    395397    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    396     whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
     398    whd in c:(??%?);
     399    <(OK_eq ??? c) whd in ⊢ (??%?) whd in ⊢ (??(???%)?) whd in ⊢ (??(???(???%))?)
     400    > union_empty_r @refl
    397401  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    398402    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    399     whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
    400   | *: #E destruct (E) % try @H1 @H2
     403    whd in c:(??%?); <(OK_eq ??? c)
     404    whd in ⊢ (??%?) whd in ⊢ (??(???%)?) whd in ⊢ (??(???(???%))?)
     405    > union_empty_r @union_commutative
     406  | 3,4: #E <(OK_eq ??? E) whd in ⊢ (??%?) @refl
     407  | #E destruct
    401408  ]
    402409| cases (classify_sub ty1 ty2)
    403410  [ 3,4: #z] whd in ⊢ (??%? → ?)
    404411  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
    405412    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    406     whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
    407   | *: #E destruct (E) % try @H1 try @H2 % // @H2
     413    whd in c:(??%?); <(OK_eq ??? c)
     414    whd in ⊢ (??%?) whd in ⊢ (??(??%?)?) > union_empty_r @refl
     415  | 1,3,4: #E <(OK_eq ??? E)
     416    whd in ⊢ (??%?) whd in ⊢ (??(???%)?)
     417    try @refl >union_empty_r @refl
     418  | #E destruct
    408419  ]
    409 | cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
    410     % try @H1 @H2
    411 | cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
    412     % try @H1 @H2
    413 | cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
    414     % try @H1 @H2
    415 | 6,7,8,9: #E destruct % try @H1 @H2
    416 | cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
    417 | 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     420| cases (classify_mul ty1 ty2) #E whd in E:(??%?) [3:destruct] <(OK_eq ??? E)
     421  @refl
     422| cases (classify_div ty1 ty2) #E whd in E:(??%?) [4:destruct] <(OK_eq ??? E)
     423  @refl
     424| cases (classify_mod ty1 ty2) #E whd in E:(??%?) [3:destruct] <(OK_eq ??? E)
     425  @refl
     426| 6,7,8,9: #E <(OK_eq ??? E) @refl
     427| cases (classify_shr ty1 ty2) #E whd in E:(??%?) [3: destruct ] <(OK_eq ??? E) @refl
     428| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?) [5,10,15,20,25,30: destruct] <(OK_eq ??? E) @refl
    418429] qed.
    419430
    420431(* We'll need to implement proper translation of pointers if we really do memory
    definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P 
    430441  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
    431442  ].
    432443
    433 definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
    434 λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
     444definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). ∀i.i∈fv_expr ? e→P i) → res (Σe':CMexpr (ASTptr r2).∀i.i∈fv_expr ? e'→P i) ≝
     445λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).∀i.i∈fv_expr ? e→P i) e.
    435446
    436447notation "hvbox(« term 19 a, break term 19 b»)"
    437448with precedence 90 for @{ (dp ?? $a $b) }.
    lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. 
    441452#A #P * #a #p @p
    442453qed.
    443454
     455definition expr_vars : ∀t.expr t → (ident → Prop) → Prop ≝ λt,e,P. ∀i.i∈fv_expr t e → P i.
     456
    444457definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
    445458λP,ty1,ty2.
    446459match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
    match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with 
    473486    | _ ⇒ Error ? (msg TypeMismatch)
    474487    ]
    475488| _ ⇒ λ_. Error ? (msg TypeMismatch)
    476 ]. whd @sig_ok qed.
     489]. @(sig_ok ?? e) qed.
    477490
    478491definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
    479492λty1,ty2,P,p.
    definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → re 
    512525
    513526notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    514527
     528axiom mem_singleton : ∀tag.∀i,j:identifier tag. i∈{(j)} → i = j.
     529
    515530let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
    516531match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
    517532[ Expr ed ty ⇒
    match e with 
    671686  | _ ⇒ Error ? (msg BadLvalue)
    672687  ]
    673688].
    674 whd try @I
    675 [ >E @I
     689[ 1,2,4,5,6,7: whd #i whd in ⊢ (?(??%?) → ?) #H cases (mem_empty … H)
     690| whd #i #H >(mem_singleton … H) whd >E @I
    676691| >(E ? (refl ??)) @refl
    677 | 3,4: @sig_ok
    678 | @(translate_binop_vars … E) @sig_ok
     692| @(sig_ok ?? e1')
     693| @(sig_ok ?? e1')
     694| whd >(translate_binop_vars … E) @(sig_ok ??
    679695| % [ % ] @sig_ok
    680696| % [ % @sig_ok ] whd @I
    681697| % [ % [ @sig_ok | @I ] | @sig_ok ]
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    diff --git a/Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma b/Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma
    index abd64e9..a1e9e85 100644
    a b match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) wi 
    2121(* Produces a few extra skips - hopefully the compiler will optimise these
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False)
     24definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. fv_stmt s = ∅
    2525λid,r,init,off.
    2626match init_expr init with
    2727[ None ⇒ St_skip
    match init_expr init with 
    3131    ]
    3232].
    3333//
    34 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     34cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; @refl
    3535qed.
    3636
    3737lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
    lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D 
    4343#A #B #C #D *; normalize /2/
    4444qed.
    4545
    46 lemma sig_stmt_vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.
    47   stmt_vars s P.
    48 #P * #s #p whd in ⊢ (?%?) //
     46lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
     47  P x.
     48#A #P * #a #p @p
    4949qed.
    5050
    51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False) ≝
     51lemma emptyset_inv : ∀tag.∀s,t:identifier_set tag. s = ∅ → t = ∅ → s ∪ t = ∅.
     52#tag #s #t #E1 #E2 >E1 >E2 @refl
     53qed.
     54
     55definition init_var : ident → region → list init_data → Σs:stmt. fv_stmt s = ∅ ≝
    5256λid,r,init.
    5357\snd (foldr ??
    5458  (λdatum,os.
    definition init_var : ident → region → list init_data → Σs:stmt. stmt_var 
    5761  〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init).
    5862[ whd //
    5963| elim init whd //
    60   #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars | @IH ]
     64  #h #t #IH whd in ⊢ (??(?(???%))?) @sndredex @emptyset_inv [ @sig_ok | @IH ]
    6165] qed.
    6266
    63 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_vars s (λ_.False)
    64 λvars. foldr ? (Σs:stmt. stmt_vars s (λ_.False))
    65   (λvar,s. dp ? (λx.stmt_vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.
    66 whd % @sig_stmt_vars
     67definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. fv_stmt s = ∅
     68λvars. foldr ? (Σs:stmt. fv_stmt s = ∅)
     69  (λvar,s. dp ? (λx.fv_stmt x = ∅) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.fv_stmt x = ∅) St_skip (refl ??)) vars.
     70@emptyset_inv @sig_ok
    6771qed.
    6872
    69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) →
     73definition add_statement : ident → (Σs:stmt. fv_stmt s = ∅) →
    7074                              list (ident × (fundef internal_function)) →
    7175                              list (ident × (fundef internal_function)) ≝
    7276λid,s. match s with [ dp s H ⇒
    definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) → 
    8690          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
    8791          ]
    8892      | inr _ ⇒ 〈id',f'〉 ]) ].
     93#id whd in H:(??%?) ⊢ ((?(??%?)) → ?) >H #H' @(f_bound f) @H' >sig_ok in H @mem_set_inv_r @H
    8994whd %
    9095[ @(stmt_vars_mp … H) #i *
    9196| //
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    diff --git a/Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma b/Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma
    index d2ede24..5f6372b 100644
    a b match e with 
    3030| Ecost _ _ e ⇒ expr_vars ? e P
    3131].
    3232
     33let rec fv_expr (t:typ) (e:expr t) on e : identifier_set SymbolTag ≝
     34match e with
     35[ Id _ i ⇒ { (i) }
     36| Cst _ _ ⇒ ∅
     37| Op1 _ _ _ e ⇒ fv_expr ? e
     38| Op2 _ _ _ _ e1 e2 ⇒ fv_expr ? e1 ∪ fv_expr ? e2
     39| Mem _ _ _ e ⇒ fv_expr ? e
     40| Cond _ _ _ e1 e2 e3 ⇒ fv_expr ? e1 ∪ fv_expr ? e2 ∪ fv_expr ? e3
     41| Ecost _ _ e ⇒ fv_expr ? e
     42].
     43
    3344lemma expr_vars_mp : ∀t,e,P,Q.
    3445  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
    3546#t0 #e elim e normalize /3/
    match s with 
    7788| St_cost _ s ⇒ stmt_vars s P
    7889].
    7990
     91let rec fv_stmt (s:stmt) : identifier_set SymbolTag ≝
     92match s with
     93[ St_skip ⇒ ∅
     94| St_assign _ i e ⇒ {(i)} ∪ fv_expr ? e
     95| St_store _ _ _ e1 e2 ⇒ fv_expr ? e1 ∪ fv_expr ? e2
     96| St_call oi e es ⇒ match oi with [ None ⇒ ∅ | Some i ⇒ {(i)} ] ∪ fv_expr ? e ∪
     97                    foldr (Σt:typ.expr t) ? (λte,s. match te with [ dp t e ⇒ s ∪ (fv_expr t e) ]) ∅ es
     98| St_tailcall e es ⇒ fv_expr ? e ∪
     99                    foldr (Σt:typ.expr t) ? (λte,s. match te with [ dp t e ⇒ s ∪ (fv_expr t e) ]) ∅ es
     100| St_seq s1 s2 ⇒ fv_stmt s1 ∪ fv_stmt s2
     101| St_ifthenelse _ _ e s1 s2 ⇒ fv_expr ? e ∪ fv_stmt s1 ∪ fv_stmt s2
     102| St_loop s ⇒ fv_stmt s
     103| St_block s ⇒ fv_stmt s
     104| St_exit _ ⇒ ∅
     105| St_switch _ _ e _ _ ⇒ fv_expr ? e
     106| St_return ote ⇒ match ote with [ None ⇒ ∅ | Some te ⇒ match te with [ dp t e ⇒ fv_expr t e ] ]
     107| St_label _ s ⇒ fv_stmt s
     108| St_goto _ ⇒ ∅
     109| St_cost _ s ⇒ fv_stmt s
     110].
     111
    80112lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q.
    81113#P #Q #H #s elim s normalize
    82114[ //
    record internal_function : Type[0] ≝ 
    101133; f_vars      : list (ident × typ)
    102134; f_stacksize : nat
    103135; f_body      : stmt
    104 ; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
     136; f_bound     : ∀id.id ∈ fv_stmt f_body → Exists ? (λx.\fst x = id) (f_params @ f_vars)
    105137}.
    106138
    107139definition Cminor_program ≝ program (fundef internal_function) unit.
  • Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

    diff --git a/Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma b/Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma
    index 56bfae7..f946e9c 100644
    a b lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s. 
    187187[ * #x * #y #E >E //
    188188| #E >E //
    189189] qed.
     190
     191lemma union_commutative : ∀tag. commutative … (union_set tag).
     192#tag * #s * #s'
     193whd in ⊢ (??%%) @eq_f whd in ⊢ (??(???%%)(???%%))
     194generalize in s:(??%) s':(??%) ⊢ (??(??%??)(??%??))
     195#n elim n
     196[ #x #y
     197  cases (BitVectorTrie_O … x) [ * * ] #E1 >E1
     198  cases (BitVectorTrie_O … y) [ 1,3: * * ] #E2 >E2
     199  @refl
     200| #m #IH #x #y
     201  cases (BitVectorTrie_Sn … x) [ * #x1 * #x2 ] #E1 >E1
     202  cases (BitVectorTrie_Sn … y) [ 1,3: * #y1 * #y2 ] #E2 >E2
     203  whd in ⊢ (??%%) try @refl
     204  >(IH x1 y1) >(IH x2 y2) @refl
     205] qed.
     206
     207lemma mem_empty : ∀tag. ∀i:identifier tag. i∈∅ → False.
     208#tag #i normalize //
     209qed.
Note: See TracBrowser for help on using the repository browser.