microsoft
/
ivy
зеркало из https://github.com/microsoft/ivy.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

added mc schemata to std include

This commit is contained in:
Ken McMillan 2018-02-23 13:26:06 -08:00
Родитель 836e634f65
Коммит 796e595082
6 изменённых файлов: 216 добавлений и 294 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

156
ivy/include/1.7/mc_schemata.ivy Normal file
Просмотреть файл

@ -0,0 +1,156 @@
#lang ivy1.7
schema trans1 = {
type t
function x : t
function z : t
property x = X & z = X -> x = z
}
schema trans2 = {
type t
function x : t
property Y = X -> (x = X <-> x = Y)
}
schema contra = {
type t
function x : t
property Y ~= X -> ~(x = X & x = Y)
}
schema cong1 = {
type t
type u
function x : t
function y : u
function f1(X:t) : u
property (f1(X) = y <-> f1(x) = y) | x ~= X
}
schema cong1b = {
type t
type u_finite
function x : t
function f2(X:t) : u_finite
property (f2(X) = f2(x)) | x ~= X
}
schema cong2 = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function y : u
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
}
schema cong2b = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
}
schema cong3 = {
type t1
type t2
type t3
type u
function x1 : t1
function x2 : t2
function x3 : t3
function y : u
function f1(X1:t1,X2:t2,X3:t3) : u
property (f1(X1,X2,X3) = y <-> f1(x1,x2,x3) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
}
schema cong3b = {
type t1
type t2
type t3
type u
function x1 : t1
function x2 : t2
function x3 : t3
function f1(X1:t1,X2:t2,X3:t3) : u
property (f1(X1,X2,X3) = f1(x1,x2,x3)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
}
schema cong4 = {
type t1
type t2
type t3
type t4
type u
function x1 : t1
function x2 : t2
function x3 : t3
function x4 : t4
function y : u
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
property (f1(X1,X2,X3,X4) = y <-> f1(x1,x2,x3,x4) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
}
schema cong4b = {
type t1
type t2
type t3
type t4
type u
function x1 : t1
function x2 : t2
function x3 : t3
function x4 : t4
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
property (f1(X1,X2,X3,X4) = f1(x1,x2,x3,x4)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
}
module total_order_schemata(t) = {
schema lt1 = {
function x1 : t
property ~(X < Y & Y < x1 & x1 < X)
}
schema lt2 = {
function x1 : t
property ~(~(X < Y) & ~(x1 < X) & x1 < Y)
}
schema lt3 = {
function x1 : t
property Y = X -> (x1 < X <-> x1 < Y)
}
schema lt4 = {
type t1
type t2
function x1 : t1
function x2 : t2
function x : t
function f1(X1:t1,X2:t2) : t
property (x < f1(X1,X2) <-> x < f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
}
schema lt5 = {
function x1 : t
property X = x1 -> ~(X < x1) & ~(x1 < X)
}
schema lt6 = {
type t1
type t2
function x1 : t1
function x2 : t2
function x : t
function f1(X1:t1,X2:t2) : t
property (f1(X1,X2) = 0 <-> f1(x1,x2) = 0) | x1 ~= X1 | x2 ~= X2
}
}

2
ivy/ivy_mc.py
Просмотреть файл

@ -507,6 +507,8 @@ class Match(object):
del self.map[x]
def unify(self,x,y):
if x not in self.map:
if x.name.endswith('_finite') and not is_finite_sort(y):
return False #
self.add(x,y)
return True
return self.map[x] == y

106
test/flash2_mc.ivy
Просмотреть файл

@ -512,67 +512,69 @@ invariant [l6]
invack(X) & dir.real(X) -> dir.pending & collecting
proof let H = home
schema trans1 = {
type t
function x : t
function z : t
property x = X & z = X -> x = z
}
include mc_schemata
schema trans2 = {
type t
function x : t
property Y = X -> (x = X <-> x = Y)
}
# schema trans1 = {
# type t
# function x : t
# function z : t
# property x = X & z = X -> x = z
# }
schema contra = {
type t
function x : t
property Y ~= X -> ~(x = X & x = Y)
}
# schema trans2 = {
# type t
# function x : t
# property Y = X -> (x = X <-> x = Y)
# }
# schema contra = {
# type t
# function x : t
# property Y ~= X -> ~(x = X & x = Y)
# }
# # schema cong1 = {
# # type t
# # type u
# # function x : t
# # function f1(X:t) : u
# # property x = X -> f1(x) = f1(X)
# # }
# schema cong1 = {
# type t
# type u
# function x : t
# function y : u
# function f1(X:t) : u
# property x = X -> f1(x) = f1(X)
# property (f1(X) = y <-> f1(x) = y) | x ~= X
# }
schema cong1 = {
type t
type u
function x : t
function y : u
function f1(X:t) : u
property (f1(X) = y <-> f1(x) = y) | x ~= X
}
# schema cong1b = {
# type t
# type u
# function x : t
# function f2(X:t) : u
# property (f2(X) = f2(x)) | x ~= X
# }
schema cong1b = {
type t
type u
function x : t
function f2(X:t) : u
property (f2(X) = f2(x)) | x ~= X
}
# schema cong2 = {
# type t1
# type t2
# type u
# function x1 : t1
# function x2 : t2
# function y : u
# function f1(X1:t1,X2:t2) : u
# property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
# }
schema cong2 = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function y : u
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
}
schema cong2b = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
}
# schema cong2b = {
# type t1
# type t2
# type u
# function x1 : t1
# function x2 : t2
# function f1(X1:t1,X2:t2) : u
# property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
# }

31
test/ibm-cache-N_mc.ivy
Просмотреть файл

@ -114,36 +114,7 @@ invariant forall C1, C2. C1 ~= C2 & s.cache(C1) = exclusive -> s.cache(C2) = inv
invariant s.homeexclusiveGranted & s.homeCurrentCommand ~= empty1 & s.channel3(C1) = invalidateAck -> C1 = owner
schema trans1 = {
type t
function x : t
function z : t
property x = X & z = X -> x = z
}
schema trans2 = {
type t
function x : t
property x = X & Y = X -> x = Y
}
schema cong1 = {
type t
type u
function x : t
function f(X:t) : u
property x = X -> f(x) = f(X)
}
schema cong2 = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function f(X1:t1,X2:t2) : u
property x1 = X1 & x2 = X2 -> f(x1,x2) = f(X1,X2)
}
include mc_schemata
export reqsharedRule

54
test/toma8_mc.ivy
Просмотреть файл

@ -284,57 +284,5 @@ object toma = {
export toma.step
schema trans1 = {
type t
function x : t
function z : t
property x = X & z = X -> x = z
}
include mc_schemata
schema trans2 = {
type t
function x : t
property Y = X -> (x = X <-> x = Y)
}
schema contra = {
type t
function x : t
property Y ~= X -> ~(x = X & x = Y)
}
# schema cong1 = {
# type t
# type u
# function x : t
# function f1(X:t) : u
# property x = X -> f1(x) = f1(X)
# }
schema cong1 = {
type t
type u
function x : t
function y : u
function f1(X:t) : u
property (f1(X) = y <-> f1(x) = y) | x ~= X
}
schema cong1b = {
type t
type u
function x : t
function f2(X:t) : bool
property (f2(X) <-> f2(x)) | x ~= X
}
schema cong2 = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function y : u
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
}

161
test/vsync_paxos.ivy
Просмотреть файл

@ -276,162 +276,5 @@ export do_vote
export decide
schema trans1 = {
type t
function x : t
function z : t
property x = X & z = X -> x = z
}
schema trans2 = {
type t
function x : t
property Y = X -> (x = X <-> x = Y)
}
schema contra = {
type t
function x : t
property Y ~= X -> ~(x = X & x = Y)
}
# schema cong1 = {
# type t
# type u
# function x : t
# function f1(X:t) : u
# property x = X -> f1(x) = f1(X)
# }
schema cong1 = {
type t
type u
function x : t
function y : u
function f1(X:t) : u
property (f1(X) = y <-> f1(x) = y) | x ~= X
}
schema cong1b = {
type t
function x : t
function f2(X:t) : bool
property (f2(X) = f2(x)) | x ~= X
}
schema cong2 = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function y : u
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
}
schema cong2b = {
type t1
type t2
type u
function x1 : t1
function x2 : t2
function f1(X1:t1,X2:t2) : u
property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
}
schema cong3 = {
type t1
type t2
type t3
type u
function x1 : t1
function x2 : t2
function x3 : t3
function y : u
function f1(X1:t1,X2:t2,X3:t3) : u
property (f1(X1,X2,X3) = y <-> f1(x1,x2,x3) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
}
schema cong3b = {
type t1
type t2
type t3
type u
function x1 : t1
function x2 : t2
function x3 : t3
function f1(X1:t1,X2:t2,X3:t3) : u
property (f1(X1,X2,X3) = f1(x1,x2,x3)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
}
schema cong4 = {
type t1
type t2
type t3
type t4
type u
function x1 : t1
function x2 : t2
function x3 : t3
function x4 : t4
function y : u
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
property (f1(X1,X2,X3,X4) = y <-> f1(x1,x2,x3,x4) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
}
schema cong4b = {
type t1
type t2
type t3
type t4
type u
function x1 : t1
function x2 : t2
function x3 : t3
function x4 : t4
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
property (f1(X1,X2,X3,X4) = f1(x1,x2,x3,x4)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
}
schema lt1 = {
function x1 : stake
property ~(X < Y & Y < x1 & x1 < X)
}
schema lt2 = {
function x1 : stake
property ~(~(X < Y) & ~(x1 < X) & x1 < Y)
}
schema lt3 = {
function x1 : stake
property Y = X -> (x1 < X <-> x1 < Y)
}
schema lt4 = {
type t1
type t2
function x1 : t1
function x2 : t2
function x : stake
function f1(X1:t1,X2:t2) : stake
property (x < f1(X1,X2) <-> x < f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
}
schema lt5 = {
function x1 : stake
property X = x1 -> ~(X < x1) & ~(x1 < X)
}
schema lt6 = {
type t1
type t2
function x1 : t1
function x2 : t2
function x : stake
function f1(X1:t1,X2:t2) : stake
property (f1(X1,X2) = 0 <-> f1(x1,x2) = 0) | x1 ~= X1 | x2 ~= X2
}
include mc_schemata
instantiate total_order_schemata(stake)