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