# Interview Mihail
## Encodings Introduction
Go
```go=
func ex1() {
var x int = 42
x = x + 1
assert x == 43
}
```
Viper
```javascript=
method ex1() {
var x: Int := 42
x := x + 1
assert x == 43
}
```
* 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)
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=
var x: Tuple2[Bool, Int] := tuple2(false, 5)
var y: Bool := fst(x)
assert y == false
```
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)
axiom {
forall x: A, y:B, z:C :: fst(tuple3(x,y,z)) == x && snd(tuple3(x,y,z)) == y && trd(tuple3(x,y,z) == z))
}
axiom {
forall t: Tuple3[A, B, C] :: tuple3(fst(t), snd(t), trd(t)) == t
}
}
```
Viper
```javascript=
domain Tuple0[] {
function tuple0() : Tuple0[]
axiom {
forall t: Tuple0[] :: tuple0() == t
}
}
```
## 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(26, true, 120)
```
Go
```go=
type student struct {
age int
enrolled bool
credits int
}
func foo() {
var felix = student{ 26, true, 120 }
felix.age = felix.age + 1 // ?
}
type aux struct {
st student
id int
}
```
Viper
```javascript=
var felix := tuple3(26, true, 120)
felix := tuple3(fst(felix) + 1, snd(felix), trd(felix))
... // TODO
Enc( x.age = e2 ) --> x := tuple3(Enc(e2), snd(x), trd(x))
Enc( x.st.age = e2) --> x := tuple2(tuple3(Enc(e2), snd(fst(x)), trd( fst(x))), snd(x))
Enc( e1.age = e2 ) -->
Enc( e1 = (e2,snd(e1)) )
e ::= x | e.f
```
## Memory
### Introduction
Go
```go=
func foo() {
var x *int = &1
var p = x
*p = 42
assert *x == 42
}
```
Viper
```javascript=
field val: Int
method ex3() {
var x: Ref
inhale acc(x.val)
x.val := 1
var p := x
p.val := 42
assert x.val == 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
```
### Int Pointer
Viper
```javascript=
method foo() {
// var x *int = &1
... // TODO
// var p = x
... // TODO
// *p = 42
... // TODO
// assert *x == 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
// var z = *x
var z: Tuple2[Int, Int] := // TODO
```
### 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
}
}
```
Viper
```javascript=
method foo(x: MemPair[Ref, Ref], y: MemPair[Ref, Ref]) {
if (fst(x) == fst(y) ) {
assert x == y
}
}
```
Viper
```javascript=
domain MemPair[A, B] {
function memFst(t: MemPair[A, B]): A
function memSnd(t: MemPair[A, B]): B
axiom { // TODO
forall t1: MemPair[A, B], t2: MemPair[A,B] :: fst(t1) == fst(t2) ==> t1 == t2
}
}
```
Viper
```javascript=
method ex10() {
// var x *pair = &pair{1,2}
... // TODO
}
```
Google Drive
Gist
Clipboard
Sign in with Wallet
