Prepare to replay XACML repository on top of this one

1 files changed, 493 insertions, 0 deletions

diff --git a/rego-proofs/paper/methodology.org b/rego-proofs/paper/methodology.org
new file mode 100644
index 0000000..25ef4f5
--- /dev/null
+++ b/rego-proofs/paper/methodology.org
@@ -0,0 +1,493 @@
+Rego documentation makes distinction between "complete" and "incremental" definitions.
+
+(Virtual) document = result of rule
+
+> Rules define the content of Virtual Documents in OPA. When OPA evaluates a rule, we say OPA generates the content of the document that is defined by the rule.
+
+* Lean
+** Types
+- Scalar values can be strings, numbers, booleans, or null
+- Composite values can be objects, _sets_, or arrays
+
+Sets aren't represented in =Lean.Data.Json=, so define our own types.
+
+#+BEGIN_SRC lean4
+inductive Scalar where
+  | null
+  | bool (b : Bool)
+  | num (n : Lean.JsonNumber)
+  | str (s : String)
+  deriving Inhabited
+
+inductive Composite where
+  | array (xs : Array Scalar)
+  -- TODO: Mathlib.Init.Set?
+  | set (isMember : Scalar → Bool)
+  | object (field : String → Scalar)
+  deriving Inhabited
+#+END_SRC
+
+References can be compiled to =field= invocations (?)
+Variables are mapped 1-to-1 to Lean names.
+*** Undefined is contagious
+> Expressions that refer to undefined values are also undefined. This includes comparisons such as !=.
+* Rego
+** Constructs That Need To Be Compiled
+*** Rules
+**** Assignment
+
+Need to support incremental definitions
+
+- rule-name IS value IF body
+- rule-name CONTAINS value IF body
+- rule-name.reference IS value IF body ("Generating Sets" and "Generating Objects")
+
+Ideas:
+
+- Some rules defining scalar values can be computed and defined as Lean variables.
+  - How do we deal with dependence on variables in the extensional database?
+- Rules defining set membership are
+  - A function for rules which aren't necessarily enumerable.
+    - =sets= in =mathlib4= are =α → Prop=
+  - A =finset= for rules which are.
+    - =finsets= in =mathlib4= are =(lists // permutation)= with no duplicated elements
+    - There's coe from finset to set, so they should be compatible in proof automation.
+- Rules defining scalars are functions, since they define what something /is/.
+  - That just /screams/ "computable."
+
+- I suppose we treat "computable" in the above as a special case.
+  - So everything is encoded in the simplest way possible, but if the source code provide enough information to determine the value of a =rule=, then we "optimize" it.
+
+- =IS= is a unary relation which can be defined inductively,
+- =CONTAINS= is also a unary relation which can be defined inductively,
+- =IS= for object members is a binary relation which can be defined inductively
+
+***** Default
+
+> When the default keyword is used, the rule syntax is restricted to:
+> 
+> default <name> := <term>
+> 
+> The term may be any scalar, composite, or comprehension value but it may not be a variable or reference. If the value is a composite then it may not contain variables or references. Comprehensions however may, as the result of a comprehension is never undefined.
+
+*** Expressions
+**** ITE
+
+#+BEGIN_SRC javascript
+{
+  "head": {
+    "name": "authorize",
+    "value": {
+      "type": "string",
+      "value": "allow"
+    },
+    "assign": true,
+    "ref": [
+      {
+        "type": "var",
+        "value": "authorize"
+      }
+    ]
+  },
+  "body": [
+    {
+      "index": 0,
+      "terms": [
+        {
+          "type": "ref",
+          "value": [
+            {
+              "type": "var",
+              "value": "equal"
+            }
+          ]
+        },
+        {
+          "type": "ref",
+          "value": [
+            {
+              "type": "var",
+              "value": "input"
+            },
+            {
+              "type": "string",
+              "value": "user"
+            }
+          ]
+        },
+        {
+          "type": "string",
+          "value": "superuser"
+        }
+      ]
+    }
+  ],
+  "else": {
+    "body": [
+      {
+        "index": 0,
+        "terms": [
+          {
+            "type": "ref",
+            "value": [
+              {
+                "type": "var",
+                "value": "equal"
+              }
+            ]
+          },
+          {
+            "type": "ref",
+            "value": [
+              {
+                "type": "var",
+                "value": "input"
+              },
+              {
+                "type": "string",
+                "value": "path"
+              },
+              {
+                "type": "number",
+                "value": 0
+              }
+            ]
+          },
+          {
+            "type": "string",
+            "value": "admin"
+          }
+        ]
+      },
+      {
+        "index": 1,
+        "terms": [
+          {
+            "type": "ref",
+            "value": [
+              {
+                "type": "var",
+                "value": "equal"
+              }
+            ]
+          },
+          {
+            "type": "ref",
+            "value": [
+              {
+                "type": "var",
+                "value": "input"
+              },
+              {
+                "type": "string",
+                "value": "source_network"
+              }
+            ]
+          },
+          {
+            "type": "string",
+            "value": "external"
+          }
+        ]
+      }
+    ],
+    "head": {
+      "name": "authorize",
+      "value": {
+        "type": "string",
+        "value": "deny"
+      },
+      "assign": true,
+      "ref": [
+        {
+          "type": "var",
+          "value": "authorize"
+        }
+      ]
+    }
+  }
+}
+#+END_SRC
+
+**** Comprehensions
+
+"Sets are defined by their membership predicate" is applicable here.
+
+**** References
+**** Variables
+Map 1-to-1 with Lean variables.
+**** Universal Quantification (FOR ALL)
+Map 1-to-1 with Lean forall (?)
+
+> Variables in Rego are existentially quantified by default: when you write
+
+array := ["one", "two", "three"]; array[i] == "three"
+
+> The query will be satisfied if there is an i such that the query’s expressions are simultaneously satisfied.
+
+**** Existential Quantification (SOME)
+Map 1-to-1 with Lean exists (?)
+**** With Keyword
+Map 1-to-1 with Lean let (?)
+**** Negation
+
+> For safety, a variable appearing in a negated expression must also appear in another non-negated equality expression in the rule.
+
+*** Unification (===)
+
+> Under the hood := and == are syntactic sugar for =, local variable creation, and additional compiler checks.
+
+*** General Purpose Functions
+*** Packages
+* Select examples
+#+BEGIN_SRC rego
+pi := 3.14159
+#+END_SRC
+
+#+BEGIN_SRC rego
+rect := {"width": 2, "height": 4}
+#+END_SRC
+
+#+BEGIN_SRC rego
+q contains name if {
+    some site in sites
+    name := site.name
+}
+#+END_SRC
+
+#+BEGIN_SRC rego
+t2 {
+    x := 42
+    y := 41
+    x > y
+}
+#+END_SRC
+
+#+BEGIN_SRC rego
+p if q["prod"]
+#+END_SRC
+
+#+BEGIN_SRC rego
+sites[0].servers[1].hostname
+#+END_SRC
+
+#+BEGIN_SRC rego
+apps_and_hostnames[[name, hostname]] {
+    some i, j, k
+    name := apps[i].name
+    server := apps[i].servers[_]
+    sites[j].servers[k].name == server
+    hostname := sites[j].servers[k].hostname
+}
+#+END_SRC
+
+(In particular, how do we encode the =some= if we're treating set membership as a function? Does it need to take a witness?)
+
+#+BEGIN_SRC rego
+fruit.apple.seeds = 12
+
+fruit.orange.color = "orange"
+#+END_SRC
+
+(How do we enforce that =fruit= should be the minimal object satisfying the partial rules above?)
+
+#+BEGIN_SRC rego
+# Find values for x and y that make the equality true
+[x, "world"] = ["hello", y]
+#+END_SRC
+
+** Queries
+
+#+BEGIN_SRC rego
+s[[1, x]]
+
++---+-----------+
+| x | s[[1, x]] |
++---+-----------+
+| 2 | [1,2]     |
+| 4 | [1,4]     |
++---+-----------+
+#+END_SRC
+
+(The table view, concretely, enumerates the possible values for free variables.)
+(A document is, I suppose, a special case of a table.)
+
+#+BEGIN_SRC rego
+package mytest
+
+import future.keywords.if
+import future.keywords.in
+
+s := {
+    [1, 2],
+    [1, 4],
+    [2, 2],
+    [2, 4]
+}
+
+y := true if {
+    ys := s[[1, x]]
+    count(ys) == 2
+} 
+#+END_SRC
+
+#+BEGIN_SRC lean4
+def s : set (list Lean.JsonNumber) :=
+  [[1, 2], [1, 4], [2, 2], [2, 4]]
+
+def y (x : Lean.JsonNumber) (s : set (list Lean.JsonNumber)) : Option bool :=
+  if [1, x] ∈ s then Some true else None
+#+END_SRC
+
+** Modeling Questions
+
+Everything as an inductive =RegoType=?
+
+This:
+
+#+BEGIN_SRC lean4
+def s : set (list Lean.JsonNumber) :=
+  [[1, 2], [1, 4], [2, 2], [2, 4]]
+
+def y (x : Lean.JsonNumber) (s : set (list Lean.JsonNumber)) : Option bool :=
+  if [1, x] ∈ s then Some true else None
+#+END_SRC
+
+Versus this:
+
+#+BEGIN_SRC lean4
+-- def s : RegoObject :=
+--   RegoObject.Set [(RegoObject.Array [1, 2]),
+--                   (RegoObject.Array [1, 4]),
+--                   (RegoObject.Array [2, 2]),
+--                   (RegoObject.Array [2, 4])]
+
+-- Assuming that coe can recurse...
+def s : RegoObject :=
+  [[1, 2], [1, 4], [2, 2], [2, 4]]
+
+def y (x : RegoObject) (s : RegoObject) : Option bool :=
+  match (x, s) with
+  | ((RegoObject.Num x'), (RegoObject.Set s')) :=
+    if [1, x'] ∈ s' then RegoObject.bool true else RegoObject.undefined
+  
+#+END_SRC
+
+*Answer*:
+
+We can't really define objects or other heterogeneous composite types without an =inductive=.
+
+Q: Set or Finset?
+
+A: Finset so we can actually define a =Boxed= inductive
+
+=Option RegoType= versus =RegoType.undefined=?
+
+* Compilation Procedure
+
+** Passes
+
+1. Parse (via =opa=)
+
+2. Group based on syntactic structure, rule name
+
+   #+BEGIN_SRC scheme
+   (define-record-type <policy>
+     (make-policy package imports rules comments)
+     policy?
+     (package  policy-package)
+     (imports  policy-imports)
+     (rules    policy-rules)
+     (comments policy-comments))
+   #+END_SRC
+
+3. ...
+
+4. Assign types to rules
+
+5. Emit 
+
+** TODO Constants
+:PROPERTIES:
+:CREATED:  2023-03-23 Thu 19:36
+:END:
+
+This:
+
+#+BEGIN_SRC js
+{"width": 2, "height": 4}
+#+END_SRC
+
+should be compiled into this:
+
+#+BEGIN_SRC lean4
+fun x => match x with
+| "width"  => some Rego.Boxed.Num 2
+| "height" => some Rego.Boxed.Num 4
+| _        => none
+end
+#+END_SRC
+
+** Assignment
+
+The following are equivalent:
+
+#+BEGIN_SRC rego
+pi := 3.14159
+#+END_SRC
+
+#+BEGIN_SRC rego
+pi := 3.14159 if {
+   true
+}
+#+END_SRC
+
+1. Attempt to identify type
+   1. Divergent types → =Rego.Any= 
+
+** Body
+
+1. Lift local variables
+2. Emit local variables as =let=
+* Upstream References
+- =ast/policy.go=
+
+* Lean IR
+
+- =predicate= (for inductive predicates, needs to encode the object in question)
+  - =kind= (what kind of object the predicate describes)
+  - =facts= (rules of inference for the predicate)
+
+- =computable-definition=
+  - =identifier=
+  - =type=
+  - =value=
+
+** Expressions
+
+- =exists=
+  - =variables= (list of identifier/type pairs)
+  - =body=
+- =conjunction= (=∧= of many expressions)
+- =compare=
+  - =kind= (===, =>=, =<=)
+- =funcall=
+  - =name=
+  - =args= (list of expressions)
+- =intro-local= (should be emitted with type)
+  - =identifier=
+  - =value=
+- =assignment-chain= (=do= notation with local assignments)
+  - Only really used for compiling references.
+- =option= (is this needed?)
+
+These can be represented as Scheme objects but need to be appropriately transformed in =emit=:
+
+- =boolean=
+- =string=
+- =number=
+
+* Not Lean IR
+
+- =scope=
+