```// A port of the proof of Peterson's Algorithm from:
// http://homes.cs.washington.edu/~jrw12/SharedMem.html
//
// Look ma, no proofs!
//
// James R. Wilcox
// January 9, 2017

// There are six possible PCs for each thread, each corresponding to
// the beginning of one atomic step.
datatype PC = SetFlag | SetVictim | CheckFlag | CheckVictim | Crit | ResetFlag

method Peterson()
decreases *
{
// Thread ids will be ints 0 or 1.
// Below, we will use 1-t to get the "other" tid from a tid t.

// We store some variables in arrays so that we can write the code
// for both threads at once, indexed by the thread id.
var flag := new bool[2];
flag[0] := false;
flag[1] := false;

// The algorithm is correct regardless of the initial value of
// victim, so we initialize in nondeterministically.
var victim;
if * {
victim := 0;
} else {
victim := 1;
}

var pc := new PC[2];
pc[0] := SetFlag;
pc[1] := SetFlag;

while true
// Invariant 1: whenever t's flag is false, its PC is at SetFlag.
//
// Comment this out to see that it is required by Invariant 2.
invariant forall t :: 0 <= t < 2 && !flag[t] ==> pc[t] == SetFlag

// Invariant 2: If t holds the lock and 1-t is trying to get it,
//              then victim == 1-t. (victim != t works too!).
//
// Comment this out to see that it is required by the mutual
// exclusion invariant below!
//
// Writing the invariant like this, using t' to represent the
// other thread, avoids a trigger matching loop.
invariant forall t, t' :: 0 <= t < 2 ==> t' == 1-t ==>
(pc[t] == Crit || pc[t] == ResetFlag) ==>
(pc[t'] == CheckVictim || pc[t'] == CheckFlag ||
pc[t'] == Crit || pc[t'] == ResetFlag) ==>
victim != t

// This is mutual exclusion: It is never the case that both
// threads are in the critical section.
//
// This is directly implied by Invariant 2, since if both PCs are
// Crit, then the victim cannot be equal to either thread.
//
// Dafny is clever enough to infer an additional loop invariant,
// namely 0 <= victim < 2, which is required to complete the proof.
invariant !(pc[0] == Crit && pc[1] == Crit)

decreases *
{
// Each iteration of the loop simulates one atomic step of execution.

// First, nondeterministically select the thread that gets to step.
var t;
if * {
t := 0;
} else {
t := 1;
}

// Now, branch on the selected thread's current PC and execute the
// corresponding atomic step.
//
// Note that each step only reads or writes one shared variable.
match pc[t] {
case SetFlag     => flag[t] := true; pc[t] := SetVictim;
case SetVictim   => victim := t; pc[t] := CheckFlag;
case CheckFlag   => pc[t] := if flag[1-t] then CheckVictim else Crit;
case CheckVictim => pc[t] := if victim == t then CheckFlag else Crit;
case Crit        => pc[t] := ResetFlag;
case ResetFlag   => flag[t] := false; pc[t] := SetFlag;
}
}
}
```