From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 25 Apr 2021 17:05:32 +0000 (+0100)
Subject: authproofs: Document proof obligations
X-Git-Tag: otter-0.6.0~524
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=7a4652abc63a2acd7890802e80ff431e641c1565;p=otter.git

authproofs: Document proof obligations

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---

diff --git a/src/authproofs.rs b/src/authproofs.rs
index c04752fa..c3587318 100644
--- a/src/authproofs.rs
+++ b/src/authproofs.rs
@@ -31,15 +31,19 @@ impl<A> Copy for Authorisation<A> { }
 pub type AuthorisationSuperuser = Authorisation<Global>;
 
 impl<T> Authorisation<T> {
+  /// Proof obligation: access to this `T` has been authorised.
   pub const fn authorised(_v: &T) -> Authorisation<T> {
     Authorisation(PhantomData)
   }
   pub fn map<U>(self, _f: fn(&T) -> &U) -> Authorisation<U> {
     self.therefore_ok()
   }
+  /// Minor proof obligation: in this case, authorised access to `T`
+  /// implies authorised access to `U`.
   pub fn therefore_ok<U>(self) -> Authorisation<U> {
     Authorisation(PhantomData)
   }
+  /// Proof obligation: access to `T` has been authorised.
   pub const fn authorise_any() -> Authorisation<T> {
     Authorisation(PhantomData)
   }