Why3 Standard Library index

```
```

# Theory of maps

```
```

## Generic Maps

```
theory Map

type map 'a 'b

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

```

## Sorted Maps (indexed by integers)

```
theory MapSorted

use import int.Int
use import Map

type elt

predicate le elt elt

(* a[l..u) is sorted for le *)
predicate sorted_sub (a : map int elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]

end

```

## Maps Equality (indexed by integers)

```theory MapEq

use import int.Int
use export Map

predicate map_eq_sub (a1 a2 : map int 'a) (l u : int) =
forall i:int. l <= i < u -> a1[i] = a2[i]

end

```

## 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]

predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)

predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n

lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n

end

```

## Map Permutation (indexed by integers)

```theory MapPermut

use import int.Int
use export Map

predicate exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] /\ a2[i] = a1[j] /\
forall k:int. (k <> i /\ k <> j) -> a1[k] = a2[k]

lemma exchange_set :
forall a : map int 'a. forall i j : int.
exchange a a[i <- a[j]][j <- a[i]] i j

inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl :
forall a : map int 'a. forall l u : int. permut_sub a a l u
| permut_sym :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
| permut_trans :
forall a1 a2 a3 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a3 l u -> permut_sub a1 a3 l u
| permut_exchange :
forall a1 a2 : map int 'a. forall l u i j : int.
l <= i < u -> l <= j < u -> exchange a1 a2 i j -> permut_sub a1 a2 l u

lemma permut_weakening :
forall a1 a2 : map int 'a. forall l1 r1 l2 r2 : int.
l1 <= l2 <= r2 <= r1 -> permut_sub a1 a2 l2 r2 -> permut_sub a1 a2 l1 r1

lemma permut_eq :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u ->
forall i:int. (i < l \/ u <= i) -> a2[i] = a1[i]

lemma permut_exists :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u ->
forall i : int. l <= i < u ->
exists j : int. l <= j < u /\ a2[i] = a1[j]

end

```

## 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

```

## 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

```

## 32-bits Bitvectors

```
theory BV32

constant size : int = 32

clone export BitVector with constant size = size

end
```

Generated by why3doc 0.81