зеркало из https://github.com/microsoft/ivy.git
toy_consensus verifies but does not compile
This commit is contained in:
Ken McMillan
Родитель
81d1227a92
Коммит
30d3beea2b
|
|
@ -19,9 +19,6 @@ isolate nset = {
|
|||
action add(s:nset, n : node) returns (s:nset)
|
||||
|
||||
specification {
|
||||
invariant [majorities_intersect]
|
||||
(majority(S) & majority(T)) -> exists N. member(N,S) & member(N,T)
|
||||
|
||||
after emptyset {
|
||||
ensure ~member(N, s)
|
||||
}
|
||||
|
|
@ -31,6 +28,11 @@ isolate nset = {
|
|||
}
|
||||
}
|
||||
|
||||
private {
|
||||
invariant [majorities_intersect]
|
||||
(majority(S) & majority(T)) -> exists N. member(N,S) & member(N,T)
|
||||
}
|
||||
|
||||
implementation {
|
||||
interpret index -> int
|
||||
function card(S:nset) : index
|
||||
|
|
@ -55,7 +57,6 @@ isolate nset = {
|
|||
card(S) := card(S) + 1 if member(i.val, S) else card(S);
|
||||
i := i.next
|
||||
};
|
||||
assume member(N,all)
|
||||
}
|
||||
|
||||
implement emptyset {
|
||||
|
|
@ -106,29 +107,30 @@ isolate toy_protocol = {
|
|||
}
|
||||
}
|
||||
}
|
||||
with nset
|
||||
with nset, nset.majorities_intersect
|
||||
|
||||
instance net : udp_simple(node,msg.t)
|
||||
object msg_kind = {
|
||||
type this = {request_vote, vote, leader}
|
||||
}
|
||||
|
||||
object msg = {
|
||||
type this = struct {
|
||||
kind : msg_kind,
|
||||
src : node,
|
||||
vote : node
|
||||
}
|
||||
}
|
||||
|
||||
instance net : udp_simple(node,msg)
|
||||
|
||||
isolate shim = {
|
||||
|
||||
object msg_kind = {
|
||||
type this = {request_vote, vote, leader}
|
||||
}
|
||||
|
||||
object msg = {
|
||||
type this = struct {
|
||||
kind : msg_kind,
|
||||
src : node,
|
||||
vote : node
|
||||
}
|
||||
}
|
||||
|
||||
module handler(p_kind) = {
|
||||
action handle(dst:node,m:msg.t)
|
||||
action handle(dst:node,m:msg)
|
||||
specification {
|
||||
before handle {
|
||||
require sent(m,dst) & m.m_kind = p_kind
|
||||
require sent(m,dst) & m.kind = p_kind
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -153,18 +155,18 @@ isolate shim = {
|
|||
|
||||
implementation {
|
||||
|
||||
action debug_sending(src:node,dst:node,m:msg.t)
|
||||
action debug_recving(dst:node,m:msg.t)
|
||||
action debug_sending(src:node,dst:node,m:msg)
|
||||
action debug_recving(dst:node,m:msg)
|
||||
|
||||
implement net.recv(dst:node,m:msg.t) {
|
||||
implement net.recv(dst:node,m:msg) {
|
||||
call debug_recving(dst,m);
|
||||
if m.m_kind = msg_kind.request_vote {
|
||||
if m.kind = msg_kind.request_vote {
|
||||
call request_vote.handle(dst,m)
|
||||
}
|
||||
else if m.m_kind = msg_kind.vote {
|
||||
else if m.kind = msg_kind.vote {
|
||||
call vote.handle(dst,m)
|
||||
}
|
||||
else if m.m_kind = msg_kind.leader {
|
||||
else if m.kind = msg_kind.leader {
|
||||
call leader.handle(dst,m)
|
||||
}
|
||||
}
|
||||
|
|
@ -181,6 +183,9 @@ isolate shim = {
|
|||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
private {
|
||||
invariant net.spec.sent(M,D) -> sent(M,D)
|
||||
}
|
||||
|
||||
|
|
@ -189,60 +194,66 @@ isolate shim = {
|
|||
|
||||
isolate toy_system = {
|
||||
|
||||
invariant [safe] shim.sent(M1) & M1.kind = shim.msg_kind.leader
|
||||
& shim.sent(M2) & M2.kind = shim.msg_kind.leader
|
||||
-> M1.src = M2.src
|
||||
|
||||
relation alreadyvoted(N:node)
|
||||
function voters(N:node) : nset
|
||||
|
||||
after init procedure init(self : node) {
|
||||
specification {
|
||||
invariant [safe] forall M1:msg, M2:msg.
|
||||
shim.sent(M1,N1) & M1.kind = msg_kind.leader
|
||||
& shim.sent(M2,N2) & M2.kind = msg_kind.leader
|
||||
-> M1.src = M2.src
|
||||
}
|
||||
|
||||
after init (self : node) {
|
||||
alreadyvoted(self) := false;
|
||||
voters(self) := nset.emptyset()
|
||||
}
|
||||
|
||||
action request_vote(self : node) {
|
||||
var msg : shim.msg;
|
||||
msg.kind := shim.msg_kind.request_vote;
|
||||
msg.src = self;
|
||||
shim.bcast(msg);
|
||||
if ~alreadyvoted(self) {
|
||||
alreadyvoted(self) := true
|
||||
voters(self) := voters.add(self);
|
||||
toy_protocol.vote(self,self) # ghost
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
implement shim.request_vote.handle(self : node, req : shim.msg) {
|
||||
action request_vote(self : node) = {
|
||||
var msg : msg;
|
||||
msg.kind := msg_kind.request_vote;
|
||||
msg.src := self;
|
||||
call shim.bcast(self,msg);
|
||||
if ~alreadyvoted(self) {
|
||||
alreadyvoted(self) := true;
|
||||
var reply : shim.msg;
|
||||
reply.kind := shim.msg_kind.vote;
|
||||
reply.src := self;
|
||||
reply.vote := req.src;
|
||||
shim.bcast(self,reply);
|
||||
toy_protocol.vote(self,req.src)
|
||||
voters(self) := voters(self).add(self);
|
||||
call toy_protocol.vote(self,self) # ghost
|
||||
}
|
||||
}
|
||||
|
||||
action receive vote(self : node, req : shim.msg) {
|
||||
voters(self) := voters.self.add(req.src);
|
||||
if nset.majority(voters(self)) {
|
||||
reply : shim.msg;
|
||||
reply.kind := shim.msg.leader;
|
||||
|
||||
implement shim.request_vote.handle(self : node, req : msg) {
|
||||
if ~alreadyvoted(self) {
|
||||
alreadyvoted(self) := true;
|
||||
var reply : msg;
|
||||
reply.kind := msg_kind.vote;
|
||||
reply.src := self;
|
||||
shim.bcast(self,reply);
|
||||
toy protocol.become_leader(self, voters(self)) # ghost
|
||||
reply.vote := req.src;
|
||||
call shim.bcast(self,reply);
|
||||
call toy_protocol.vote(self,req.src)
|
||||
}
|
||||
}
|
||||
|
||||
implement shim.vote.handle(self : node, req : msg) {
|
||||
if req.vote = self {
|
||||
voters(self) := voters(self).add(req.src);
|
||||
if nset.majority(voters(self)) {
|
||||
var reply : msg;
|
||||
reply.kind := msg_kind.leader;
|
||||
reply.src := self;
|
||||
call shim.bcast(self,reply);
|
||||
call toy_protocol.become_leader(self, voters(self)) # ghost
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private {
|
||||
|
||||
invariant shim.sent(M) & M.kind = shim.msg_kind.vote -> toy_protocol.voted(M.src, M.vote)
|
||||
# invariant shim.sent(M) & M.kind = shim.msg_kind.request -> toy_protocol.voted(M.src,M.src)
|
||||
invariant forall M:msg. shim.sent(M,N) & M.kind = msg_kind.vote -> toy_protocol.voted(M.src, M.vote)
|
||||
# invariant shim.sent(M) & M.kind = msg_kind.request -> toy_protocol.voted(M.src,M.src)
|
||||
invariant nset.member(N1 ,voters(N2)) -> toy_protocol.voted(N1,N2)
|
||||
invariant shim.sent(M) & M.kind = shim.msg_kind.leader -> toy protocol.isleader(M.src)
|
||||
invariant forall M:msg. shim.sent(M,N) & M.kind = msg_kind.leader -> toy_protocol.isleader(M.src)
|
||||
invariant toy_protocol.voted(N1,N2) -> alreadyvoted(N1)
|
||||
|
||||
}
|
||||
|
|
@ -252,5 +263,6 @@ isolate toy_system = {
|
|||
|
||||
} with nset, toy_protocol, shim
|
||||
|
||||
export toy_protocol.vote
|
||||
export toy_protocol.become_leader
|
||||
export toy_system.request_vote
|
||||
|
||||
extract iso_impl(self:node) = toy_system(self),shim(self),net(self),nset,node
|
||||
|
|
|
|||
|
|
@ -326,7 +326,7 @@ class Variable(Term):
|
|||
|
||||
class MethodCall(Term):
|
||||
def __str__(self):
|
||||
return str(args[0]) + '.' + str(args[1])
|
||||
return str(self.args[0]) + '.' + str(self.args[1])
|
||||
|
||||
class Literal(AST):
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -121,9 +121,21 @@ class TopContext(Context):
|
|||
self.actions = actions
|
||||
self.name = 'top_context'
|
||||
|
||||
class EmptyVariableContext(object):
|
||||
def __init__(self):
|
||||
self.map = dict()
|
||||
|
||||
class VariableContext(Context):
|
||||
def __init__(self,vs):
|
||||
self.map = dict(variable_context.map.iteritems())
|
||||
for v in vs:
|
||||
self.map[v.name] = v.sort
|
||||
self.name = 'variable_context'
|
||||
|
||||
return_context = None
|
||||
expr_context = None
|
||||
top_context = None
|
||||
variable_context = EmptyVariableContext()
|
||||
|
||||
def pull_args(args,num,sym,top):
|
||||
if len(args) < num:
|
||||
|
|
@ -236,10 +248,13 @@ def compile_app(self):
|
|||
|
||||
def compile_method_call(self):
|
||||
with ReturnContext(None):
|
||||
obj = self.args[0].compile()
|
||||
child_name = self.args[1].relname
|
||||
base = self.args[0].compile()
|
||||
child_name = self.args[1].rep
|
||||
args = [a.compile() for a in self.args[1].args]
|
||||
sort = base.sort
|
||||
if ivy_logic.is_topsort(sort):
|
||||
raise IvyError(self,'cannot apply method notation to {} because its type is not inferred'.format(base))
|
||||
|
||||
# trucky: we first look for the method as a child of the sort.
|
||||
# if not found, we look for a sibling of the sort
|
||||
destr_name = iu.compose_names(sort.name,child_name)
|
||||
|
|
@ -255,7 +270,7 @@ def compile_method_call(self):
|
|||
args.insert(0,base)
|
||||
return sym(*args)
|
||||
|
||||
|
||||
ivy_ast.MethodCall.cmpl = compile_method_call
|
||||
|
||||
def cmpl_sort(sortname):
|
||||
return ivy_logic.find_sort(resolve_alias(sortname))
|
||||
|
|
@ -269,7 +284,16 @@ ivy_ast.NativeExpr.cmpl = cmpl_native_expr
|
|||
|
||||
ivy_ast.App.cmpl = ivy_ast.Atom.cmpl = compile_app
|
||||
|
||||
ivy_ast.Variable.cmpl = lambda self: ivy_logic.Variable(self.rep,cmpl_sort(self.sort) if isinstance(self.sort,str) else self.sort)
|
||||
def variable_sort(self):
|
||||
return cmpl_sort(self.sort) if isinstance(self.sort,str) else self.sort
|
||||
|
||||
def compile_variable(self):
|
||||
sort = variable_sort(self)
|
||||
if ivy_logic.is_topsort(sort):
|
||||
sort = variable_context.map.get(self.rep,sort)
|
||||
return ivy_logic.Variable(self.rep,sort)
|
||||
|
||||
ivy_ast.Variable.cmpl = compile_variable
|
||||
|
||||
ivy_ast.ConstantSort.cmpl = lambda self,name: ivy_logic.ConstantSort(name)
|
||||
|
||||
|
|
@ -280,7 +304,12 @@ SymbolList.cmpl = lambda self: self.clone([find_symbol(s) for s in self.symbols]
|
|||
def cquant(q):
|
||||
return ivy_logic.ForAll if isinstance(q,ivy_ast.Forall) else ivy_logic.Exists
|
||||
|
||||
ivy_ast.Quantifier.cmpl = lambda self: cquant(self)([v.compile() for v in self.bounds],self.args[0].compile())
|
||||
def compile_quantifier(self):
|
||||
bounds = [ivy_logic.Variable(v.rep,variable_sort(v)) for v in self.bounds]
|
||||
with VariableContext(bounds):
|
||||
return cquant(self)(bounds,self.args[0].compile())
|
||||
|
||||
ivy_ast.Quantifier.cmpl = compile_quantifier
|
||||
|
||||
ivy_ast.NamedBinder.cmpl = lambda self: ivy_logic.NamedBinder(
|
||||
self.name,
|
||||
|
|
@ -523,7 +552,11 @@ def compile_native_arg(arg):
|
|||
if arg.rep in ivy_logic.sig.symbols:
|
||||
return sortify_with_inference(arg)
|
||||
res = arg.clone(map(sortify_with_inference,arg.args)) # handles action names
|
||||
return res.rename(resolve_alias(res.rep))
|
||||
iu.dbg('res')
|
||||
res1 = res.rename(resolve_alias(res.rep))
|
||||
iu.dbg('res1')
|
||||
return res1
|
||||
|
||||
|
||||
def compile_native_symbol(arg):
|
||||
name = arg.rep
|
||||
|
|
@ -552,7 +585,9 @@ def compile_native_name(atom):
|
|||
def compile_native_def(self):
|
||||
fields = self.args[1].code.split('`')
|
||||
args = [compile_native_name(self.args[0]),self.args[1]] + [compile_native_arg(a) if not fields[i*2].endswith('"') else compile_native_symbol(a) for i,a in enumerate(self.args[2:])]
|
||||
return self.clone(args)
|
||||
cres = self.clone(args)
|
||||
iu.dbg('cres')
|
||||
return cres
|
||||
|
||||
def compile_action_def(a,sig):
|
||||
sig = sig.copy()
|
||||
|
|
@ -874,13 +909,14 @@ class IvyDomainSetup(IvyDeclInterp):
|
|||
def interpret(self,thing):
|
||||
sig = self.domain.sig
|
||||
interp = sig.interp
|
||||
lhs = resolve_alias(thing.formula.args[0].rep)
|
||||
iu.dbg('lhs')
|
||||
if isinstance(thing.formula.args[1],ivy_ast.NativeType):
|
||||
lhs = thing.formula.args[0].rep
|
||||
if lhs in interp or lhs in self.domain.native_types :
|
||||
raise IvyError(thing,"{} is already interpreted".format(lhs))
|
||||
self.domain.native_types[lhs] = thing.formula.args[1]
|
||||
return
|
||||
lhs,rhs = (a.rep for a in thing.formula.args)
|
||||
rhs = thing.formula.args[1].rep
|
||||
self.domain.interps[lhs].append(thing)
|
||||
if lhs in self.domain.native_types :
|
||||
raise IvyError(thing,"{} is already interpreted".format(lhs))
|
||||
|
|
|
|||
|
|
@ -220,26 +220,27 @@ def strip_sort(sort,strip_params):
|
|||
return ivy_logic.FunctionSort(*(dom+[sort.rng]))
|
||||
return sort.rng
|
||||
|
||||
def strip_action(ast,strip_map,strip_binding):
|
||||
def strip_action(ast,strip_map,strip_binding,is_init=False):
|
||||
if isinstance(ast,ia.CallAction):
|
||||
name = canon_act(ast.args[0].rep)
|
||||
args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args[0].args]
|
||||
args = [strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args[0].args]
|
||||
strip_params = get_strip_params(name,ast.args[0].args,strip_map,strip_binding,ast)
|
||||
call = ast.args[0].clone(args[len(strip_params):])
|
||||
return ast.clone([call]+[strip_action(arg,strip_map,strip_binding) for arg in ast.args[1:]])
|
||||
return ast.clone([call]+[strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args[1:]])
|
||||
if isinstance(ast,ia.Action):
|
||||
for sym in ast.modifies():
|
||||
if sym.name in ivy_logic.sig.symbols:
|
||||
lhs_params = strip_map_lookup(sym.name,strip_map)
|
||||
if len(lhs_params) != num_isolate_params:
|
||||
raise iu.IvyError(ast,"assignment may be interfering")
|
||||
if not (len(lhs_params) == 0 and len(strip_binding) == 0 and is_init):
|
||||
raise iu.IvyError(ast,"assignment may be interfering")
|
||||
if (ivy_logic.is_constant(ast) or ivy_logic.is_variable(ast)) and ast in strip_binding:
|
||||
sname = strip_binding[ast]
|
||||
if sname not in ivy_logic.sig.symbols:
|
||||
ivy_logic.add_symbol(sname,ast.sort)
|
||||
strip_added_symbols.append(ivy_logic.Symbol(sname,ast.sort))
|
||||
return ivy_logic.Symbol(sname,ast.sort)
|
||||
args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args]
|
||||
args = [strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args]
|
||||
if ivy_logic.is_app(ast):
|
||||
name = ast.rep.name
|
||||
strip_params = get_strip_params(name,ast.args,strip_map,strip_binding,ast)
|
||||
|
|
@ -348,7 +349,7 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip):
|
|||
strip_binding = dict(zip(action.formal_params,strip_params))
|
||||
# if isinstance(action,ia.NativeAction) and len(strip_params) != num_isolate_params:
|
||||
# raise iu.IvyError(None,'foreign function {} may be interfering'.format(name))
|
||||
new_action = strip_action(action,strip_map,strip_binding)
|
||||
new_action = strip_action(action,strip_map,strip_binding,is_init=name.endswith('init[after]'))
|
||||
new_action.formal_params = action.formal_params[len(strip_params):]
|
||||
new_action.formal_returns = action.formal_returns
|
||||
new_actions[name] = new_action
|
||||
|
|
@ -1687,13 +1688,14 @@ def check_isolate_completeness(mod = None):
|
|||
|
||||
|
||||
def iter_isolate(mod,iso,fun,verified=True,present=True):
|
||||
suff = "spec" if isinstance(iso,ivy_ast.ExtractDef) else "impl"
|
||||
def recur(name):
|
||||
fun(name)
|
||||
for child in mod.hierarchy[name]:
|
||||
cname = iu.compose_names(name,child)
|
||||
if not(child == "impl"
|
||||
or iu.compose_names(name,'impl') in mod.attributes
|
||||
or iu.compose_names(name,'private') in mod.attributes):
|
||||
if not(child == suff
|
||||
or iu.compose_names(cname,suff) in mod.attributes
|
||||
or iu.compose_names(cname,'private') in mod.attributes):
|
||||
recur(cname)
|
||||
|
||||
if verified:
|
||||
|
|
|
|||
|
|
@ -355,12 +355,12 @@ def p_fmla_fmla_iff_fmla(p):
|
|||
p[0].lineno = get_lineno(p,2)
|
||||
|
||||
def p_fmla_forall_vars_dot_fmla(p):
|
||||
'fmla : FORALL simplevars DOT fmla'
|
||||
'fmla : FORALL simplevars DOT fmla %prec SEMI'
|
||||
p[0] = Forall(p[2],p[4])
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
def p_fmla_exists_vars_dot_fmla(p):
|
||||
'fmla : EXISTS simplevars DOT fmla'
|
||||
'fmla : EXISTS simplevars DOT fmla %prec SEMI'
|
||||
p[0] = Exists(p[2],p[4])
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
|
|
@ -382,7 +382,7 @@ def p_term_namedbinder_vars_dot_fmla(p):
|
|||
p[0].lineno = get_lineno(p,2)
|
||||
|
||||
def p_term_namedbinder_dot_fmla(p):
|
||||
'term : DOLLAR SYMBOL DOT fmla'
|
||||
'term : DOLLAR SYMBOL DOT fmla %prec SEMI'
|
||||
p[0] = NamedBinder(p[2], [],p[4])
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import ply.yacc as yacc
|
|||
# Parser for formulas
|
||||
|
||||
precedence = (
|
||||
('left', 'SEMI'),
|
||||
('left', 'GLOBALLY', 'EVENTUALLY'),
|
||||
('left', 'IF'),
|
||||
('left', 'ELSE'),
|
||||
|
|
|
|||
|
|
@ -2511,7 +2511,14 @@ def emit_one_initial_state(header):
|
|||
check_init_cond("initial condition",im.module.labeled_inits)
|
||||
check_init_cond("axiom",im.module.labeled_axioms)
|
||||
|
||||
clauses = ilu.and_clauses(im.module.init_cond,im.module.background_theory())
|
||||
constraints = [ilu.clauses_to_formula(im.module.init_cond)]
|
||||
for a in im.module.axioms:
|
||||
constraints.append(a)
|
||||
for ldf in im.relevant_definitions(ilu.symbols_asts(constraints)):
|
||||
constraints.append(fix_definition(ldf.formula).to_constraint())
|
||||
clauses = ilu.formula_to_clauses(il.And(*constraints))
|
||||
# clauses = ilu.and_clauses(im.module.init_cond,im.module.background_theory())
|
||||
iu.dbg('clauses')
|
||||
m = slv.get_model_clauses(clauses)
|
||||
if m == None:
|
||||
print clauses
|
||||
|
|
@ -2780,6 +2787,8 @@ def get_all_bounds(header,variables,body,exists,varnames):
|
|||
|
||||
|
||||
def emit_quant(variables,body,header,code,exists=False):
|
||||
iu.dbg('variables')
|
||||
iu.dbg('body')
|
||||
global indent_level
|
||||
if len(variables) == 0:
|
||||
body.emit(header,code)
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче