notebook.spec 263 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Workflow

loop {
	choose {
		forallmay x:User, i:Info
			Written(i, x) → Read += (x, i)
	} {
		forallmay x:User, i:Info
			Oracle(i, x) → Written += (i, x)
	}
}

Declassify

Oracle(i:Info,x:User): F (Written(u:User, i:Info))

Target

Read(u:User, info:Info)