//
// Copyright (c) Microsoft Corporation.  All rights reserved.
//

/*****************************************************************************
******************************************************************************
**** AXIOMS AND TRUSTED DEFINITIONS
******************************************************************************
*****************************************************************************/

//////////////////////////////////////////////////////////////////////////////
// TRIGGERS
//////////////////////////////////////////////////////////////////////////////

// Triggers for quantifiers
// We could use a single trigger for all values; the distinction between the
// various triggers below is just to help the prover run fast.

// TV is a trigger for values in general, including addresses.
function{:expand false} TV(val:int) returns (bool) { true }

// TO is a trigger specifically for word offsets from addresses, where
// word offset n is byte offset 4 * n.
function{:expand false} TO(wordOffset:int) returns (bool) { true }

// TSlot is a trigger for slots in sparse tags
function{:expand false} TSlot(slot:int) returns (bool) { true }

// TT is a trigger for tables
function{:expand false} TT(table:int) returns (bool) { true }

//////////////////////////////////////////////////////////////////////////////
// WORDS
//////////////////////////////////////////////////////////////////////////////

// i1 <= x < i2
function between(i1:int, i2:int, x:int) returns(bool) { i1 <= x && x < i2 }

// valid 32-bit unsigned words
// word(i) <==> 0 <= i < 2^32
const WORD_HI:int; // 2^32
axiom WORD_HI >= 100; // REVIEW: should we go ahead and set WORD_HI to exactly 2^32?
function word(val:int) returns(bool) { 0 <= val && val < WORD_HI }

// converts 2's complement 32-bit val into signed integer
function asSigned(val:int) returns(int);

// null value(s)
const NULL: int; axiom NULL == 0;

//////////////////////////////////////////////////////////////////////////////
// ASSEMBLY LANGUAGE
//////////////////////////////////////////////////////////////////////////////

// invariant: word(r) for each register r
// To maintain invariant, simply check word(exp) for each assignment r := exp

// invariant: word(r) for each word w in memory
// To maintain invariant, simply check word(exp) for each store of exp to memory

var eax:int;
var ebx:int;
var ecx:int;
var edx:int;
var esi:int;
var edi:int;
var ebp:int;
var esp:int;

function neg (int) returns (int);
function and (int, int) returns (int);
function or (int, int) returns (int);
function xor (int, int) returns (int);
function shl (int, int) returns (int);
function shr (int, int) returns (int);

function{:expand false} TVM(a:int, b:int) returns(bool) { true }
function Mult(a:int, b:int) returns(int);
axiom (forall a:int, b:int::{TVM(a, b)} Mult(a, b) == a * b);

// REVIEW: one would hope that this axiom is derivable from
// Mult(a, b) == a * b, using b = b1 + b2, but Z3 couldn't seem to do it yet:
function{:expand false} TVM3(a:int, b1:int, b2:int) returns(bool) { true }
axiom (forall a:int, b1:int, b2:int::{TVM3(a, b1, b2)} Mult(a, b1 + b2) == a * (b1 + b2));

procedure Add(x:int, y:int) returns(ret:int);
  requires word(x + y);
  ensures  ret == x + y;

procedure Sub(x:int, y:int) returns(ret:int);
  requires word(x - y);
  ensures  ret == x - y;

procedure Mul(x:int, y:int) returns(ret:int, hi:int);
  requires word(x * y);
  ensures  ret == x * y;
  ensures  ret == Mult(x, y);

// Note: we only support 32-bit division, so the upper 32 bits must be 0
procedure Div(x:int, zero:int, y:int) returns(ret:int, rem:int);
  requires zero == 0;
  requires y != 0;
  ensures  word(ret);
  ensures  word(rem);
  ensures  ret == x / y && ret * y + rem == x;
  ensures  rem == x % y && rem < y;

procedure Not(x:int) returns(ret:int);
  ensures  ret == neg(x);
  ensures  word(ret);

procedure And(x1:int, x2:int) returns(ret:int);
  ensures  ret == and(x1, x2);
  ensures  word(ret);

procedure Or(x1:int, x2:int) returns(ret:int);
  ensures  ret == or(x1, x2);
  ensures  word(ret);

procedure Xor(x1:int, x2:int) returns(ret:int);
  ensures  ret == xor(x1, x2);
  ensures  word(ret);

procedure Shl(x1:int, x2:int) returns(ret:int);
  requires x2 < 32;
  ensures  ret == shl(x1, x2);
  ensures  word(ret);

procedure Shr(x1:int, x2:int) returns(ret:int);
  requires x2 < 32;
  ensures  ret == shr(x1, x2);
  ensures  word(ret);

// run-time overflow checked
procedure AddChecked(x:int, y:int) returns(ret:int);
  ensures  word(x + y);
  ensures  ret == x + y;

