Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (9 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/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(*
Note: See TracChangeset for help on using the changeset viewer.