зеркало из https://github.com/microsoft/ivy.git
pulled out boilerplate into std
This commit is contained in:
Ken McMillan
Родитель
3d26332337
Коммит
c72c8ccd18
|
|
@ -12,6 +12,8 @@
|
|||
|
||||
## Forgot to include seq_nums object in iso_n
|
||||
|
||||
include std
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# This is the abstract specification of the sharded hash table protocol. It defines
|
||||
|
|
@ -26,65 +28,21 @@
|
|||
#
|
||||
################################################################################
|
||||
|
||||
########################################
|
||||
# total order theory
|
||||
|
||||
module total_order(carrier) = {
|
||||
relation (T:carrier < U:carrier)
|
||||
# note: because < is polymorphic, we need to use the type here
|
||||
axiom (T:carrier < U & U < V) -> (T < V)
|
||||
axiom ~(T:carrier < U & U < T)
|
||||
axiom T:carrier < U | T = U | U < T
|
||||
# could add <= as derived relation here
|
||||
}
|
||||
|
||||
module total_non_strict_order(carrier) = {
|
||||
relation (T:carrier <= U:carrier)
|
||||
# note: because <= is polymorphic, we need to use the type here
|
||||
axiom (T:carrier <= U & U <= V) -> (T <= V)
|
||||
axiom T:carrier <= T
|
||||
axiom (T:carrier <= U & U <= T) -> T = U
|
||||
axiom T:carrier <= U | U <= T
|
||||
# could add <= as derived relation here
|
||||
}
|
||||
|
||||
########################################
|
||||
# Maps. This module provides a relational model of a map from a type
|
||||
# dom to a type rng. Initially, everything is mapped to the element zero.
|
||||
|
||||
module map(dom,rng,zero) = {
|
||||
relation map(X:dom,Y:rng)
|
||||
init map(X,Y) <-> Y = zero
|
||||
action set_(x:dom,y:rng) = {
|
||||
local oldval:rng {
|
||||
assume map(x,oldval)
|
||||
};
|
||||
map(x,Y) := Y = y
|
||||
}
|
||||
action set_closed_interval(lo:dom,hi:dom,val:rng) = {
|
||||
# map(X,Y) := (Y = val) if lo <= X & X <= hi else map(X,Y)
|
||||
map(X,Y) := (Y = val) & lo <= X & X <= hi
|
||||
| map(X,Y) & ~(lo <= X & X <= hi)
|
||||
}
|
||||
action get(x:dom) returns (y:rng) = {
|
||||
assume map(x,y)
|
||||
}
|
||||
|
||||
conjecture map(K,L) & map(K,M) -> L = M
|
||||
|
||||
}
|
||||
|
||||
########################################
|
||||
# type of local time
|
||||
|
||||
type ltime
|
||||
instantiate total_order(ltime)
|
||||
|
||||
########################################
|
||||
# type of hash table data
|
||||
|
||||
type data
|
||||
|
||||
########################################
|
||||
# type of hash table keys
|
||||
|
||||
type key
|
||||
instantiate total_non_strict_order(key)
|
||||
|
||||
|
|
@ -102,14 +60,17 @@ axiom 0 <= K:key
|
|||
|
||||
########################################
|
||||
# type of message types
|
||||
|
||||
type mtype = {request_t, reply_t, delegate_t, ack_t}
|
||||
|
||||
########################################
|
||||
# type of hash table ops
|
||||
|
||||
type otype = {read, write}
|
||||
|
||||
########################################
|
||||
# id's of protocol agents
|
||||
|
||||
type id
|
||||
|
||||
########################################
|
||||
|
|
@ -182,7 +143,6 @@ object reference = {
|
|||
|
||||
########################################
|
||||
# memory events by local time
|
||||
# TODO: can we export this read-only?
|
||||
|
||||
instantiate evs(T:ltime) : hashev
|
||||
|
||||
|
|
@ -294,67 +254,6 @@ module delegation_map_spec = {
|
|||
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Ordered set representation
|
||||
#
|
||||
# This is intended to be implemented using the STL set template.
|
||||
#
|
||||
# Ordered sets assume the element type has a total non-strict order,
|
||||
# with a least element 0. They provide insertion of elements (in log
|
||||
# time), deletion of ranges (in n log(n) time) and finding greatest
|
||||
# lower bounds (log n).
|
||||
#
|
||||
# For help with proofs, this module also provides an auxiliary map
|
||||
# "succ" that gives the successor of every element in the set.
|
||||
|
||||
module ordered_set(key) = {
|
||||
|
||||
relation s(K:key)
|
||||
init s(K) <-> K = 0
|
||||
|
||||
instantiate succ : map(key,key,0) # ghost
|
||||
|
||||
# insert one element
|
||||
action insert(nkey:key) = {
|
||||
s(nkey) := true;
|
||||
|
||||
# following is ghost code to update the successor relation
|
||||
local v:key {
|
||||
if some lub:key. ~(lub <= nkey) & s(lub) minimizing lub {
|
||||
v := lub
|
||||
}
|
||||
else {
|
||||
v := 0
|
||||
};
|
||||
call succ.set_(nkey,v)
|
||||
};
|
||||
if some glb:key. ~(nkey <= glb) & s(glb) maximizing glb {
|
||||
local the_succ:key, succ_val:id {
|
||||
the_succ := succ.get(glb) # lemma
|
||||
};
|
||||
call succ.set_(glb,nkey)
|
||||
}
|
||||
}
|
||||
|
||||
# erase elements in a closed interval
|
||||
action erase(lo:key,hi:key) = {
|
||||
s(K) := s(K) & ~(lo <= K & K <= hi)
|
||||
}
|
||||
|
||||
# the the greatest element <= k
|
||||
action get_glb(k:key) returns (res:key) = {
|
||||
if some glb:key. glb <= k & s(glb) maximizing glb {
|
||||
local the_succ:key, succ_val:id {
|
||||
the_succ := succ.get(glb) # lemma
|
||||
};
|
||||
res := glb
|
||||
}
|
||||
}
|
||||
|
||||
conjecture s(K) & succ.map(K,L) & L ~= 0 -> ~(L <= K) & s(L)
|
||||
conjecture s(K) & succ.map(K,L) & ~(M <= K) & (L = 0 | ~(L <= M)) -> ~s(M)
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
|
|
@ -379,7 +278,7 @@ module delegation_map() = {
|
|||
};
|
||||
call has.erase(lo,hi);
|
||||
entries(lo) := dst;
|
||||
call has.insert(lo) #ghost
|
||||
call has.insert(lo)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -387,7 +286,12 @@ module delegation_map() = {
|
|||
val := entries(has.get_glb(k))
|
||||
}
|
||||
|
||||
# The value of every key between K and its successor is the same as K's value.
|
||||
|
||||
conjecture has.s(K) & has.succ.map(K,L) & K <= M & (L = 0 | ~(L <= M)) -> dma.map(me,M,entries(K))
|
||||
|
||||
# We always have an entry for key zero.
|
||||
|
||||
conjecture has.s(0)
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,133 @@
|
|||
#lang ivy1.5
|
||||
|
||||
# This is a start on a "standard library" for Ivy
|
||||
|
||||
################################################################################
|
||||
# Total order theories
|
||||
|
||||
module total_order(carrier) = {
|
||||
relation (T:carrier < U:carrier)
|
||||
# note: because < is polymorphic, we need to use the type here
|
||||
axiom (T:carrier < U & U < V) -> (T < V)
|
||||
axiom ~(T:carrier < U & U < T)
|
||||
axiom T:carrier < U | T = U | U < T
|
||||
}
|
||||
|
||||
module total_non_strict_order(carrier) = {
|
||||
relation (T:carrier <= U:carrier)
|
||||
# note: because <= is polymorphic, we need to use the type here
|
||||
axiom (T:carrier <= U & U <= V) -> (T <= V)
|
||||
axiom T:carrier <= T
|
||||
axiom (T:carrier <= U & U <= T) -> T = U
|
||||
axiom T:carrier <= U | U <= T
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Maps.
|
||||
#
|
||||
# This module provides a relational model of a function from a type
|
||||
# dom to a type rng. Initially, everything is mapped to the element zero.
|
||||
#
|
||||
# The key invariant of a map is that it is a function, i.e., for every
|
||||
# X there exists a Y such that map(X,Y). The module does not state
|
||||
# this invariant, however, since the quantifier alternation could
|
||||
# destroy stratificaiton. Instead it provides a "lemma" that allows
|
||||
# the user to instantiate Y for particular values of X.
|
||||
#
|
||||
# Parameters:
|
||||
#
|
||||
# dom The domain type
|
||||
# rng The range type
|
||||
# zero The initial value for every domain element
|
||||
|
||||
module map(dom,rng,zero) = {
|
||||
|
||||
relation map(X:dom,Y:rng)
|
||||
init map(X,Y) <-> Y = zero
|
||||
|
||||
# set the value of x to y
|
||||
action set_(x:dom,y:rng) = {
|
||||
local oldval:rng {
|
||||
assume map(x,oldval)
|
||||
};
|
||||
map(x,Y) := Y = y
|
||||
}
|
||||
|
||||
# get the value of x
|
||||
action get(x:dom) returns (y:rng) = {
|
||||
assume map(x,y)
|
||||
}
|
||||
|
||||
# prove there exists a value for x
|
||||
action lemma(x:dom) = {
|
||||
assume exists Y. map(x,Y)
|
||||
}
|
||||
|
||||
conjecture map(K,L) & map(K,M) -> L = M
|
||||
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Ordered set representation
|
||||
#
|
||||
# This is intended to be implemented using the STL set template.
|
||||
#
|
||||
# Ordered sets assume the element type has a total non-strict order,
|
||||
# with a least element 0. They provide insertion of elements (in log
|
||||
# time), deletion of ranges (in n log(n) time) and finding greatest
|
||||
# lower bounds (log n).
|
||||
#
|
||||
# For help with proofs, this module also provides an auxiliary map
|
||||
# "succ" that gives the successor of every element in the set. The
|
||||
# "successor" of the maximal element in the set is 0.
|
||||
|
||||
module ordered_set(key) = {
|
||||
|
||||
relation s(K:key)
|
||||
init s(K) <-> K = 0
|
||||
|
||||
instantiate succ : map(key,key,0) # ghost
|
||||
|
||||
# insert one element
|
||||
action insert(nkey:key) = {
|
||||
s(nkey) := true;
|
||||
|
||||
# following is ghost code to update the successor relation
|
||||
local v:key {
|
||||
if some lub:key. ~(lub <= nkey) & s(lub) minimizing lub {
|
||||
v := lub
|
||||
}
|
||||
else {
|
||||
v := 0
|
||||
};
|
||||
call succ.set_(nkey,v)
|
||||
};
|
||||
if some glb:key. ~(nkey <= glb) & s(glb) maximizing glb {
|
||||
call succ.lemma(glb); # instantiate succ(glb)
|
||||
call succ.set_(glb,nkey)
|
||||
}
|
||||
}
|
||||
|
||||
# erase elements in a closed interval
|
||||
action erase(lo:key,hi:key) = {
|
||||
s(K) := s(K) & ~(lo <= K & K <= hi)
|
||||
}
|
||||
|
||||
# the the greatest element <= k
|
||||
action get_glb(k:key) returns (res:key) = {
|
||||
if some glb:key. glb <= k & s(glb) maximizing glb {
|
||||
call succ.lemma(glb); # instantiate succ(glb)
|
||||
res := glb
|
||||
}
|
||||
}
|
||||
|
||||
# Useful invariants of the "succ" relation. The successor of K is
|
||||
# also in the set, and nothing between K and its successor is in
|
||||
# the set. Here, if L = 0 it means K is the maximim element, so we
|
||||
# have to treat this as a special case.
|
||||
|
||||
conjecture s(K) & succ.map(K,L) & L ~= 0 -> ~(L <= K) & s(L)
|
||||
conjecture s(K) & succ.map(K,L) & ~(M <= K) & (L = 0 | ~(L <= M)) -> ~s(M)
|
||||
}
|
||||
|
|
@ -161,10 +161,6 @@ def get_strip_params(name,args,strip_map,strip_binding,ast):
|
|||
raise iu.IvyError(ast,"cannot strip isolate parameters from {}".format(name))
|
||||
for sp,ap in zip(strip_params,args):
|
||||
if ap not in strip_binding or strip_binding[ap] != sp:
|
||||
iu.dbg('ast')
|
||||
iu.dbg('strip_binding')
|
||||
iu.dbg('sp')
|
||||
iu.dbg('ap')
|
||||
raise iu.IvyError(ast,"cannot strip parameter {} from {}".format(ap,name))
|
||||
return strip_params
|
||||
|
||||
|
|
@ -194,10 +190,6 @@ def strip_action(ast,strip_map,strip_binding):
|
|||
new_sort = strip_sort(ast.rep.sort,strip_params)
|
||||
new_args = args[len(strip_params):]
|
||||
new_symbol = ivy_logic.Symbol(name,new_sort)
|
||||
iu.dbg('new_sort')
|
||||
iu.dbg('new_sort.dom')
|
||||
iu.dbg('new_args')
|
||||
iu.dbg('new_symbol')
|
||||
return new_symbol(*new_args)
|
||||
return ast.clone(args)
|
||||
|
||||
|
|
@ -217,7 +209,6 @@ def strip_labeled_fmla(lfmla,strip_map):
|
|||
fmla = lfmla.formula
|
||||
strip_binding = {}
|
||||
get_strip_binding(fmla,strip_map,strip_binding)
|
||||
iu.dbg('strip_binding')
|
||||
fmla = strip_action(fmla,strip_map,strip_binding)
|
||||
lbl = lfmla.label
|
||||
if lbl:
|
||||
|
|
@ -234,8 +225,6 @@ def strip_isolate(mod,isolate):
|
|||
for atom in isolate.verified() + isolate.present():
|
||||
name = atom.relname
|
||||
if atom.args:
|
||||
for a in atom.args:
|
||||
print type(a)
|
||||
if not all(isinstance(v,ivy_ast.App) and not v.args for v in atom.args):
|
||||
raise iu.IvyError(atom,"bad isolate parameter")
|
||||
for a in atom.args:
|
||||
|
|
@ -245,10 +234,7 @@ def strip_isolate(mod,isolate):
|
|||
# strip the actions
|
||||
new_actions = {}
|
||||
for name,action in mod.actions.iteritems():
|
||||
iu.dbg('name')
|
||||
iu.dbg('action')
|
||||
strip_params = strip_map_lookup(name[4:] if name.startswith('ext:') else name,strip_map)
|
||||
iu.dbg('strip_params')
|
||||
if not(len(action.formal_params) >= len(strip_params)):
|
||||
raise iu.IvyError(action,"cannot strip isolate parameters from {}".format(name))
|
||||
strip_binding = dict(zip(action.formal_params,strip_params))
|
||||
|
|
@ -256,7 +242,6 @@ def strip_isolate(mod,isolate):
|
|||
new_action.formal_params = action.formal_params[len(strip_params):]
|
||||
new_action.formal_returns = action.formal_returns
|
||||
new_actions[name] = new_action
|
||||
iu.dbg('new_action')
|
||||
mod.actions.clear()
|
||||
mod.actions.update(new_actions)
|
||||
|
||||
|
|
@ -273,7 +258,6 @@ def strip_isolate(mod,isolate):
|
|||
new_sort = strip_sort(sym.sort,strip_params)
|
||||
sym = ivy_logic.Symbol(name,new_sort)
|
||||
new_symbols[name] = sym
|
||||
iu.dbg('sym')
|
||||
ivy_logic.sig.symbols.clear()
|
||||
ivy_logic.sig.symbols.update(new_symbols)
|
||||
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче