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.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • 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.
Note: See TracChangeset for help on using the changeset viewer.