Changeset 1876


Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (8 years ago)
Author:
campbell
Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1713 r1876  
    349349[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    350350| * #id #ty #t #IH #en #m #en' #m'
    351   lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
     351  lapply (refl ? (alloc ? m O (sizeof ty) Any)) #ALLOC #EXEC
    352352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
  • src/Clight/test/castremoval.test.ma

    r1513 r1876  
    44example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    55normalize  (* you can examine the result here *)
    6 @refl
     6%
    77qed.
    88
     
    1616example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
    1717normalize  (* you can examine the result here *)
    18 @refl
     18%
    1919qed.
    2020
  • src/Clight/test/duff.test.ma

    r1513 r1876  
    33example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    44normalize  (* you can examine the result here *)
    5 @refl
     5%
    66qed.
  • src/Clight/test/factorial.test.ma

    r1513 r1876  
    33example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    44normalize  (* you can examine the result here *)
    5 @refl
     5%
    66qed.
  • src/Clight/test/null-op.test.ma

    r1513 r1876  
    33example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
    44normalize  (* you can examine the result here *)
    5 @refl
     5%
    66qed.
  • src/Clight/test/search.c.ma

    r1618 r1876  
    186186example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    187187normalize  (* you can examine the result here *)
    188 @refl
     188%
    189189qed.
    190190
     
    197197*)
    198198normalize
    199 @refl
     199%
    200200qed.
    201201
     
    213213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    214214normalize
    215 @refl
     215%
    216216qed.
    217217(*
  • src/Clight/test/sum.test.ma

    r1618 r1876  
    33example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    44normalize  (* you can examine the result here *)
    5 @refl
     5%
    66qed.
    77
     
    1010example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
    1111normalize  (* you can examine the result here *)
    12 @refl
     12%
    1313qed.
    1414
     
    2020   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
    2121normalize
    22 @refl
     22%
    2323qed.
    2424
     
    3131 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
    3232normalize
    33 @refl
     33%
    3434qed.
    3535(*
  • src/Clight/test/switcher.test.ma

    r1513 r1876  
    44example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
    55normalize  (* you can examine the result here *)
    6 @refl qed.
     6% qed.
    77
    88example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
    99normalize  (* you can examine the result here *)
    10 @refl qed.
     10% qed.
    1111
    1212example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
    1313normalize  (* you can examine the result here *)
    14 @refl qed.
     14% qed.
    1515
    1616example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    1717normalize  (* you can examine the result here *)
    18 @refl qed.
     18% qed.
    1919
    2020example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
    2121normalize  (* you can examine the result here *)
    22 @refl qed.
     22% qed.
  • src/common/Animation.ma

    r1231 r1876  
    9292| witness : ∀a:A. result A a.
    9393
    94 definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
    95 λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
     94inductive finishes_with : int → ∀S.res (snapshot S) → Prop ≝
     95fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
    9696
    9797include "common/Mem.ma".
Note: See TracChangeset for help on using the changeset viewer.