// run-time overflow checked
procedure SubChecked(x:int, y:int) returns(ret:int);
  ensures  word(x - y);
  ensures  ret == x - y;

// run-time overflow checked
procedure MulChecked(x:int, y:int) returns(ret:int, hi:int);
  ensures  word(x * y);
  ensures  word(Mult(x, y));
  ensures  ret == x * y;
  ensures  ret == Mult(x, y);

procedure Lea(addr:int) returns(ret:int);
  requires word(addr);
  ensures  ret == addr;

procedure LeaUnchecked(addr:int) returns(ret:int);
  ensures  word(ret);

// REVIEW: add more general support for signed arithmetic?
procedure LeaSignedIndex(base:int, scale:int, index:int, offset:int) returns(ret:int);
  requires scale == 1 || scale == 2 || scale == 4 || scale == 8;
  requires word(base + scale * asSigned(index) + offset);
  ensures  ret == base + scale * asSigned(index) + offset;

procedure DebugBreak();
  ensures false; // DebugBreak never returns.

//////////////////////////////////////////////////////////////////////////////
// READ-ONLY MEMORY
//////////////////////////////////////////////////////////////////////////////

function roS8(ptr:int) returns(int);
function roU8(ptr:int) returns(int);
function roS16(ptr:int) returns(int);
function roU16(ptr:int) returns(int);
function ro32(ptr:int) returns(int);

function inRo(ptr:int, size:int) returns(bool);

// read and zero-extend 8 bits
procedure RoLoadU8(ptr:int) returns (val:int);
  requires inRo(ptr, 1);
  ensures  word(val);
  ensures  val == roU8(ptr);

// read and sign-extend 8 bits
procedure RoLoadS8(ptr:int) returns (val:int);
  requires inRo(ptr, 1);
  ensures  word(val);
  ensures  asSigned(val) == roS8(ptr);

// read and zero-extend 16 bits
procedure RoLoadU16(ptr:int) returns (val:int);
  requires inRo(ptr, 2);
  ensures  word(val);
  ensures  val == roU16(ptr);

// read and sign-extend 16 bits
procedure RoLoadS16(ptr:int) returns (val:int);
  requires inRo(ptr, 2);
  ensures  word(val);
  ensures  asSigned(val) == roS16(ptr);

procedure RoLoad32(ptr:int) returns (val:int);
  requires inRo(ptr, 4);
  ensures  word(val);
  ensures  val == ro32(ptr);

//////////////////////////////////////////////////////////////////////////////
// GC-CONTROLLED MEMORY
//////////////////////////////////////////////////////////////////////////////

// valid gc-controlled addresses (must be disjoint from null values)
// warning: because of interior pointers, ?gcHi must be a 32-bit word
//   (it can equal 2^32 - 1, but not 2^32)
const ?gcLo: int;
const ?gcHi: int;
axiom NULL < ?gcLo;
axiom ?gcLo <= ?gcHi;
axiom ?gcHi < WORD_HI;
function gcAddr(i:int) returns (bool) {?gcLo <= i && i < ?gcHi}
function gcAddrEx(i:int) returns (bool) {?gcLo <= i && i <= ?gcHi}

// Aligned(i) <==> i is a multiple of 4
function Aligned(i:int) returns(bool);
axiom (forall i:int, j:int::{TV(i), TO(j)} TV(i) && TO(j) ==> Aligned(i) == Aligned(i + 4 * j));
axiom Aligned(?gcLo);
axiom Aligned(?gcHi);

// $GcMem[i] = data at address i, if gcAddr(i) and Aligned(i).
var $GcMem:[int]int; // Do not modify directly! Use procedures below.

// Read a word from gc-controlled memory
procedure GcLoad(ptr:int) returns (val:int);
  requires TV(ptr);
  requires gcAddr(ptr);
  requires Aligned(ptr);
  ensures  word(val);
  ensures  TV(val);
  ensures  val == $GcMem[ptr];

// Write a word to gc-controlled memory
procedure GcStore(ptr:int, val:int);
  requires gcAddr(ptr);
  requires Aligned(ptr);
  requires word(val);
  requires TV(ptr) && TV(val);
  modifies $GcMem;
  ensures  $GcMem == old($GcMem)[ptr := val];

// MAP_ZERO maps all addresses to value zero.
const MAP_ZERO:[int]int;
axiom (forall i:int::{TV(i)} TV(i) ==> MAP_ZERO[i] == 0);

//////////////////////////////////////////////////////////////////////////////
// ABSTRACT NODES
//////////////////////////////////////////////////////////////////////////////

// The mutator controls an abstract graph consisting of abstract nodes,
// which contain abstract values.  These abstract values may be
// abstract primitive values or abstract edges pointing to abstract nodes.

// Abstract values are represented by integers.  For any integer A,
// we may interpret A as an abstract primitive value or an abstract pointer:
//   - the abstract primitive value A represents the concrete integer A
//   - the abstract pointer A may be one of the following:
//     - NO_ABS, representing no value (used for partial maps)
//     - any other value, representing a node in the abstract graph
// Any primitive value A will satisfy word(A). To avoid confusion
// between abstract primitive and abstract pointer values, the
// mutator should choose abstract pointer values A such that !word(A).

const NO_ABS:int; // the value "none"

// Each abstract object node A has some number of fields,
// which is chosen when A is allocated, and never changes afterwards.
function numFields(abs:int) returns (int);

// $AbsMem represents of the abstract graph's edges: for abstract node A
// and field j, $AbsMem[A][j] is the abstract node pointed to by A's field j.
// Do not modify $AbsMem directly!  $AbsMem is controlled by the mutator.
var $AbsMem:[int][int]int;

//////////////////////////////////////////////////////////////////////////////
// REACHABILITY
//////////////////////////////////////////////////////////////////////////////

type Time;
var $Time:Time;

// reached(A,T) means that the GC has reached abstract node A at some time
// after the initial time T.  Initially (at time T), the mutator will
// say that reached(root, T).  After that, the GC calls the "reach"
// ghost procedure to generate reached(A, T) for other A.
function reached(a:int, t:Time) returns (bool);

// If we've reached A, and A points to A', then reach A'.
// Note: this depends on $AbsMem being defined by the mutator.  The GC
// should not write to $AbsMem directly (if it did, then it could reach
// anything, trivially).
procedure reach($a:int, $j:int, $t:Time);
  requires reached($a, $t);
  requires $AbsMem[$a][$j] != NO_ABS;
  ensures  reached($AbsMem[$a][$j], $t);

//////////////////////////////////////////////////////////////////////////////
// POINTERS AND VALUES
//////////////////////////////////////////////////////////////////////////////

function Pointer(rev:[int]int, ptr:int, abs:int) returns (bool)
{
  gcAddr(ptr) && Aligned(ptr) && abs != NO_ABS && rev[ptr] == abs // AbsMapped(ptr,rev,abs)
}

// An interior pointer ("interiorPtr") points to an actual
// object address ("ptr") plus some offset ("offset"):
//   !nullAddr(interiorPtr) ==> interiorPtr == ptr + offset && 0 <= offset && offset <= 4 * numFields($toAbs[ptr - 4]) - 4;
function InteriorValue(isPtr:bool, rev:[int]int, val:int, abs:int, offset:int) returns (bool)
{
     (isPtr && word(val) && gcAddrEx(val) && Pointer(rev, val - 4 - offset, abs)
       && !word(abs)
       && 0 <= offset && offset <= 4 * numFields(abs) - 4)
  || (isPtr && word(val) && !gcAddrEx(val) && abs == val)
  || (!isPtr && word(val) && abs == val)
}

function Value(isPtr:bool, rev:[int]int, val:int, abs:int) returns (bool)
{
  InteriorValue(isPtr, rev, val, abs, 0)
}

//////////////////////////////////////////////////////////////////////////////
// BARTOK INTERFACE
//////////////////////////////////////////////////////////////////////////////

function getBit(x:int, i:int) returns(bool) { 1 == and(shr(x, i), 1) }
function getNib(x:int, i:int) returns(int) { and(shr(x, i), 15) }

const ?SPARSE_TAG:int;        axiom ?SPARSE_TAG              == 1;
const ?DENSE_TAG:int;         axiom ?DENSE_TAG               == 3;
const ?PTR_VECTOR_TAG:int;    axiom ?PTR_VECTOR_TAG          == 5;
const ?OTHER_VECTOR_TAG:int;  axiom ?OTHER_VECTOR_TAG        == 7;
const ?PTR_ARRAY_TAG:int;     axiom ?PTR_ARRAY_TAG           == 9;
const ?OTHER_ARRAY_TAG:int;   axiom ?OTHER_ARRAY_TAG         == 11;
const ?STRING_TAG:int;        axiom ?STRING_TAG              == 13;

function isOtherTag(t:int) returns(bool)
{
 !(
      t == ?SPARSE_TAG || t == ?DENSE_TAG
   || t == ?PTR_VECTOR_TAG || t == ?OTHER_VECTOR_TAG
   || t == ?PTR_ARRAY_TAG  || t == ?OTHER_ARRAY_TAG
   || t == ?STRING_TAG
  )
}

function isVarSize(t:int) returns(bool)
{
    t == ?PTR_VECTOR_TAG || t == ?OTHER_VECTOR_TAG
 || t == ?PTR_ARRAY_TAG  || t == ?OTHER_ARRAY_TAG
 || t == ?STRING_TAG
}

function isReadonlyField(t:int, j:int) returns(bool)
{
    (j == 1)
 || (t == ?PTR_VECTOR_TAG && j == 2)
 || (t == ?OTHER_VECTOR_TAG && j == 2)
 || (t == ?PTR_ARRAY_TAG && (j == 2 || j == 3))
 || (t == ?OTHER_ARRAY_TAG && (j == 2 || j == 3))
 || (t == ?STRING_TAG && j == 2)
}

const ?STRING_VTABLE:int;

const ?VT_MASK:int;                axiom ?VT_MASK == 60;
const ?VT_BASE_LENGTH:int;         axiom ?VT_BASE_LENGTH == 52;
const ?VT_ARRAY_ELEMENT_SIZE:int;  axiom ?VT_ARRAY_ELEMENT_SIZE == 44;
const ?VT_ARRAY_ELEMENT_CLASS:int; axiom ?VT_ARRAY_ELEMENT_CLASS == 40;
const ?VT_ARRAY_OF:int;            axiom ?VT_ARRAY_OF == 36;

function mask(vt:int) returns(int) { ro32(vt + ?VT_MASK) }
function tag(vt:int) returns(int) { and(mask(vt), 15) }
function baseLength(vt:int) returns(int) { ro32(vt + ?VT_BASE_LENGTH) }
function arrayElementSize(vt:int) returns(int) { ro32(vt + ?VT_ARRAY_ELEMENT_SIZE) }
function arrayElementClass(vt:int) returns(int) { ro32(vt + ?VT_ARRAY_ELEMENT_CLASS) }
function arrayOf(vt:int) returns(int) { ro32(vt + ?VT_ARRAY_OF) }

function baseWords(vt:int) returns(int) { shr(baseLength(vt), 2) }
function arrayElementWords(vt:int) returns(int) { shr(arrayElementSize(vt), 2) }

const ?TYPE_STRUCT:int; axiom ?TYPE_STRUCT == 3;

//  true ==> field j is pointer
// false ==> field j is primitive
function VFieldPtr(abs:int, f:int) returns(bool);

function fieldToSlot(vt:int, j:int) returns(k:int);

// field 0 is the first non-header field
function Sparse1(abs:int, vt:int, j:int, field:int) returns(bool)
{
    VFieldPtr(abs, j) == (fieldToSlot(vt, field) != 0)
 && (fieldToSlot(vt, field) != 0 ==> between(1, 8, fieldToSlot(vt, field))
     && getNib(mask(vt), 4 * fieldToSlot(vt, field)) - 1 == field)
}

function Sparse2(vt:int, nFields:int) returns(bool)
{
  (forall k:int::{TSlot(k)} TSlot(k) ==> 1 <= k && k < 8 && getNib(mask(vt), 4 * k) != 0 ==>
      between(0, nFields, getNib(mask(vt), 4 * k) - 1)
   && fieldToSlot(vt, getNib(mask(vt), 4 * k) - 1) == k)
}

function{:expand false} TVT(abs:int, vt:int) returns(bool) { true }
function VTable(abs:int, vt:int) returns(bool);
axiom (forall abs:int, vt:int::{TVT(abs, vt)} VTable(abs, vt) <==>
(
    !VFieldPtr(abs, 0) // REVIEW: is this redundant?
 && !VFieldPtr(abs, 1) // REVIEW: is this redundant?
 && (tag(vt) == ?DENSE_TAG ==> (forall j:int::{TO(j)} TO(j) ==> 2 <= j && j < numFields(abs) ==>
      VFieldPtr(abs, j) == (j < 30 && getBit(mask(vt), 2 + j))) // REVIEW: is the "j < 30" redundant?
    )
 && (tag(vt) == ?SPARSE_TAG ==>
        (forall j:int::{TO(j)} TO(j) ==> Sparse1(abs, vt, j, j - 2))
     && Sparse2(vt, numFields(abs) - 2)
    )
 && (tag(vt) == ?STRING_TAG ==>
      (forall j:int::{TO(j)} TO(j) ==> !VFieldPtr(abs, j))
    )
 && (tag(vt) == ?PTR_VECTOR_TAG ==>
        between(3, numFields(abs), baseWords(vt))
     && (forall j:int::{TO(j)} TO(j) ==> (baseWords(vt) <= j && j < numFields(abs) <==> VFieldPtr(abs, j)))
    )
 && (tag(vt) == ?OTHER_VECTOR_TAG ==>
        !VFieldPtr(abs, 2)
     && inRo(arrayElementClass(vt) + ?VT_MASK, 4) // REVIEW
     && between(3, numFields(abs), baseWords(vt))
     && (arrayOf(vt) != ?TYPE_STRUCT ==> (forall j:int::{TO(j)} TO(j) ==> !VFieldPtr(abs, j)))
     && (arrayOf(vt) == ?TYPE_STRUCT ==> !isVarSize(tag(arrayElementClass(vt))))
     && (arrayOf(vt) == ?TYPE_STRUCT && mask(arrayElementClass(vt)) == ?SPARSE_TAG ==>
          (forall j:int::{TO(j)} TO(j) ==> !VFieldPtr(abs, j))) // REVIEW: redundant
     && (arrayOf(vt) == ?TYPE_STRUCT && tag(arrayElementClass(vt)) == ?SPARSE_TAG ==>
            (forall j:int::{TO(j)} TO(j) ==>
                (VFieldPtr(abs, j) ==> baseWords(vt) <= j && j < numFields(abs))
             && (baseWords(vt) <= j && j < numFields(abs) ==>
                  (forall m:int::{TO(m)} TO(m) ==>
                    between(0, arrayElementWords(vt), j - Mult(arrayElementWords(vt), m) - baseWords(vt)) ==>
                        baseWords(vt) + Mult(arrayElementWords(vt), m) + arrayElementWords(vt) <= numFields(abs)
                     && Sparse1(abs, arrayElementClass(vt), j, j - Mult(arrayElementWords(vt), m) - baseWords(vt)))))
         && arrayElementWords(vt) >= 0
         && Sparse2(arrayElementClass(vt), arrayElementWords(vt)))
    )
 && (tag(vt) == ?PTR_ARRAY_TAG ==>
        between(4, numFields(abs), baseWords(vt))
     && (forall j:int::{TO(j)} TO(j) ==> (baseWords(vt) <= j && j < numFields(abs) <==> VFieldPtr(abs, j)))
    )
 && (tag(vt) == ?OTHER_ARRAY_TAG ==>
        !VFieldPtr(abs, 2)
     && !VFieldPtr(abs, 3)
     && between(4, numFields(abs), baseWords(vt))
     && (arrayOf(vt) != ?TYPE_STRUCT ==> (forall j:int::{TO(j)} TO(j) ==> !VFieldPtr(abs, j)))
    )
 && (isOtherTag(tag(vt)) ==>
        (forall j:int::{TO(j)} TO(j) ==>
            VFieldPtr(abs, j) == (fieldToSlot(vt, j) != 0)
         && (fieldToSlot(vt, j) != 0 ==> between(1, 1 + ro32(mask(vt)), fieldToSlot(vt, j))
             && ro32(mask(vt) + 4 * fieldToSlot(vt, j)) + 1 == j))
     && (forall k:int::{TSlot(k)} TSlot(k) ==> 1 <= k && k < 1 + ro32(mask(vt)) ==>
            inRo(mask(vt) + 4 * k, 4)
         && (ro32(mask(vt) + 4 * k) != 0 ==>
                between(0, numFields(abs), ro32(mask(vt) + 4 * k) + 1)
             && fieldToSlot(vt, ro32(mask(vt) + 4 * k) + 1) == k))
     && inRo(mask(vt), 4)
     && ro32(mask(vt)) >= 0
    )
));

axiom (forall abs:int, vt:int::{TVT(abs, vt)} VTable(abs, vt) ==>
    inRo(vt + ?VT_MASK, 4)
 && inRo(vt + ?VT_BASE_LENGTH, 4)
 && inRo(vt + ?VT_ARRAY_ELEMENT_SIZE, 4)
 && inRo(vt + ?VT_ARRAY_ELEMENT_CLASS, 4)
 && inRo(vt + ?VT_ARRAY_OF, 4)
);

function pad(i:int) returns(int)
{
  and(i + 3, neg(3))
}

function{:expand false} TVL(abs:int) returns(bool) { true }
function ObjSize(abs:int, vt:int, nElems1:int, nElems2:int) returns(bool);
axiom (forall abs:int, vt:int, nElems1:int, nElems2:int::{TVL(abs), ObjSize(abs, vt, nElems1, nElems2)} ObjSize(abs, vt, nElems1, nElems2) <==>
(
    numFields(abs) >= 2
 && (!isVarSize(tag(vt)) ==> 4 * numFields(abs) == baseLength(vt))
 && (tag(vt) == ?STRING_TAG ==> numFields(abs) >= 4 && 4 * numFields(abs) == pad(16 + 2 * nElems1))
 && (tag(vt) == ?PTR_VECTOR_TAG ==> numFields(abs) >= 3 && 4 * numFields(abs) == pad(baseLength(vt) + 4 * nElems1))
 && (tag(vt) == ?OTHER_VECTOR_TAG ==> numFields(abs) >= 3 && 4 * numFields(abs) == pad(baseLength(vt) + Mult(arrayElementSize(vt), nElems1)))
 && (tag(vt) == ?PTR_ARRAY_TAG ==> numFields(abs) >= 4 && 4 * numFields(abs) == pad(baseLength(vt) + 4 * nElems2))
 && (tag(vt) == ?OTHER_ARRAY_TAG ==> numFields(abs) >= 4 && 4 * numFields(abs) == pad(baseLength(vt) + Mult(arrayElementSize(vt), nElems2)))
));

