more coercions used in mach.* modules

parent f5f8599c
......@@ -15,91 +15,91 @@ module Array32
type array 'a = private {
mutable ghost elts : int -> 'a;
length : int32;
} invariant { 0 <= to_int length }
} invariant { 0 <= length }
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int32) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int32)
ensures { 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: int32) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: int32) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. 0 <= i < to_int n -> result[i] = v }
requires { "expl:array creation size" n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
ensures { result.length = n }
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
ensures { result.length = a1.length + a2.length }
ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < a2.length ->
result[a1.length + i] = a2[i] }
val sub (a: array 'a) (ofs: int32) (len: int32) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
ensures { forall i:int. 0 <= i < len ->
result[i] = a[ofs + i] }
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] }
val fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a) : unit writes {a}
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
(0 <= i < ofs \/
ofs + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. ofs <= i < ofs + len ->
a[i] = v }
val blit (a1: array 'a) (ofs1: int32)
(a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
requires { 0 <= to_int ofs2 /\
to_int ofs2 + to_int len <= to_int a2.length }
requires { 0 <= ofs1 /\ 0 <= len }
requires { ofs1 + len <= a1.length }
requires { 0 <= ofs2 /\
ofs2 + len <= a2.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a2.length) ->
(0 <= i < ofs2 \/
ofs2 + len <= i < a2.length) ->
a2[i] = (old a2)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a2[i] = a1[ofs1 + i - ofs2] }
val self_blit (a: array 'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
requires { 0 <= ofs1 /\ 0 <= len /\
ofs1 + len <= a.length }
requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
(0 <= i < ofs2 \/
ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a[i] = (old a)[ofs1 + i - ofs2] }
end
......@@ -114,91 +114,91 @@ module Array31
type array 'a = private {
mutable ghost elts : int -> 'a;
length : int31;
} invariant { 0 <= to_int length }
} invariant { 0 <= length }
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int31) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: int31) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int31)
ensures { 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: int31) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: int31) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. 0 <= i < to_int n -> result[i] = v }
requires { "expl:array creation size" n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
ensures { result.length = n }
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
ensures { result.length = a1.length + a2.length }
ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < a2.length ->
result[a1.length + i] = a2[i] }
val sub (a: array 'a) (ofs: int31) (len: int31) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
ensures { forall i:int. 0 <= i < len ->
result[i] = a[ofs + i] }
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] }
val fill (a: array 'a) (ofs: int31) (len: int31) (v: 'a) : unit
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
(0 <= i < ofs \/
ofs + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. ofs <= i < ofs + len ->
a[i] = v }
val blit (a1: array 'a) (ofs1: int31)
(a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
requires { 0 <= to_int ofs2 /\
to_int ofs2 + to_int len <= to_int a2.length }
requires { 0 <= ofs1 /\ 0 <= len }
requires { ofs1 + len <= a1.length }
requires { 0 <= ofs2 /\
ofs2 + len <= a2.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a2.length) ->
(0 <= i < ofs2 \/
ofs2 + len <= i < a2.length) ->
a2[i] = (old a2)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a2[i] = a1[ofs1 + i - ofs2] }
val self_blit (a: array 'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
requires { 0 <= ofs1 /\ 0 <= len /\
ofs1 + len <= a.length }
requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
(0 <= i < ofs2 \/
ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a[i] = (old a)[ofs1 + i - ofs2] }
end
......@@ -213,92 +213,92 @@ module Array63
type array 'a = private {
mutable ghost elts : int -> 'a;
length : int63;
} invariant { 0 <= to_int length }
} invariant { 0 <= length }
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int63) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: int63) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
requires { "expl:index in array bounds" 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int63)
ensures { 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: int63) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: int63) (v: 'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. 0 <= i < to_int n -> result[i] = v }
requires { "expl:array creation size" n >= 0 }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
ensures { result.length = n }
val append (a1: array 'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
ensures { result.length = a1.length + a2.length }
ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < a2.length ->
result[a1.length + i] = a2[i] }
val sub (a: array 'a) (ofs: int63) (len: int63) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
ensures { forall i:int. 0 <= i < len ->
result[i] = a[ofs + i] }
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] }
val fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a) : unit
writes { a }
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
(0 <= i < ofs \/
ofs + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. ofs <= i < ofs + len ->
a[i] = v }
val blit (a1: array 'a) (ofs1: int63)
(a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
requires { 0 <= to_int ofs2 /\
to_int ofs2 + to_int len <= to_int a2.length }
requires { 0 <= ofs1 /\ 0 <= len }
requires { ofs1 + len <= a1.length }
requires { 0 <= ofs2 /\
ofs2 + len <= a2.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a2.length) ->
(0 <= i < ofs2 \/
ofs2 + len <= i < a2.length) ->
a2[i] = (old a2)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a2[i] = a1[ofs1 + i - ofs2] }
val self_blit (a: array 'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
requires { 0 <= ofs1 /\ 0 <= len /\
ofs1 + len <= a.length }
requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
(0 <= i < ofs2 \/
ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
ofs2 <= i < ofs2 + len ->
a[i] = (old a)[ofs1 + i - ofs2] }
end
......
......@@ -99,14 +99,14 @@ module Bounded_int
use import int.ComputerDivision
val (/) (a:t) (b:t) : t
requires { "expl:division by zero" to_int b <> 0 }
requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) }
ensures { to_int result = div (to_int a) (to_int b) }
requires { "expl:division by zero" b <> 0 }
requires { "expl:integer overflow" in_bounds (div a b) }
ensures { result = div a b }
val (%) (a:t) (b:t) : t
requires { "expl:division by zero" to_int b <> 0 }
requires { "expl:integer overflow" in_bounds (mod (to_int a) (to_int b)) }
ensures { to_int result = mod (to_int a) (to_int b) }
requires { "expl:division by zero" b <> 0 }
requires { "expl:integer overflow" in_bounds (mod a b) }
ensures { result = mod a b }
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment