# Changeset 535

Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (8 years ago)
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
Location:
Deliverables/D3.1/C-semantics
Files:
6 edited

Unmodified
Removed
• ## Deliverables/D3.1/C-semantics/Integers.ma

 r487 include "extralib.ma". include "cerco/BitVector.ma". include "cerco/BitVectorZ.ma". include "cerco/Arithmetic.ma". (* * * Comparisons *) integer (type [Z]) plus a proof that it is in the range 0 (included) to [modulus] (excluded. *) (* XXX: hack to prevent normalization of huge proof term. *) inductive inrange : Z → Prop ≝ | inrg_mod : ∀i:Z. inrange (i \mod modulus) | inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i. inductive int: Type[0] ≝ | mk_int: ∀i:Z. inrange i → int. (* record int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }. *) definition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ]. definition int : Type[0] ≝ BitVector wordsize. definition intval: int → Z ≝ Z_of_unsigned_bitvector ?. definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus. #i cases i; #x #H cases H; [ #x' @modZ_lt_mod //; | //; ] qed. #i % whd in ⊢ (?%%) [ @Z_unsigned_min | @Z_unsigned_max ] qed. (* The [unsigned] and [signed] functions return the Coq integer corresponding (* Conversely, [repr] takes a Coq integer and returns the corresponding machine integer.  The argument is treated modulo [modulus]. *) (*axiom repr : Z → int.*) (* definition repr : Z → int := λx. mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos). *) definition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x). definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z. definition zero := repr 0. definition iwordsize := repr (Z_of_nat wordsize). axiom mk_int_eq: ∀x,y,Px,Py. x = y → mk_int x Px = mk_int y Py. (*Proof. intros. subst y. generalize (proof_irrelevance _ Px Py); intro. subst Py. reflexivity. Qed.*) axiom eq_dec: ∀x,y: int. (x = y) + (x ≠ y). (*Proof. intros. destruct x; destruct y. case (zeq intval0 intval1); intro. left. apply mkint_eq. auto. right. red; intro. injection H. exact n. Qed.*) lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y). #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E [ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ] | %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ] ] qed. (* * Arithmetic and logical operations over machine integers *) definition eq : int → int → bool ≝ λx,y: int. if eqZb (unsigned x) (unsigned y) then true else false. definition eq : int → int → bool ≝ eq_bv wordsize. definition lt : int → int → bool ≝ λx,y:int. if Zltb (signed x) (signed y) then true else false. ] | neg p ⇒ match p with match p return λ_.bool × Z with [ p1 q ⇒ 〈true, Zpred (neg q)〉 | p0 q ⇒ 〈false, neg q〉 theorem eq_sym: ∀x,y. eq x y = eq y x. #x #y whd in ⊢ (??%%); @eqZb_elim #H [ >H >(eqZb_z_z …) // | >(eqZb_false … (sym_neq … H)) // #x #y @eq_bv_elim @eq_bv_elim /2/ [ #NE #E @False_ind >E in NE * /2/ | #E #NE @False_ind >E in NE * /2/ ] qed. theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y). #x #y whd in ⊢ (??%??); elim (eq_dec x y); #H [ >H >(eqZb_z_z …) //; | >(eqZb_false …) //; elim x in H ⊢ %; elim y; #x' #Px #y' #Py #H normalize; @(not_to_not … H) @mk_int_eq ] qed. #x #y @eq_bv_elim #H @H qed. theorem eq_true: ∀x. eq x x = true. theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. #i cases i; #i' #H cases H; /2/; #i @intrange qed.
• ## Deliverables/D3.1/C-semantics/Smallstep.ma

 r487 [ @(t'⧺t2) | // | <(Eapp_assoc …) //; | <(Eapp_assoc …)

star tr ge s1 t s2. #tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1 @(star_step … H1 H2 …) //; @(star_step … H1 H2 …) @e1; qed. forever tr ge s1 (t ⧻ T). #tr #ge #s1 #t1 #s2 #H elim H; [ #s' #T #H2 //; [ #s' #T #H2 @H2 | #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3 >e1 >(Eappinf_assoc …) elim (IH ? B); #st3' *; #C #D %{ st3'} % //; @(star_trans ??? tA st2' ? tB) //; elim A; /2/; *; //; @(star_trans ??? tA st2' ? tB ?? C Ht) elim A /2/ * // ] qed.

• ## Deliverables/D3.1/C-semantics/cerco/BitVector.ma

 r475 false) b c. lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. (x = y → P true) → (x ≠ y → P false) → P (eq_bv n x y). #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) #Q * *; normalize /3/ qed. let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
• ## Deliverables/D3.1/C-semantics/cerco/Util.ma

 r534 ]. (* notation "hvbox('if' b 'then' t 'else' f)" non associative with precedence 83 for @{ 'if_then_else \$b \$t \$f }. *) notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
• ## Deliverables/D3.1/C-semantics/cerco/Vector.ma

 r534 include "arithmetics/nat.ma". include "oldlib/eq.ma". (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ match v return (λm.λv. Vector A m) with [ VEmpty ⇒ [[ ]] | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) ]. // qed. (* At some points matita will attempt to reduce reverse with a known vector, which reduces the equality proof for the cast.  Normalising this proof needs to be fast enough to keep matita usable. *) let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ match n return λn'.∀m.S(n'+m) = n'+S m with [ O ⇒ λm.refl ?? | S n' ⇒ λm. ? ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. let rec revapp (A: Type[0]) (n: nat) (m:nat) (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝ match v return λn'.λ_. Vector A (n' + m) with [ VEmpty ⇒ acc | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ ]. > plus_n_Sm_fast @refl qed. let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝ (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. < plus_n_O @refl qed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) qed. lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with [ O ⇒ λP.λv.P [[ ]] → P v | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v ] P v. @(λA,n. λP:Vector A n → Prop. λv. match v return ? with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P) [ // | // ] qed. (* XXX Proof below fails at qed. #A #n #P * [ #H @H | #m #h #t #H @H ] qed. *) lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → ∀n,x,y. (x = y → P true) → (x ≠ y → P false) → P (eq_v A n f x y). #P #A #f #f_elim #n #x elim x [ #y @(vector_inv_n … y) normalize /2/ | #m #h #t #IH #y @(vector_inv_n … y) #h' #t' #Ht #Hf whd in ⊢ (?%) @(f_elim ? h h') #Eh [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ] | @Hf % #E' destruct (E') elim Eh /2/ ] ] qed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Subvectors.                                                                *)
• ## Deliverables/D3.1/C-semantics/extralib.ma

 r487 ]. interpretation "integer multiplication" 'times x y = (Z_times x y). (* Now in cerco/Util.ma (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *) notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). *) (* datatypes/list.ma *)
Note: See TracChangeset for help on using the changeset viewer.