type $FrameLayout;
function frameLayoutArgs($FrameLayout) returns(int);
function frameLayoutLocals($FrameLayout) returns(int);
function frameHasPtr($FrameLayout, int) returns(bool);
function frameDescriptor($FrameLayout) returns(desc:int);
function frameFieldToSlot($FrameLayout, int) returns(int);

var $FrameCount:int;
var $FrameSlice:[int]int;
var $FrameAddr:[int]int;
var $FrameLayout:[int]$FrameLayout;
var $FrameMem:[int]int;
var $FrameAbs:[int][int]int;
var $FrameOffset:[int]int;

function inFrame(layout:$FrameLayout, j:int) returns(bool)
{
  -frameLayoutLocals(layout) <= j && j < 2 + frameLayoutArgs(layout)
}

function{:expand false} TVF(l:$FrameLayout) returns(bool) { true }
axiom (forall l:$FrameLayout, j:int::{TVF(l),TO(j)}
    (inFrame(l, 0) && !frameHasPtr(l, 0))
 && (inFrame(l, 1) && !frameHasPtr(l, 1))
 && (TO(j) && frameHasPtr(l, j) ==> inFrame(l, j))
 && (TO(j) && getBit(frameDescriptor(l), 0) && !getBit(frameDescriptor(l), 1) && and(shr(frameDescriptor(l), 6), 1023) == 0 ==>
        between(0, 16, frameLayoutArgs(l))
     && frameLayoutArgs(l) == and(shr(frameDescriptor(l), 2), 15)
     && (frameHasPtr(l, j) ==> 0 <= frameLayoutArgs(l) + 1 - j && frameLayoutArgs(l) - 1 - j < 16)
     && (0 <= frameLayoutArgs(l) + 1 - j && frameLayoutArgs(l) - 1 - j < 16 ==> (
            (j >= 2 ==> frameHasPtr(l, j) == getBit(frameDescriptor(l), 16 + frameLayoutArgs(l) + 1 - j))
         && (j < 0  ==> frameHasPtr(l, j) == getBit(frameDescriptor(l), 16 + frameLayoutArgs(l) - 1 - j)))
    ))
 && (TO(j) && !getBit(frameDescriptor(l), 0) ==> inRo(frameDescriptor(l), 4))
 && (TO(j) && !getBit(frameDescriptor(l), 0) && ro32(frameDescriptor(l)) == 4096 && inFrame(l, j) ==> (
        inRo(frameDescriptor(l) + 4, 1)
     && inRo(frameDescriptor(l) + 6 + frameFieldToSlot(l, j), 1)
     && j == roS8(frameDescriptor(l) + 6 + frameFieldToSlot(l, j))
     && frameHasPtr(l, j) == (
          between(0, roU8(frameDescriptor(l) + 4), frameFieldToSlot(l, j))
        )
    )));
axiom (forall l:$FrameLayout, k:int::{TVF(l),TSlot(k)}
        TSlot(k) && !getBit(frameDescriptor(l), 0) && ro32(frameDescriptor(l)) == 4096 && between(0, roU8(frameDescriptor(l) + 4), k) ==>
            inFrame(l, roS8(frameDescriptor(l) + 6 + k))
         && k == frameFieldToSlot(l, roS8(frameDescriptor(l) + 6 + k))
    );

const ?sectionCount:int;
const ?staticDataPointerBitMap:int;
const ?dataSectionEnd:int;
const ?dataSectionBase:int;

function sectionSlice(ptr:int) returns(section:int);
function sectionBase(section:int) returns(ptr:int) { ro32(?dataSectionBase + 4 * section) }
function sectionEnd(section:int) returns(ptr:int) { ro32(?dataSectionEnd + 4 * section) }
function sectionHasPtr(section:int, j:int) returns(bool);

function inSectionData(ptr:int) returns(bool);

function{:expand false} TVS(s:int, j:int) returns(bool) { true }
axiom (forall s:int, j:int::{TVS(s, j)}
        0 <= s && s < ?sectionCount && 0 <= j ==>
            inRo(?dataSectionBase + 4 * s, 4)
         && inRo(?dataSectionEnd + 4 * s, 4)
         && inRo(?staticDataPointerBitMap + 4 * s, 4)
         && (sectionBase(s) + 4 * j < sectionEnd(s) ==>
                inSectionData(ro32(?dataSectionBase + 4 * s) + 4 * j)
             && inRo(ro32(?staticDataPointerBitMap + 4 * s) + 4 * shr(j, 5), 4)
             && and(j, 31) < 32 // REVIEW: this is true, so just prove it
             && sectionHasPtr(s, j) == getBit(
                  ro32(ro32(?staticDataPointerBitMap + 4 * s) + 4 * shr(j, 5)),
                  and(j, 31)
                  )));

