Various DafnyPrelude.bpl cleanup.

Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments

1 files changed, 4 insertions, 124 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index eea23383..6ddff694 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -103,21 +103,6 @@ const $ArbitraryBoxValue: Box;
 function $Box<T>(T): Box;

 function $Unbox<T>(Box): T;

 

-/*

-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

-axiom (forall b: Box :: { $Unbox(b): int } $Box($Unbox(b): int) == b);

-axiom (forall b: Box :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);

-axiom (forall b: Box :: { $Unbox(b): Set Box } $Box($Unbox(b): Set Box) == b);

-axiom (forall b: Box :: { $Unbox(b): MultiSet Box } $Box($Unbox(b): MultiSet Box) == b);

-axiom (forall b: Box :: { $Unbox(b): Seq Box } $Box($Unbox(b): Seq Box) == b);

-axiom (forall b: Box :: { $Unbox(b): Map Box Box } $Box($Unbox(b): Map Box Box) == b);

-axiom (forall b: Box :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);

-// Note: an axiom like this for bool would not be sound; instead, we do:

-function $IsCanonicalBoolBox(Box): bool;

-axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));

-axiom (forall b: Box :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);

-*/

-

 axiom (forall<T> x : T :: { $Box(x) } $Unbox($Box(x)) == x);

 

 axiom (forall bx : Box ::

@@ -255,7 +240,6 @@ const unique class._System.seq: ClassName;
 const unique class._System.multiset: ClassName;

 

 function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty

-// function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;

 

 function TypeTuple(a: ClassName, b: ClassName): ClassName;

 function TypeTupleCar(ClassName): ClassName;

@@ -275,10 +259,6 @@ type HandleType;
 

 type DatatypeType;

 

-// function /*{:never_pattern true}*/ DtType(DatatypeType): Ty;  // the analog of dtype for datatype values

-                                                // changed from ClassName to Ty

-// function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName;  // the analog of TypeParams

-

 type DtCtorId;

 function DatatypeCtorId(DatatypeType): DtCtorId;

 

@@ -358,91 +338,6 @@ axiom(forall h, k : Heap, bx : Box, t : Ty ::
 const unique alloc: Field bool;

 axiom FDim(alloc) == 0 && !$IsGhostField(alloc);  // treat as non-ghost field, because it cannot be changed by ghost code

 

-// DtAlloc, removed

-//function DtAlloc(DatatypeType, Heap): bool;

-//axiom (forall h, k: Heap, d: DatatypeType ::

-//  { $HeapSucc(h, k), DtAlloc(d, h) }

-//  $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));

-

-// GenericAlloc removed.

-

-/*

-function GenericAlloc(Box, Heap): bool;

-axiom (forall h: Heap, k: Heap, d: Box ::

-  { $HeapSucc(h, k), GenericAlloc(d, h) }

-  $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));

-// GenericAlloc ==>

-//references

-axiom (forall b: Box, h: Heap ::

-  { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }

-  GenericAlloc(b, h) ==>

-  $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);

-//seqs

-axiom (forall b: Box, h: Heap, i: int ::

-  { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq Box, i) }

-  GenericAlloc(b, h) &&

-  0 <= i && i < Seq#Length($Unbox(b): Seq Box) ==>

-  GenericAlloc( Seq#Index($Unbox(b): Seq Box, i), h ) );

-

-//maps

-//seq-like axiom, talking about the range elements

-axiom (forall b: Box, h: Heap, i: Box ::

-  { GenericAlloc(b, h), Map#Domain($Unbox(b): Map Box Box)[i] }

-  GenericAlloc(b, h) && Map#Domain($Unbox(b): Map Box Box)[i] ==>

-  GenericAlloc( Map#Elements($Unbox(b): Map Box Box)[i], h ) );

-//set-like axiom, talking about the domain elements

-axiom (forall b: Box, h: Heap, t: Box ::

-  { GenericAlloc(b, h), Map#Domain($Unbox(b): Map Box Box)[t] }

-  GenericAlloc(b, h) && Map#Domain($Unbox(b): Map Box Box)[t] ==>

-  GenericAlloc(t, h));

-

-//sets

-axiom (forall b: Box, h: Heap, t: Box ::

-  { GenericAlloc(b, h), ($Unbox(b): Set Box)[t] }

-  GenericAlloc(b, h) && ($Unbox(b): Set Box)[t] ==>

-  GenericAlloc(t, h));

-//datatypes

-axiom (forall b: Box, h: Heap ::

-  { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }

-  GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));

-axiom (forall dt: DatatypeType, h: Heap ::

-  { GenericAlloc($Box(dt), h) }

-  GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h));

-// ==> GenericAlloc

-axiom (forall b: bool, h: Heap ::

-  $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));

-axiom (forall x: int, h: Heap ::

-  $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));

-axiom (forall r: ref, h: Heap ::

-  { GenericAlloc($Box(r), h) }

-  $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));

-// boxes in the heap

-axiom (forall r: ref, f: Field Box, h: Heap ::

-  { GenericAlloc(read(h, r, f), h) }

-  $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>

-  GenericAlloc(read(h, r, f), h));

-

-axiom (forall h: Heap, r: ref, j: int ::

- { read(h, r, IndexField(j)) }

- $IsGoodHeap(h) && r != null && read(h, r, alloc) &&

- 0 <= j && j < _System.array.Length(r)

- ==>

- GenericAlloc(read(h, r, IndexField(j)), h));

-axiom (forall h: Heap, r: ref, m: Field Box, j: int ::

- { read(h, r, MultiIndexField(m, j)) }

- $IsGoodHeap(h) && r != null && read(h, r, alloc)

- // It would be best also to constrain MultiIndexField(m,j) to produce

- // a proper field (that is, to refer to an array element within

- // bounds.  However, since the LengthX fields of multi-dimentional

- // are produced on the fly, adding them would require more work.

- // Thus, the model to keep in mind is that MultiIndexField then

- // produces a field who value, when dereferenced for array 'r',

- // is a box that has the desired allocation properties.

- ==>

- GenericAlloc(read(h, r, MultiIndexField(m, j)), h));

- */

-

-

 // ---------------------------------------------------------------

 // -- Arrays -----------------------------------------------------

 // ---------------------------------------------------------------

@@ -558,10 +453,6 @@ axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
 axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

 axiom (forall<T> r: T :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1);

 

-// the singleton set will be the same type as its box

-//axiom (forall bx : Ty, t: Ty :: { $Is(Set#Singleton(

-

-

 function Set#UnionOne<T>(Set T, T): Set T;

 axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }

   Set#UnionOne(a,x)[o] <==> o == x || a[o]);

@@ -832,12 +723,13 @@ axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
 axiom (forall x: ref ::

   { Seq#Contains(Seq#Empty(), x) }

   !Seq#Contains(Seq#Empty(), x));

+

 axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::

   { Seq#Contains(Seq#Append(s0, s1), x) }

   Seq#Contains(Seq#Append(s0, s1), x) <==>

     Seq#Contains(s0, x) || Seq#Contains(s1, x));

 

-axiom (forall<T> s: Seq T, v: T, x: T ::

+axiom (forall<T> s: Seq T, v: T, x: T ::  // needed to prove things like '4 in [2,3,4]', see method TestSequences0 in SmallTests.dfy

   { Seq#Contains(Seq#Build(s, v), x) }

     Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x)));

 

@@ -869,9 +761,7 @@ axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
 

 function Seq#Take<T>(s: Seq T, howMany: int): Seq T;

 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }

-  0 <= n ==>

-    (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

-    (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

+  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n);

 axiom (forall<T> s: Seq T, n: int, j: int ::

   {:weight 25}

   { Seq#Index(Seq#Take(s,n), j) }

@@ -881,9 +771,7 @@ axiom (forall<T> s: Seq T, n: int, j: int ::
 

 function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;

 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }

-  0 <= n ==>

-    (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

-    (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

+  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n);

 axiom (forall<T> s: Seq T, n: int, j: int ::

   {:weight 25}

   { Seq#Index(Seq#Drop(s,n), j) }

@@ -926,14 +814,6 @@ axiom (forall h0, h1: Heap, a: ref ::
 axiom (forall h: Heap, i: int, v: Box, a: ref ::

   { Seq#FromArray(update(h, a, IndexField(i), v), a) }

     0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );

-/**** Someday:

-axiom (forall h: Heap, a: ref :: { Seq#FromArray(h, a) }

-    $IsGoodHeap(h) &&

-    a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool

-    ==>

-    (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }

-      0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==>  $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));

-****/

 

 // Commutability of Take and Drop with Update.

 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::