Skip to content
  • David Swasey's avatar
    Added (optional) safety. It's optional for my work on security · 6de81061
    David Swasey authored
    protocols where I want to prove something called robust safety.
    Ironically, to even state robust safety requires Hoare triples that
    don't imply safety. So Iris supports both {P} e {Q} (implying safety)
    and [P] e [Q] (not). I'll add a rule for forgetting about safety:
    
    	{P} e {Q}
    	— Unsafe
    	[P] e [Q]
    
    some time soon.
    
    Aside: I'm an SSReflect weenie and know next to nothing about the
    usual Coq tactics. My proof script changes likely reflect that fact.
    6de81061