const ?callSiteTableCount:int;
const ?codeBaseStartTable:int;
const ?returnAddressToCallSiteSetNumbers:int;
const ?callSiteSetCount:int;
const ?callSiteSetNumberToIndex:int;
const ?activationDescriptorTable:int;

function LookupDesc(t:int, j:int) returns(int)
{
  ro32(ro32(?activationDescriptorTable + 4 * t) + 4 *
    roU16(ro32(?callSiteSetNumberToIndex + 4 * t) + 2 * j))
}

function InTable(t:int, j:int) returns(bool)
{
  0 <= t && t < ?callSiteTableCount && 0 <= j && j < ro32(ro32(?callSiteSetCount + 4 * t))
}

function RetAddrAt(t:int, j:int, retaddr:int) returns(bool)
{
    InTable(t, j)
 && between(ro32(ro32(?returnAddressToCallSiteSetNumbers + 4 * t) + 4 * j),
            ro32(ro32(?returnAddressToCallSiteSetNumbers + 4 * t) + 4 * (j + 1)),
            retaddr - ro32(?codeBaseStartTable + 4 * t))
}

function{:expand false} TVFT(f:int) returns(bool) { true }

function FrameNextInv(f:int, ra:int, nextFp:int, $FrameAddr:[int]int, $FrameLayout:[int]$FrameLayout) returns(bool);
axiom (forall f:int, ra:int, nextFp:int, $FrameAddr:[int]int, $FrameLayout:[int]$FrameLayout::{TVFT(f), FrameNextInv(f, ra, nextFp, $FrameAddr, $FrameLayout)} FrameNextInv(f, ra, nextFp, $FrameAddr, $FrameLayout) <==>
(
    f >= 0
 && (f == 0 <==> !(exists t:int, j:int::{TT(t), TO(j)} TT(t) && TO(j) && RetAddrAt(t, j, ra)))
 && (f > 0 ==>
        $FrameAddr[f - 1] == nextFp
     && (forall t:int, j:int::{TT(t), TO(j)} TT(t) && TO(j) ==>
          RetAddrAt(t, j, ra) ==> frameDescriptor($FrameLayout[f - 1]) == LookupDesc(t, j)))
));

axiom (forall f:int::{TVFT(f)}
(
  (forall t:int::{TT(t)} TT(t) ==> 0 <= t && t < ?callSiteTableCount ==>
      inRo(?codeBaseStartTable + 4 * t, 4)
   && inRo(?returnAddressToCallSiteSetNumbers + 4 * t, 4)
   && inRo(?callSiteSetCount + 4 * t, 4)
   && inRo(ro32(?callSiteSetCount + 4 * t), 4)
   && inRo(?callSiteSetNumberToIndex + 4 * t, 4)
   && inRo(?activationDescriptorTable + 4 * t, 4)
   && (forall j:int::{TO(j)} TO(j) ==> 0 <= j && j <= ro32(ro32(?callSiteSetCount + 4 * t)) ==>
          inRo(ro32(?returnAddressToCallSiteSetNumbers + 4 * t) + 4 * j, 4)
       && inRo(ro32(?callSiteSetNumberToIndex + 4 * t) + 2 * j, 2)
       && inRo(ro32(?activationDescriptorTable + 4 * t)
            + 4 * roU16(ro32(?callSiteSetNumberToIndex + 4 * t) + 2 * j), 4)
      )
  )
));

axiom (forall f:int::{TVFT(f)}
(
  (forall t:int, j1:int, j2:int::{TT(t), TO(j1), TO(j2)} TT(t) && TO(j1) && TO(j2) ==>
    0 <= t && t < ?callSiteTableCount && 0 <= j1 && j1 < j2 && j2 <= ro32(ro32(?callSiteSetCount + 4 * t)) ==>
      ro32(ro32(?returnAddressToCallSiteSetNumbers + 4 * t) + 4 * j1) < ro32(ro32(?returnAddressToCallSiteSetNumbers + 4 * t) + 4 * j2)
  )
));

// Note: we allow reads, but not writes, from $frame == $FrameCount, which
// is the garbage collector's own initial stack frame.  This feature allows
// the collector to read the arguments and saved return address set
// by the mutator.  It does not allow reading the collector's own data.
procedure FrameLoad($frame:int, ptr:int) returns(val:int);
  requires 0 <= $frame && $frame <= $FrameCount;
  requires $FrameSlice[ptr] == $frame;
  ensures  word(val);
  ensures  val == $FrameMem[ptr];

procedure FrameStore($frame:int, ptr:int, val:int);
  requires 0 <= $frame && $frame < $FrameCount;
  requires $FrameSlice[ptr] == $frame;
  requires word(val);
  modifies $FrameMem;
  ensures  $FrameMem == old($FrameMem)[ptr := val];

