Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (9 years ago)
Author:
campbell
Message:

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Smallstep.ma

    r487 r535  
    8787    [ @(t'⧺t2)
    8888    | //
    89     | <(Eapp_assoc …) //;
     89    | <(Eapp_assoc …) <H2 @H5
    9090    ]
    9191]
     
    104104  star tr ge s1 t s3.
    105105#tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3
    106 @(star_trans … H1 … (star_one … H2)) //;
     106@(star_trans … H1 … (star_one … H2)) @H3
    107107qed.
    108108
     
    124124  ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2.
    125125#tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1
    126 @(star_step … H1 H2 …) //;
     126@(star_step … H1 H2 …) @e1;
    127127qed.
    128128
     
    216216  forever tr ge s1 (t ⧻ T).
    217217#tr #ge #s1 #t1 #s2 #H elim H;
    218 [ #s' #T #H2 //;
     218[ #s' #T #H2 @H2
    219219| #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3
    220220    >e1 >(Eappinf_assoc …)
     
    551551    elim (IH ? B); #st3' *; #C #D
    552552    %{ st3'} % //;
    553     @(star_trans ??? tA st2' ? tB) //;
    554     elim A; /2/; *; //;
     553    @(star_trans ??? tA st2' ? tB ?? C Ht)
     554    elim A /2/ * //
    555555] qed.
    556556
Note: See TracChangeset for help on using the changeset viewer.