Proof size

• Two main modules:

  SeparationProof: 3-4 screen-fulls

  proves CondSeparation (separation holds provided the observed channel algorithm is well-behaved)

  GoodAlgProof: 3-4 screen-fulls

  proves AllGoodAlgs (thanks to memory protection, all algorithms are well-behaved)

• total proof file sizes in bytes: 23k+22k+... = 85k (11k compressed)
• Total program+properties size in bytes: 14k (4.5k compressed)