(** {1 Theory of maps} *) (** {2 Generic Maps} *) theory Map type map 'a 'b (** if ['b] is an infinite type, then [map 'a 'b] is infinite *) meta "material_type_arg" type map, 1 function get (map 'a ~'b) 'a : 'b function set (map 'a ~'b) 'a 'b : map 'a 'b (** syntactic sugar *) function ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i function ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v axiom Select_eq : forall m : map 'a 'b. forall a1 a2 : 'a. forall b : 'b [m[a1 <- b][a2]]. a1 = a2 -> m[a1 <- b][a2] = b axiom Select_neq : forall m : map 'a 'b. forall a1 a2 : 'a. forall b : 'b [m[a1 <- b][a2]]. a1 <> a2 -> m[a1 <- b][a2] = m[a2] function const ~'b : map 'a 'b axiom Const : forall b:'b, a:'a. (const b)[a] = b end (** {2 Sorted Maps (indexed by integers)} *) theory MapSorted use import int.Int use import Map type elt predicate le elt elt predicate sorted_sub (a : map int elt) (l u : int) = forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2] (** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)] is sorted w.r.t order relation [le] *) end (** {2 Maps Equality (indexed by integers)} *) theory MapEq use import int.Int use import Map predicate map_eq_sub (a1 a2 : map int 'a) (l u : int) = forall i:int. l <= i < u -> a1[i] = a2[i] end (** {2 Injectivity and surjectivity for maps (indexed by integers)} *) theory MapInjection use import int.Int use export Map predicate injective (a: map int int) (n: int) = forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j] (** [injective a n] is true when [a] is an injection on the domain [(0..n-1)] *) predicate surjective (a: map int int) (n: int) = forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i) (** [surjective a n] is true when [a] is a surjection from [(0..n-1)] to [(0..n-1)] *) predicate range (a: map int int) (n: int) = forall i: int. 0 <= i < n -> 0 <= a[i] < n (** [range a n] is true when [a] maps the domain [(0..n-1)] into [(0..n-1)] *) lemma injective_surjective: forall a: map int int, n: int. injective a n -> range a n -> surjective a n (** main lemma: an injection on [(0..n-1)] that ranges into [(0..n-1)] is also a surjection *) end (** {2 Map Permutation (indexed by integers)} *) theory MapPermut use import int.Int use import Map use import MapEq predicate exchange (a1 a2: map int 'a) (l u i j: int) = l <= i < u /\ l <= j < u /\ a1[i] = a2[j] /\ a1[j] = a2[i] /\ (forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k]) inductive permut (map int 'a) (map int 'a) int int = | permut_refl : (* a1[l..u[ and a2[l..u[ are identical *) forall a1 a2 : map int 'a. forall l u : int. map_eq_sub a1 a2 l u -> permut a1 a2 l u | permut_trans : (* transitivity *) forall a1 a2 a3 : map int 'a. forall l u : int. permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u | permut_exchange : (* elements at indices i and j have been swapped *) forall a1 a2 : map int 'a. forall l u i j : int. exchange a1 a2 l u i j -> permut a1 a2 l u (** [permut m1 m2 l u] is true when the segment [m1(l..u-1)] is a permutation of the segment [m2(l..u-1)]. Values outside of the interval (l..u-1) are ignored. It is defined inductively as the smallest equivalence relation that contains the exchanges *) (* (* symmetry can be proved *) lemma permut_sym: forall a1 a2 : map int 'a. forall l u : int. permut a1 a2 l u -> permut a2 a1 l u *) lemma exchange_set : forall a: map int 'a, l u i j: int. l <= i < u -> l <= j < u -> exchange a a[i <- a[j]][j <- a[i]] l u i j lemma permut_exists : forall a1 a2: map int 'a, l u i: int. permut a1 a2 l u -> l <= i < u -> exists j: int. l <= j < u /\ a1[j] = a2[i] (* THIS IS FALSE WHEN m < l < u lemma permut_concat: forall a1 a2: map int 'a, l m u: int. permut a1 a2 l m -> permut a1 a2 m u -> permut a1 a2 l u *) end (** {2 Sum of elements of a map (indexed by integers)} *) theory MapSum use import int.Int use export Map (** [sum m l h] is the sum of [m[i]] for [l <= i < h] *) type container = map int int clone export sum.Sum with type container = container, function f = get end (** {2 Bitvectors (arbitrary length)} Seen as maps from int to bool *) theory BitVector use export bool.Bool use import int.Int constant size : int type bv function nth bv int: bool constant bvzero : bv axiom Nth_zero: forall n:int. 0 <= n < size -> nth bvzero n = False constant bvone : bv axiom Nth_one: forall n:int. 0 <= n < size -> nth bvone n = True predicate eq (v1 v2 : bv) = forall n:int. 0 <= n < size -> nth v1 n = nth v2 n function bw_and (v1 v2 : bv) : bv axiom Nth_bw_and: forall v1 v2:bv, n:int. 0 <= n < size -> nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n) (** logical shift right *) function lsr bv int : bv axiom Lsr_nth_low: forall b:bv,n s:int. 0 <= n+s < size -> nth (lsr b s) n = nth b (n+s) axiom Lsr_nth_high: forall b:bv,n s:int. n+s >= size -> nth (lsr b s) n = False (** arithmetic shift right *) function asr bv int : bv axiom Asr_nth_low: forall b:bv,n s:int. 0 <= n+s < size -> nth (asr b s) n = nth b (n+s) axiom Asr_nth_high: forall b:bv,n s:int. n+s >= size -> nth (asr b s) n = nth b (size-1) (** logical shift left *) function lsl bv int : bv axiom Lsl_nth_high: forall b:bv,n s:int. 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s) axiom Lsl_nth_low: forall b:bv,n s:int. n-s < 0 -> nth (lsl b s) n = False end (** {2 32-bits Bitvectors} *) theory BV32 constant size : int = 32 clone export BitVector with constant size = size end