//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
package chalice;
object TranslatorPrelude {
val P =
"""// Copyright (c) 2008, Microsoft
type Field a;
type HeapType = [ref,Field a]a;
type MaskType = [ref,Field a][PermissionComponent]int;
type CreditsType = [ref]int;
type ref;
const null: ref;
var Heap: HeapType;
type PermissionComponent;
const unique perm$R: PermissionComponent;
const unique perm$N: PermissionComponent;
const Permission$MinusInfinity: int;
axiom Permission$MinusInfinity < -10000;
const Permission$PlusInfinity: int;
axiom 10000 < Permission$PlusInfinity;
var Mask: MaskType where IsGoodMask(Mask);
const Permission$Zero: [PermissionComponent]int;
axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;
const Permission$Full: [PermissionComponent]int;
axiom Permission$Full[perm$R] == 100 && Permission$Full[perm$N] == 0;
const ZeroMask: MaskType;
axiom (forall o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);
axiom IsGoodMask(ZeroMask);
function {:expand false} CanRead(m: MaskType, obj: ref, f: Field T) returns (bool)
{
0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
}
function {:expand false} CanWrite(m: MaskType, obj: ref, f: Field T) returns (bool)
{
m[obj,f][perm$R] == 100 && m[obj,f][perm$N] == 0
}
function {:expand true} IsGoodMask(m: MaskType) returns (bool)
{
(forall o: ref, f: Field T ::
0 <= m[o,f][perm$R] &&
(NonPredicateField(f) ==>
(m[o,f][perm$R]<=100 &&
(0 < m[o,f][perm$N] ==> m[o,f][perm$R] < 100))) &&
(m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
}
var Credits: CreditsType;
function IsGoodState(T) returns (bool);
function combine(T, U) returns (T);
const nostate: HeapType;
axiom (forall a: T, b: U :: {IsGoodState(combine(a, b))} IsGoodState(combine(a, b)) <==> IsGoodState(a) && IsGoodState(b));
axiom IsGoodState(nostate);
type ModuleName;
const CurrentModule: ModuleName;
type TypeName;
function dtype(ref) returns (TypeName);
const CanAssumeFunctionDefs: bool;
type Mu;
const unique mu: Field Mu;
axiom NonPredicateField(mu);
function MuBelow(Mu, Mu) returns (bool); // strict partial order
axiom (forall m: Mu, n: Mu ::
{ MuBelow(m,n), MuBelow(n,m) }
!(MuBelow(m,n) && MuBelow(n,m)));
axiom (forall m: Mu, n: Mu, o: Mu ::
{ MuBelow(m,n), MuBelow(n,o) }
MuBelow(m,n) && MuBelow(n,o) ==> MuBelow(m,o));
const $LockBottom: Mu;
axiom (forall m, n: Mu :: MuBelow(m, n) ==> n != $LockBottom);
const unique held: Field int;
function Acquire$Heap(int) returns (HeapType);
function Acquire$Mask(int) returns (MaskType);
function Acquire$Credits(int) returns (CreditsType);
axiom NonPredicateField(held);
function LastSeen$Heap(Mu, int) returns (HeapType);
function LastSeen$Mask(Mu, int) returns (MaskType);
function LastSeen$Credits(Mu, int) returns (CreditsType);
const unique rdheld: Field bool;
axiom NonPredicateField(rdheld);
function wf(h: HeapType, m: MaskType) returns (bool);
function IsGoodInhaleState(ih: HeapType, h: HeapType,
m: MaskType) returns (bool)
{
(forall o: ref, f: Field T :: { ih[o, f] } CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&
(forall o: ref :: { ih[o, held] } (0 ih[o, mu] == h[o, mu]) &&
(forall o: ref :: { h[o, rdheld] } h[o, rdheld] ==> ih[o, mu] == h[o, mu])
}
// ---------------------------------------------------------------
// -- If then else -----------------------------------------------
// ---------------------------------------------------------------
function ite(bool, T, T) returns (T);
axiom (forall con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
axiom (forall con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
type Seq T;
function Seq#Length(Seq T) returns (int);
axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
function Seq#Empty() returns (Seq T);
axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0);
axiom (forall s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
function Seq#Singleton(T) returns (Seq T);
axiom (forall t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
function Seq#Build(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
axiom (forall s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }
0 <= len ==> Seq#Length(Seq#Build(s,i,v,len)) == len);
function Seq#Append(Seq T, Seq T) returns (Seq T);
axiom (forall s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
function Seq#Index(Seq T, int) returns (T);
axiom (forall t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
(n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
(Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
axiom (forall s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }
0 <= n && n < len ==>
(i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
(i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
function Seq#Contains(Seq T, T) returns (bool);
axiom (forall s: Seq T, x: T :: { Seq#Contains(s,x) }
Seq#Contains(s,x) <==>
(exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
axiom (forall x: ref ::
{ Seq#Contains(Seq#Empty(), x) }
!Seq#Contains(Seq#Empty(), x));
axiom (forall 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 s: Seq T, i: int, v: T, len: int, x: T ::
{ Seq#Contains(Seq#Build(s, i, v, len), x) }
Seq#Contains(Seq#Build(s, i, v, len), x) <==>
(0 <= i && i < len && x == v) ||
(exists j: int :: { Seq#Index(s,j) } 0 <= j && j < Seq#Length(s) && j < len && j!=i && Seq#Index(s,j) == x));
axiom (forall s: Seq T, n: int, x: T ::
{ Seq#Contains(Seq#Take(s, n), x) }
Seq#Contains(Seq#Take(s, n), x) <==>
(exists i: int :: { Seq#Index(s, i) }
0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
axiom (forall s: Seq T, n: int, x: T ::
{ Seq#Contains(Seq#Drop(s, n), x) }
Seq#Contains(Seq#Drop(s, n), x) <==>
(exists i: int :: { Seq#Index(s, i) }
0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
function Seq#Equal(Seq T, Seq T) returns (bool);
axiom (forall s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
Seq#Equal(s0,s1) <==>
Seq#Length(s0) == Seq#Length(s1) &&
(forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
axiom(forall a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
Seq#Equal(a,b) ==> a == b);
function Seq#SameUntil(Seq T, Seq T, int) returns (bool);
axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
Seq#SameUntil(s0,s1,n) <==>
(forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
function Seq#Take(s: Seq T, howMany: int) returns (Seq T);
axiom (forall 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)));
axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}
0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
function Seq#Drop(s: Seq T, howMany: int) returns (Seq T);
axiom (forall 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));
axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}
0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
axiom (forall s, t: Seq T ::
{ Seq#Append(s, t) }
Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
function Seq#Range(min: int, max: int) returns (Seq int);
axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j Seq#Index(Seq#Range(min, max), j) == min + j);
// ---------------------------------------------------------------
// -- Permissions ------------------------------------------------
// ---------------------------------------------------------------
axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);
function DecPerm(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
axiom (forall m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
);
function DecEpsilons(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
axiom (forall m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
);
function IncPerm(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
axiom (forall m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
);
function IncEpsilons(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
axiom (forall m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
);
function Havocing(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
axiom (forall h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
);
const unique joinable: Field int;
axiom NonPredicateField(joinable);
const unique token#t: TypeName;
function Call$Heap(int) returns (HeapType);
function Call$Mask(int) returns (MaskType);
function Call$Credits(int) returns (CreditsType);
function Call$Args(int) returns (ArgSeq);
type ArgSeq = [int]T;
function EmptyMask(m: MaskType) returns (bool);
axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
const ZeroCredits: CreditsType;
axiom (forall o: ref :: ZeroCredits[o] == 0);
function EmptyCredits(c: CreditsType) returns (bool);
axiom (forall c: CreditsType :: {EmptyCredits(c)} EmptyCredits(c) <==> (forall o: ref :: o != null ==> c[o] == 0));
function NonPredicateField(f: Field T) returns (bool);
function PredicateField(f: Field T) returns (bool);
axiom (forall f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
axiom (forall f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
function submask(m1: MaskType, m2: MaskType) returns (bool);
axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
submask(m1, m2) <==> (forall o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
);
// ---------------------------------------------------------------
// -- Arithmetic -------------------------------------------------
// ---------------------------------------------------------------
// the connection between % and /
axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
// sign of denominator determines sign of remainder
axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0);
// the following axiom has some unfortunate matching, but it does state a property about % that
// is sometime useful
axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
// ---------------------------------------------------------------
// -- End of prelude ---------------------------------------------
// ---------------------------------------------------------------
"""
}