// Exercise 2: gcd by repeated subtraction (subtractive Euclid). Fill in the
// loop invariant(s) so that the postcondition goes through. (We're only asking
// for a common divisor bound here, not a proof that `r` is the *greatest*
// common divisor -- that needs more machinery than this exercise is about.)
proc gcd(a: Int, b: Int) returns (r: Int)
  requires a > 0 && b > 0
  ensures r > 0 && r <= a && r <= b
{
  var x := a
  var y := b
  while (x != y)
    invariant true // TODO: replace with a real invariant
  {
    if (x > y) {
      x := x - y
    } else {
      y := y - x
    }
  }
  r := x
}