• Robbert Krebbers's avatar
    Step-indexed order on CMRAs · 780f6b82
    Robbert Krebbers authored
    * Remove the order from RAs, it is now defined in terms of the ⋅ operation.
    * Define ownership using the step-indexed order.
    * Remove the order also from DRAs and change STS accordingly. While doing
      that, I changed STS to no longer use decidable token sets, which removes the
      requirement of decidable equality on tokens.
    780f6b82
auth.v 2.5 KB