зеркало из https://github.com/microsoft/ivy.git
working on sht
This commit is contained in:
Ken McMillan
Родитель
6209923cfc
Коммит
b974fb77c5
|
|
@ -0,0 +1,97 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include order
|
||||
include collections
|
||||
|
||||
module message_queue(net_msg,seq_num) = {
|
||||
|
||||
relation contents(M:net_msg.t)
|
||||
init ~contents(M)
|
||||
|
||||
action enqueue(msg:net_msg.t)
|
||||
action empty returns (res:bool)
|
||||
action pick_one returns (res:net_msg.t)
|
||||
action delete_all(seq:seq_num)
|
||||
|
||||
|
||||
object spec = {
|
||||
|
||||
before enqueue {
|
||||
assert ~contents(msg);
|
||||
contents(msg) := true
|
||||
}
|
||||
|
||||
after empty returns (res:bool) {
|
||||
call impl.lemma;
|
||||
assert contents(M) -> ~res;
|
||||
assert ~res -> exists M. contents(M)
|
||||
}
|
||||
|
||||
before pick_one {
|
||||
assert exists M. contents(M);
|
||||
call impl.lemma
|
||||
}
|
||||
|
||||
after pick_one {
|
||||
assert contents(res)
|
||||
}
|
||||
|
||||
before delete_all {
|
||||
contents(M) := contents(M) & ~(net_msg.num(M) <= seq)
|
||||
}
|
||||
}
|
||||
|
||||
object impl = {
|
||||
|
||||
type range
|
||||
|
||||
# instantiate totally_ordered_with_zero(t)
|
||||
# instance iter : order_iterator(range)
|
||||
|
||||
individual full(X:range) : bool
|
||||
individual items(X:range) : net_msg.t
|
||||
|
||||
init ~full(X)
|
||||
|
||||
instance rev : map(net_msg.t,range,0)
|
||||
|
||||
implement enqueue {
|
||||
assume exists X. ~full(X);
|
||||
if some pos:range. ~full(pos) {
|
||||
full(pos) := true;
|
||||
items(pos) := msg;
|
||||
call rev.set_(msg,pos)
|
||||
}
|
||||
}
|
||||
|
||||
implement empty {
|
||||
if exists X. full(X) {
|
||||
res := false
|
||||
}
|
||||
else {
|
||||
res := true
|
||||
}
|
||||
}
|
||||
|
||||
implement delete_all(seq:seq_num) {
|
||||
full(X) := full(X) & ~(net_msg.num(items(X)) <= seq)
|
||||
}
|
||||
|
||||
implement pick_one {
|
||||
if some pos:range. full(pos) {
|
||||
res := items(pos)
|
||||
}
|
||||
}
|
||||
|
||||
action lemma = {
|
||||
if some (msg:net_msg.t) contents(msg) {
|
||||
call rev.lemma(msg)
|
||||
}
|
||||
}
|
||||
|
||||
conjecture rev.map(M,X) -> (contents(M) <-> (full(X) & items(X) = M))
|
||||
conjecture full(X) & items(X) = M -> rev.map(M,X)
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include order
|
||||
|
||||
module sequence_numbers = {
|
||||
|
||||
type t
|
||||
instantiate totally_ordered(t)
|
||||
|
||||
action next(seq:t) returns (res:t)
|
||||
|
||||
object spec = {
|
||||
after next {
|
||||
assume exists X. seq < X;
|
||||
assert seq < res & (X < res -> X <= seq)
|
||||
}
|
||||
}
|
||||
|
||||
object impl = {
|
||||
interpret t->bv[16]
|
||||
implement next {
|
||||
res := seq + 1
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -100,7 +100,8 @@ module hash_table(key,value,shard) = {
|
|||
invariant lo <= X & X <= hi & shard.value(s,X) = 0 -> ~tab.s(X)
|
||||
invariant lo <= X & X <= hi & shard.iter.done(Y,pos) & shard.at(s,X,Y) -> tab.s(X) & tab.r(X,shard.value(s,X))
|
||||
invariant ~(lo <= X & X <= hi) -> tab_invar(X,Y)
|
||||
# -> shard.value(res,X) = tab.get(X)
|
||||
# following are object invariants of tab and shouldn't be needed here
|
||||
invariant tab.r(X,Y) & tab.r(X,Z) -> Y = Z
|
||||
{
|
||||
local r : shard.range {
|
||||
r := shard.iter.val(pos);
|
||||
|
|
@ -119,7 +120,7 @@ module hash_table(key,value,shard) = {
|
|||
& (~tab.s(X) -> hash(X) = 0)
|
||||
& (tab.s(X) -> tab.r(X,hash(X)))
|
||||
|
||||
conjecture tab_invar(X,Y)
|
||||
conjecture shard.value(S,X)=Z -> tab_invar(X,Y)
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,21 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include queue
|
||||
include seq_num
|
||||
|
||||
instance seq_num : sequence_numbers
|
||||
|
||||
object net_msg = {
|
||||
type t = struct {
|
||||
num : seq_num.t
|
||||
}
|
||||
}
|
||||
|
||||
instance q : message_queue(net_msg,seq_num.t)
|
||||
|
||||
isolate iso_q = q.impl with q,net_msg,seq_num
|
||||
|
||||
export q.enqueue
|
||||
export q.empty
|
||||
export q.pick_one
|
||||
export q.delete_all
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include trans
|
||||
include seq_num
|
||||
include udp
|
||||
|
||||
type ltime
|
||||
type id
|
||||
type req
|
||||
type shard
|
||||
|
||||
instance seq_num : sequence_numbers
|
||||
|
||||
intance u : udp_simple(id,t.impl.net_msg.t)
|
||||
|
||||
instance t : net(u,req,shard,seq_num,ltime)
|
||||
|
||||
isolate iso_t = t.impl with t,u,seq_num
|
||||
|
||||
export t.enqueue
|
||||
export t.empty
|
||||
export t.pick_one
|
||||
export t.delete_all
|
||||
|
|
@ -0,0 +1,209 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include queue
|
||||
include timeout
|
||||
|
||||
module net(lower,req,shard,seq_num,ltime) = {
|
||||
|
||||
relation requested(D:id,R:req)
|
||||
relation delegated(D:id,S:shard)
|
||||
|
||||
init ~requested(D,R)
|
||||
init ~delegated(D,S)
|
||||
|
||||
action send_request(src:id,dst:id,rq:req)
|
||||
action send_delegate(src:id,dst:id,s:shard)
|
||||
action send_reply(src:id, dst:id, d:data, lt:ltime)
|
||||
action recv_request(dst:id,rq:req)
|
||||
action recv_delegate(dst:id,s:shard)
|
||||
|
||||
object spec = {
|
||||
before send_request {
|
||||
assert ~requested(dst,rq);
|
||||
requested(dst,rq) := true
|
||||
}
|
||||
|
||||
before send_delegate {
|
||||
assert ~delegated(dst,s);
|
||||
delegated(dst,s) := true
|
||||
}
|
||||
|
||||
before recv_request {
|
||||
assert requested(dst,rq);
|
||||
requested(dst,rq) := false
|
||||
}
|
||||
|
||||
before recv_delegate {
|
||||
assert delegated(dst,s);
|
||||
delegated(dst,s) := false
|
||||
}
|
||||
}
|
||||
|
||||
object impl(me:id) = {
|
||||
|
||||
# these type describe the format of messages
|
||||
|
||||
type mtype = {request_t, reply_t, delegate_t, ack_t}
|
||||
|
||||
type net_msg = struct {
|
||||
mty : mtype,
|
||||
src : id,
|
||||
rq : req,
|
||||
num : seq_num.t,
|
||||
sh : shard
|
||||
}
|
||||
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num.t)
|
||||
instance timer(D:id) : timeout_sec
|
||||
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
|
||||
individual send_seq(S:id) : seq_num.t
|
||||
individual recv_seq(S:id) : seq_num.t
|
||||
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
|
||||
# Implementations of interface actions
|
||||
|
||||
implement send_request(dst:id,rq:req) {
|
||||
local msg : net_msg, seq : seq_num.t {
|
||||
# msg := encoder.mk_req(me,dst,rq,send_seq(dst));
|
||||
net_msg.mty(msg) := request_t;
|
||||
net_msg.src(msg) := me;
|
||||
net_msg.rq(msg) := rq;
|
||||
net_msg.num(msg) := send_seq(dst);
|
||||
send_seq(dst) := seq_num.next(send_seq(dst));
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(dst,msg)
|
||||
}
|
||||
}
|
||||
|
||||
implement send_delegate(dst:id,sh:shard) {
|
||||
local msg : net_msg, seq : seq_num.t {
|
||||
# msg := encoder.mk_delegate(me,dst,sh,send_seq(dst));
|
||||
net_msg.mty(msg) := delegate_t;
|
||||
net_msg.src(msg) := me;
|
||||
net_msg.sh(msg) := sh;
|
||||
net_msg.num(msg) := send_seq(dst);
|
||||
send_seq(dst) := seq_nums.next(send_seq(dst));
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send_msg(dst,msg)
|
||||
}
|
||||
}
|
||||
|
||||
implement send_reply(dst:id, d:data, lt:ltime) {
|
||||
# for now, do nothing, but we verify data correct
|
||||
}
|
||||
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
|
||||
implement lower.recv_msg(msg:net_msg) {
|
||||
local src:id,seq:seq_num.t {
|
||||
seq := net_msg.num(msg);
|
||||
src := net_msg.src(msg);
|
||||
if seq <= recv_seq(src) & net_msg.mty(msg) ~= ack_t {
|
||||
local ack : net_msg {
|
||||
net_msg.mty(ack) := ack_t;
|
||||
net_msg.src(ack) := me;
|
||||
net_msg.num(ack) := seq;
|
||||
call lower.send_msg(src,ack)
|
||||
}
|
||||
};
|
||||
if seq = recv_seq(src) {
|
||||
recv_seq(src) := seq_nums.next(recv_seq(src));
|
||||
if net_msg._mty(msg) = request_t {
|
||||
call recv_request(me,net_msg.req(msg))
|
||||
}
|
||||
else if net_msg.mty(msg) = delegate_t {
|
||||
call recv_delegate(me,net_msg.sh(msg))
|
||||
}
|
||||
else if net_msg_mtype(msg) = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send_msg(dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
|
||||
# If I have a request message for D enqueued and if its sequence number is
|
||||
# >= D's receive sequence number, then the message is pending.
|
||||
|
||||
conjecture mq(D).contents(M) & neti(D).recv_seq(me) <= net_msg_seq_num(M)
|
||||
& net_msg_mtype(M) = request_t -> net.requested(D,net_msg_req(M))
|
||||
|
||||
# If I have a delegate message for D enqueued and if its sequence number is
|
||||
# >= D's receive sequence number, then the message is pending.
|
||||
|
||||
conjecture mq(D).contents(M) & neti(D).recv_seq(me) <= net_msg_seq_num(M)
|
||||
& net_msg_mtype(M) = delegate_t -> net.delegated(D,net_msg_shard(M))
|
||||
|
||||
# A given request cannot occur twice in the network
|
||||
|
||||
conjecture neti(S1).mq(D).contents(M1) & neti(D).recv_seq(S1) <= net_msg_seq_num(M1)
|
||||
& neti(S2).mq(D).contents(M2) & neti(D).recv_seq(S2) <= net_msg_seq_num(M2)
|
||||
& net_msg_mtype(M1) = request_t & net_msg_mtype(M2) = request_t
|
||||
& (S1 ~= S2 | net_msg_seq_num(M1) ~= net_msg_seq_num(M2))
|
||||
-> net_msg_req(M1) ~= net_msg_req(M2)
|
||||
|
||||
# A given delegation cannot occur twice in the network
|
||||
|
||||
conjecture neti(S1).mq(D).contents(M1) & neti(D).recv_seq(S1) <= net_msg_seq_num(M1)
|
||||
& neti(S2).mq(D).contents(M2) & neti(D).recv_seq(S2) <= net_msg_seq_num(M2)
|
||||
& net_msg_mtype(M1) = delegate_t & net_msg_mtype(M2) = delegate_t
|
||||
& (S1 ~= S2 | net_msg_seq_num(M1) ~= net_msg_seq_num(M2))
|
||||
-> net_msg_shard(M1) ~= net_msg_shard(M2)
|
||||
|
||||
# The sending seq number is greater than any queue entry
|
||||
|
||||
conjecture mq(D).contents(M) -> ~(send_seq(D) <= net_msg_seq_num(M))
|
||||
|
||||
# No two messages in a queue have the same sequence number
|
||||
|
||||
conjecture mq(D).contents(M1) & mq(D).contents(M2) & M1 ~= M2
|
||||
-> net_msg_seq_num(M1) ~= net_msg_seq_num(M2)
|
||||
|
||||
# A sent non-ack message must match any message queue entry with the same
|
||||
# sequence number
|
||||
|
||||
conjecture low.sent(M,D) & net_msg_src(M) = me
|
||||
& mq(D).contents(M2) & net_msg_seq_num(M2) = net_msg_seq_num(M)
|
||||
& net_msg_mtype(M) ~= ack_t -> M = M2
|
||||
|
||||
# Following added due to counterexamples
|
||||
|
||||
# A sent non-ack message with seq num >= receiver must be in the
|
||||
# corresponding queue
|
||||
|
||||
conjecture low.sent(M,D) & net_msg_src(M) = S
|
||||
& neti(D).recv_seq(S) <= net_msg_seq_num(M) & net_msg_mtype(M) ~= ack_t
|
||||
-> neti(S).mq(D).contents(M)
|
||||
|
||||
# If an ack is sent, the receiving seq_num must be greater
|
||||
|
||||
conjecture low.sent(M,D) & net_msg_src(M) = S
|
||||
& net_msg_mtype(M) = ack_t -> ~(neti(S).recv_seq(D) <= net_msg_seq_num(M))
|
||||
|
||||
# The sending seq number is greater than non-ack sent message
|
||||
|
||||
conjecture low.sent(M,D) & net_msg_src(M) = me & net_msg_mtype(M) ~= ack_t
|
||||
-> ~(send_seq(D) <= net_msg_seq_num(M))
|
||||
|
||||
# A message in the queue has correct src and is not ack
|
||||
|
||||
conjecture mq(D).contents(M) -> net_msg_src(M) = me & net_msg_mtype(M) ~= ack_t
|
||||
}
|
||||
}
|
||||
|
|
@ -259,28 +259,32 @@ module ordered_map(key,value) = {
|
|||
relation r(K:key.t,V:value)
|
||||
init ~s(K) & ~r(K,V)
|
||||
|
||||
instantiate succ : map(key.t,key.t,0) # ghost
|
||||
# instantiate succ : map(key.t,key.t,0) # ghost
|
||||
|
||||
|
||||
object spec = {
|
||||
# insert one element
|
||||
before set {
|
||||
s(nkey) := true;
|
||||
r(nkey,X) := X = v;
|
||||
r(nkey,X) := X = v
|
||||
|
||||
# ;
|
||||
|
||||
# # following is ghost code to update the successor relation
|
||||
# local sk:key.t {
|
||||
# if some (lub:key.t) ~(lub <= nkey) & s(lub) minimizing lub {
|
||||
# sk := lub
|
||||
# }
|
||||
# else {
|
||||
# sk := 0
|
||||
# };
|
||||
# call succ.set_(nkey,sk)
|
||||
# };
|
||||
# if some (glb:key.t) ~(nkey <= glb) & s(glb) maximizing glb {
|
||||
# call succ.lemma(glb); # instantiate succ(glb)
|
||||
# call succ.set_(glb,nkey)
|
||||
|
||||
|
||||
# following is ghost code to update the successor relation
|
||||
local sk:key.t {
|
||||
if some (lub:key.t) ~(lub <= nkey) & s(lub) minimizing lub {
|
||||
sk := lub
|
||||
}
|
||||
else {
|
||||
sk := 0
|
||||
};
|
||||
call succ.set_(nkey,sk)
|
||||
};
|
||||
if some (glb:key.t) ~(nkey <= glb) & s(glb) maximizing glb {
|
||||
call succ.lemma(glb); # instantiate succ(glb)
|
||||
call succ.set_(glb,nkey)
|
||||
}
|
||||
}
|
||||
|
||||
after get {
|
||||
|
|
@ -311,7 +315,7 @@ module ordered_map(key,value) = {
|
|||
after next {
|
||||
local k:key.t {
|
||||
k := key.iter.val(it);
|
||||
call succ.lemma(k);
|
||||
# call succ.lemma(k);
|
||||
if some (lub:key.t) lub > k & s(lub) minimizing lub {
|
||||
assert key.iter.val(res) = lub
|
||||
}
|
||||
|
|
@ -323,13 +327,14 @@ module ordered_map(key,value) = {
|
|||
|
||||
}
|
||||
|
||||
|
||||
# Useful invariants of the "succ" relation. The successor of K is
|
||||
# also in the map, and nothing between K and its successor is in
|
||||
# the map. 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)
|
||||
# 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)
|
||||
|
||||
# Mapping relation R is injective
|
||||
|
||||
|
|
|
|||
|
|
@ -368,6 +368,7 @@ class EnumeratedSort(Sort):
|
|||
def __init__(self,extension):
|
||||
self.extension = extension
|
||||
self.dom = []
|
||||
self.args = []
|
||||
def __repr__(self):
|
||||
return '{' + ','.join(self.extension) + '}'
|
||||
def defines(self):
|
||||
|
|
@ -933,8 +934,8 @@ def ast_rewrite(x,rewrite):
|
|||
return res
|
||||
if isinstance(x,TypeDef):
|
||||
atom = rewrite.rewrite_atom(Atom(x.args[0]))
|
||||
if atom.args:
|
||||
raise iu.IvyError(x,'Types cannot have parameters: {}'.format(atom))
|
||||
# if atom.args:
|
||||
# raise iu.IvyError(x,'Types cannot have parameters: {}'.format(atom))
|
||||
name = atom.rep
|
||||
if isinstance(x.args[1],StructSort):
|
||||
t = ast_rewrite(x.args[1],rewrite)
|
||||
|
|
@ -983,6 +984,8 @@ def substitute_constants_ast(ast,subs):
|
|||
if (isinstance(ast, Atom) or isinstance(ast,App)) and not ast.args:
|
||||
return subs.get(ast.rep,ast)
|
||||
else:
|
||||
if isinstance(ast,str):
|
||||
print ast
|
||||
new_args = [substitute_constants_ast(x,subs) for x in ast.args]
|
||||
res = ast.clone(new_args)
|
||||
copy_attributes_ast(ast,res)
|
||||
|
|
|
|||
|
|
@ -98,6 +98,8 @@ def inst_mod(ivy,module,pref,subst,vsubst):
|
|||
map1 = distinct_variable_renaming(used_variables_ast(pref),used_variables_ast(decl))
|
||||
vpref = substitute_ast(pref,map1)
|
||||
vvsubst = dict((x,map1[y.rep]) for x,y in vsubst.iteritems())
|
||||
iu.dbg('decl')
|
||||
iu.dbg('type(decl)')
|
||||
idecl = subst_prefix_atoms_ast(decl,subst,vpref,module.defined)
|
||||
idecl = substitute_constants_ast(idecl,vvsubst)
|
||||
else:
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче