---
# System prepended metadata

title: Interview Mihail

---

# 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
}

```