Add code examples showing the need for synchronization

[cacay]

The PickANumber example demonstrates a bug in the compiler. The problem isn't with synchronization, however. It is to do with where declassify operations are performed. An operation let y = declassify x to l must be placed on a protocol that can read x, but we only require that it is placed on a protocol that can read y. This is a strictly bigger set of protocols, and causes certain values to be reveal before they should.

[codecov]

Codecov Report

Merging #344 (d1d6dd2) into master (f3ead9d) will not change coverage.
The diff coverage is n/a.

@@            Coverage Diff            @@
##             master     #344   +/-   ##
=========================================
  Coverage     58.96%   58.96%           
  Complexity     1128     1128           
=========================================
  Files           233      233           
  Lines          9094     9094           
  Branches       1362     1362           
=========================================
  Hits           5362     5362           
  Misses         3468     3468           
  Partials        264      264           

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f3ead9d...d1d6dd2. Read the comment docs.