# Interview Dionisi
## Encodings Introduction
Go
```go=
func ex1() {
var x int = 42
x = x + 1
assert x == 45
}
```
Viper
```javascript=
method ex1() {
var x: Int := 42
x := x + 1
assert x == 45
}
```
* ENC(`var x int = e`) --> `var x: Int = ENC(e)`
* ENC(`x = e` ) --> `x := ENC(e)`
* ENC(`assert e` ) --> `assert ENC(e)`
* ENC(`42` ) --> `42`
* ENC(`a + b`) --> `ENC(a) + ENC(b)`
## Tuples
Go
```go=
var x tuple2[bool,int] = (false, 5)
var y = fst(x)
var z = snd(x)
assert y == false
```
Viper
```javascript=
domain Tuple2[A, B] {
function tuple2(x: A, y: B): Tuple2[A, B]
function fst(t: Tuple2[A, B]): A
function snd(t: Tuple2[A, B]): B
axiom {
forall x: A, y: B :: fst(tuple2(x,y)) == x && snd(tuple2(x,y)) == y
}
axiom {
forall t: Tuple2[A, B] :: tuple2(fst(t),snd(t)) == t
}
}
```
Viper
```javascript=
domain Tuple3[A, B, C] {
function tuple3(x: A, y: B, z: C): Tuple3[A, B, C]
function fst(t: Tuple3[A, B, C]): A
function snd(t: Tuple3[A, B, C]): B
function thd(t: Tuple3[A, B, C]): C
axiom {
forall x: A, y: B, z: C :: fst(tuple3(x,y,z)) == x && snd(tuple3(x,y,z)) == y && thd(tuple3(x,y,z)) == z
}
axiom {
forall t: Tuple3[A, B, C] :: tuple3(fst(t),snd(t),thd(t)) == t
}
}
```
Viper
```javascript=
domain Tuple0 {
function tuple3: Tuple0
axiom {
forall x, y: Tuple0 :: x == y
}
}
```
Go
```go=
var x tuple2[bool,int] = (false, 5)
var y = fst(x)
assert y == false
```
Viper
```javascript=
// var x tuple2[bool,int] = (false, 5)
var x : tuple2[bool, int] := tuple2(false, 5)
// TODO
// var y = fst(x)
var y: bool := fst(x)
... // TODO
// assert y == false
... // TODO
```
## Structs
Go
```go=
type student struct {
age int
enrolled bool
credits int
}
func foo() {
var felix = student{ 26, true, 120 }
var kim = student{ 31, false, 93 }
var averageCredits = felix.credits + kim.credits / 2
assert averageCredits >= 90
}
```
Viper
```javascript=
// var felix = student{ 26, true, 120 }
var felix: Tuple3[int, bool, int] := tuple3(26, true, 120)
// var y = felix.enrolled
var y : bool := snd(felix)
// felix.age = felix.age + 1
felix := tuple3(fst(felix) + 1, snd(felix), thd(felix))
```
## Memory
### Introduction
Go
```go=
func foo() {
var x *int = &1
var p = x
*p = 42
assert *x == 42
}
```
Viper
```javascript=
field left: Int
field right: Int
method ex3() {
var someObject: Ref
inhale acc(someObject.left) && acc(someObject.right)
someObject.left := 42
someObject.middle := 5 // fails
}
field middle: Int
```
Viper
```javascript=
field val: Int
method foo() {
// var x *int = &1
... // TODO
// var p = x
var p: Ref
p := x
... // TODO
// *p = 42
p.val := 42
... // TODO
// assert *x == 42
assert x.val == 42
... // TODO
}
```
### Struct
Go
```go=
type pair struct{
left, right int
}
func foo() {
var x *pair = &pair{1,2}
var y = x.left
assert y == 1
var p *int = &x.left
*p = 3
assert x.left == 3
}
```
Viper
```javascript=
// var x *pair = &pair{1,2}
var x: Tuple2[Ref, Ref]
inhale acc(fst(x).val) && acc(snd(x).val)
fst(x).val := 1
snd(x).val := 2
// var y = x.left
var y: Int := fst(x).val... // TODO
// assert y == 1
assert y == 1
// var p *int = &x.left
var p: Ref
p := fst(x)... // TODO
// *p = 3
p.val := 3
// assert x.left == 3
assert fst(x).val == 3
```
// how would ref -> pair[int, int] work
### Difference Mathematical and Memory
Go
```go=
type pair struct {
left, right int
}
func foo(x, y *pair) {
if &x.left == &y.left {
assert x == y
assert *x == *y
}
}
```
Viper
```javascript=
method ex6(x: Tuple2[Ref, Ref], y: Tuple2[Ref, Ref]) {
if (fst(x) == fst(y)) { // TODO
assert x == y // TODO
}
}
```
#### Problems
Viper
```javascript=
domain MemPair[A, B] {
function memPair(x: A, y: B): MemPair[A, B]
function memFst(t: MemPair[A, B]): A
function memSnd(t: MemPair[A, B]): B
axiom {
forall x: A, y: B :: memFst(memPair(x,y)) == x && memSnd(memPair(x,y)) == y
}
axiom {
forall t: MemPair[A, B] :: memPair(memFst(t), memSnd(t)) == t
}
axiom {
forall t1, t2: MemPair[A, B] :: memFst(t1) == memFst(t2) -> t1 == t2
}
}
```
Viper
```javascript=
var x: MemPair[Int, Int] := memPair(3, 4)
var y: MemPair[Int, Int] := memPair(3, 5)
assert false
```
#### Solution
Viper
```javascript=
domain MemPairY[A, B] {
function memFstY(t: MemPair[A, B]): A
function memSndY(t: MemPair[A, B]): B
axiom {
forall t1, t2: MemPair[A, B] :: ( memFstY(t1) == memFstY(t2) ==> t1 == t2 ) && ( memSndY(t1) == memSndY(t2) ==> t1 == t2 )
}
... // TODO
}
```
Viper
```javascript=
method ex10() {
// var x *pair = &pair{1,2}
var l : Ref
inhale acc(l.val)
l.val := 1
var r : Ref
inhale acc(r.val)
r.val := 2
var x : MemPairY[Ref, Ref]
assume memFst(x) = l /\ memSnd(x) = r
}
```
Google Drive
Gist
Clipboard
Sign in with Wallet
