Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1605 r1626  
    1212
    1313definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
    14   stmt_P (λs.stmt_vars (present ?? en) s ∧
     14  stmt_P (λs.stmt_vars (λid,ty. present ?? en id) s ∧
    1515             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
    1616
     
    2323#s * #H1 #H2 %
    2424[ @(stmt_vars_mp … H1)
    25   #l #H @update_still_present @H
     25  #l #ty #H @update_still_present @H
    2626| @H2
    2727] qed.
     
    5353inductive stack : Type[0] ≝
    5454| SStop : stack
    55 | Scall : ∀dest:option ident. ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some id ⇒ present ?? en id] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
     55| Scall : ∀dest:option (ident×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
    5656
    5757inductive state : Type[0] ≝
     
    9292axiom FailedLoad : String.
    9393
    94 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (present ?? en)) (sp:block) (m:mem) on e : res (trace × val) ≝
    95 match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
     94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝
     95match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → res (trace × val) with
    9696[ Id _ i ⇒ λEnv.
    9797    let r ≝ lookup_present ?? en i ? in
     
    383383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
    384384                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
    385                    | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
     385                   | Some idty ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
    386386                   ] dstP
    387387        ]
     
    414414  @(stmt_P_mp … (f_inv f))
    415415  #s * #V #L %
    416   [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
     416  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    417417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
    418       * #id' #ty * #E1 #H <E1 @H
     418      * #id' #ty * #E1 destruct #H @H
    419419    | *: #H cases (Exists_All … H (init_locals_env … en …))
    420       * #id' #ty * #E1 #H <E1 @H
     420      * #id' #ty * #E1 destruct #H @H
    421421    ]
    422422  | 2,4: @L
Note: See TracChangeset for help on using the changeset viewer.