Add comment from rust version

src/ir/auth_logic/lowering_ast_datalog.h

@@ -35,6 +35,92 @@ namespace raksha::ir::auth_logic {
 // (Internally, this is a stateful class because it uses a counter to
 // generate fresh names for arguments. The public interface hides this
 // implementation detail.)
+
+//-----------------------------------------------------------------------------
+// Description of Translation
+//-----------------------------------------------------------------------------
+// Asside from queries, this translation is quite similar to the one given in
+// Section 7 of the SecPal paper "SecPAL: Design and Semantics of a Decentralized
+// Authorization Language"
+// https://www.pure.ed.ac.uk/ws/files/17662538/jcs_final.pdf. See that section
+// for a formal and completely general description of this translation. This
+// comment gives a more intuitive description using a few examples at the
+// expense of losing some generality.
+//
+// As a minor wrinkle, this language also supports grouping assertions together
+// as in:
+//      Prin says { assertion_1, ..., assertion_n }
+// and these are simply "unrolled" to
+//      Prin says assertion_1.
+//      ...
+//      Prin says assertion_n.
+//
+//
+// ## Translation of assertions
+//
+// First, predicates with modifiers like "says", "canSay", and "actAs" are
+// converted into normal predicates by appending these modifiers to the
+// predicate name and moving the principals referenced by these predicates
+// into the arguments of the predicates. So for example
+//         A says B canSay foo(x, y)
+// becomes
+//         says_canSay_foo(A, B, x, y)
+// The rest of this comment ignores this part of the translation for the sake
+// of readability.
+//
+// Next we need to add a principal for the conditions in assertions. To prove
+// an assertion like
+//         "A says fact(x) :- fact1(x), fact2(x).
+// we need to show that *A believes* both fact1(x) and fact2(x). So we prepend
+// predicates on the RHS in "A says", producing the new assertion:
+//         A says fact(x) :- A says fact1(x), A says fact2(x)
+// (where says is actually prepended to the names of predicates and A becomes
+// an extra argument as above).
+//
+//  Next we need to translate delegations which should pass beliefs from one
+//  principal to another. For example, if we have
+//      A says B canSay fact(x) :- fact1(x)
+//  we do the usual translation resulting in
+//      (1) A says B canSay fact(x) :- A says fact1(x)
+//  but we also add the additional rule
+//      (2) A says fact(x) :- x says fact(x), A says x canSay fact(x)
+//  where x is a fresh variable.
+//  The result is that rule (1) gives the condition for delegation
+//  and rule (2) passes beliefs from B to A when the condition from (1) is met.
+//
+// Finally we need to translate canActAs which should pass properties from
+// one principal to another:
+// Assertions of either the form
+//      A says B canActAs C :- ...
+// or
+//      A says B <anyPredicate(...)> :-
+// are claims by A that B has a property (where canActAs is just a special
+// case). Syntactically these are both treated as "A says B <verbphrase>" with
+// different instances of <verbphrase>. Whenever some other principal can act
+// as B, we want to pass these properties from B to that other principal.
+// (For the special case where this property is B canActAs C, this essentially
+// makes canActAs transitive). In either case, we add an additional rule
+//    A says x verbphrase <- A says x canActAs B, A says B verbphrase
+// which will add "verbphrase" as a property of D whenever we can prove
+// the assertion "A says D canActAsB".
+//
+// ## Translation of Queries
+// Neither Souffle nor SecPal support queries, but this language does.
+// Queries check of a single unconditional assertion is true. A query of
+// the form:
+// ```Datalog
+//      Q_NAME = query ASSERTION(<ARGS>) ?
+// ```
+//
+// is translated into an assertion with just one argument, and this
+// assertion is made an output, so we can simply check the CSV that
+// souffle emits as in:
+// ```Datalog
+//      Q_NAME("dummy_var") :- grounded("dummy_var"), ASSERTION(<ARGS>).
+//      grounded("dummy_var").
+//      .output Q_NAME
+// ```
+
 class LoweringToDatalogPass {
  public:
   static DLIRProgram Lower(Program auth_logic_program) {
@@ -77,16 +163,16 @@ class LoweringToDatalogPass {
                     attribute.predicate());
   }
 
-  // This is the translation for the attribute case of a base fact.
-  // This returns two outputs as a pair:
+  // Translating an attribute results in two objects:
   // - A predicate, this is the main result of the translation
   // - An additional rule that allows attributes to be passed with canActAs
+  // This function is for generating the additional rule.
   // This takes both a speaker and the actual attribute as argument because
-  // the speaker is needed to generate the additional rule. Note all base
+  // the speaker is needed to generate the additional rule. Note that all base
   // facts have a speaker either explicitly or implicitly:
   // - If it appears on the LHS of an assertion, it explicitly has a speaker
   // - If it appears on the RHS of an assertion, it behaves semantically
-  // like has the same speaker as the head of the assertion.
+  // like it has the same speaker as the head of the assertion.
   DLIRAssertion SpokenAttributeToDLIR(Principal speaker,
                                       Attribute attribute) {
     Predicate main_predicate = AttributeToDLIR(attribute);
@@ -128,6 +214,11 @@ class LoweringToDatalogPass {
         can_act_as.right_principal().name()}, kPositive);
   }
 
+  // In the same way that attributes are passed around with "CanActAs", so
+  // are other "CanActAs" facts. To implement this, the translation of
+  // CanActAs also results in both a predicate and an extra rule that passes
+  // these facts around. This function is for generating the extra rule and
+  // it works similarly to "SpokenAttributeToDLIR".
   DLIRAssertion SpokenCanActAsToDLIR(Principal speaker,
                                   CanActAs can_act_as) {
     Predicate main_predicate = CanActAsToDLIR(can_act_as);