function FrameInv(f:int, l:$FrameLayout, r:[int]int, $FrameAddr:[int]int, $FrameSlice:[int]int, $FrameLayout:[int]$FrameLayout, $FrameMem:[int]int, $FrameAbs:[int][int]int, $FrameOffset:[int]int, $Time:Time) returns(bool)
{
    FrameNextInv(f, $FrameMem[$FrameAddr[f] + 4], $FrameMem[$FrameAddr[f]], $FrameAddr, $FrameLayout)
 && (forall j:int::{TO(j)} TO(j) ==> inFrame(l, j) ==>
        $FrameSlice[$FrameAddr[f] + 4 * j] == f
     && word($FrameAddr[f] + 4 * j)
     && InteriorValue(frameHasPtr(l, j), r, $FrameMem[$FrameAddr[f] + 4 * j], $FrameAbs[f][j], $FrameOffset[$FrameAddr[f] + 4 * j])
     && (frameHasPtr(l, j) && gcAddrEx($FrameMem[$FrameAddr[f] + 4 * j]) ==> reached($FrameAbs[f][j], $Time))
    )
}

function StackInv(r:[int]int, $FrameCount:int, $FrameAddr:[int]int, $FrameLayout:[int]$FrameLayout,
  $FrameSlice:[int]int, $FrameMem:[int]int, $FrameAbs:[int][int]int, $FrameOffset:[int]int, t:Time) returns(bool)
{
  (forall f:int::{TV(f)} TV(f) ==> 0 <= f && f < $FrameCount ==>
    FrameInv(f, $FrameLayout[f], r, $FrameAddr, $FrameSlice, $FrameLayout, $FrameMem, $FrameAbs, $FrameOffset, t))
}

var $SectionMem:[int]int;
var $SectionAbs:[int][int]int;

function SectionInv(s:int, i1:int, i2:int, r:[int]int, $SectionMem:[int]int, $SectionAbs:[int][int]int, t:Time) returns(bool)
{
  (forall j:int::{TO(j)} TO(j) ==> 0 <= j && i1 + 4 * j < i2 ==>
      sectionSlice(i1 + 4 * j) == s
   && Value(sectionHasPtr(s, j), r, $SectionMem[i1 + 4 * j], $SectionAbs[s][j])
   && (sectionHasPtr(s, j) && gcAddrEx($SectionMem[i1 + 4 * j]) ==> reached($SectionAbs[s][j], t))
  )
}

function StaticInv(r:[int]int, $SectionMem:[int]int, $SectionAbs:[int][int]int, t:Time) returns(bool)
{
  (forall s:int::{TV(s)} TV(s) ==> 0 <= s && s < ?sectionCount ==>
    SectionInv(s, sectionBase(s), sectionEnd(s), r, $SectionMem, $SectionAbs, t))
}

procedure SectionLoad(ptr:int) returns(val:int);
  requires inSectionData(ptr);
  ensures  word(val);
  ensures  val == $SectionMem[ptr];

procedure SectionStore(ptr:int, val:int);
  requires inSectionData(ptr);
  requires word(val);
  modifies $SectionMem;
  ensures  $SectionMem == old($SectionMem)[ptr := val];

//////////////////////////////////////////////////////////////////////////////
// ABSTRACT AND CONCRETE GRAPHS
//////////////////////////////////////////////////////////////////////////////

// Each integer i is considered a concrete node.
// The memory manager controls concrete nodes in memory.  
//   - Each abstract object node is either mapped to one concrete node or is unmapped
//   - Each concrete node is either mapped to one abstract object node or is unmapped
//   - If abstract object node A is mapped to concrete node C, then C is mapped to A
// Let the notation C<-->A indicate that A is mapped to C and C is mapped to A.
// Let the notation C-->none indicate that C is unmapped.
// Let the notation A-->none indicate that A is unmapped.

// The variable $toAbs maps concrete nodes to abstract nodes, and thereby
// exactly describes all C<-->A and C-->none.  The A-->none mappings are
// implied; if there is no C such that C<-->A, then A-->none.
var $toAbs:[int]int; // maps a concrete node C to an abstract node A or to "none"

// MAP_NO_ABS has no C<-->A mappings.
const MAP_NO_ABS:[int]int;
axiom (forall i:int::{TV(i)} TV(i) ==> MAP_NO_ABS[i] == NO_ABS);

// WellFormed($toAbs) ensures that if C1 != C2 and $toAbs[C1] != NO_ABS
// and $toAbs[C2] != NO_ABS then $toAbs[C1] != $toAbs[C2].
function WellFormed($toAbs:[int]int) returns(bool)
{
    (forall i1:int, i2:int::{TV(i1), TV(i2)} TV(i1) && TV(i2)
      && gcAddr(i1) && gcAddr(i2) && i1 != i2 && $toAbs[i1] != NO_ABS && $toAbs[i2] != NO_ABS
      ==> $toAbs[i1] != $toAbs[i2])
}