---
# System prepended metadata

title: Interview Dionisi

---

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

```