Rego compiler: initial commit

9 files changed, 242 insertions, 0 deletions

diff --git a/rego-proofs/compiler-rewrite/.gitignore b/rego-proofs/compiler-rewrite/.gitignore
new file mode 100644
index 0000000..e35d885
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/.gitignore
@@ -0,0 +1 @@
+_build
diff --git a/rego-proofs/compiler-rewrite/bin/dune b/rego-proofs/compiler-rewrite/bin/dune
new file mode 100644
index 0000000..5dd24b4
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/bin/dune
@@ -0,0 +1,10 @@
+(executable
+ (public_name compiler_rewrite)
+ (name main)
+ (libraries core compiler_rewrite unix yojson)
+ (preprocess
+   (pps ppx_deriving.show)))
+
+(env
+  (dev
+    (flags (:standard -w -66 -w -37 -w -30 -w -32))))
diff --git a/rego-proofs/compiler-rewrite/bin/main.ml b/rego-proofs/compiler-rewrite/bin/main.ml
new file mode 100644
index 0000000..1bb28c1
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/bin/main.ml
@@ -0,0 +1,198 @@
+open Core
+open Yojson.Basic.Util
+
+let invoke ?(stdin="") ?(env=[| |]) cmd =
+  let ic, oc, ec = UnixLabels.open_process_full cmd ~env:env in
+  Out_channel.output_string oc stdin ;
+  Out_channel.close oc;
+  (In_channel.input_all ic,
+   In_channel.input_all ec)
+
+type scalar = String of string
+            | Number of float
+            | Bool of bool
+            | Null
+[@@deriving show]
+and ref_target = Var of string
+                | Array of term list
+                | Object of (object_item * object_item)
+                | Set of term list
+                | ArrayComprehension of term * query
+                | ObjectComprehension of object_item * query
+                | SetComprehension of term * query
+                | Call of (string list) * (expr list)
+[@@deriving show]
+and ref_arg = Scalar of scalar
+             | Var of string
+             | Array of term list
+             | Object of (object_item * object_item)
+             | Set of term list
+             | Ignore
+[@@deriving show]
+and object_item = Scalar of scalar | Ref of ref_target * (ref_arg list) | Var
+[@@deriving show]
+and ref_item = Var of string
+              | Array of term list
+              | Object of (object_item * object_item) list
+              | Set of term list
+              | ArrayComprehension of term * query
+              | ObjectComprehension of object_item * query
+              | SetComprehension of term * query
+              | Call of (string list) * (expr list)
+[@@deriving show]
+and term = Ref of ref_target * (ref_arg list)
+          | Var of string
+          | Scalar of scalar
+          | Array of term list
+          | Object of (object_item * object_item) list
+          | Set of term list
+          | Membership of (term list) * term
+          | ArrayComprehension of term * query
+          | ObjectComprehension of object_item * query
+          | SetComprehension of term * query
+[@@deriving show]
+and infix_operator = BoolEq
+                   | BoolNot
+                   | BoolLt
+                   | BoolGt
+                   | BoolGeq
+                   | BoolLeq
+                   | ArithAdd
+                   | ArithSub
+                   | ArithMul
+                   | ArithDiv
+                   | BinAnd
+                   | BinOr
+                   | Assign
+                   | Unify
+[@@deriving show]
+and every_item = Term of term
+               | Call of (string list) * (expr list)
+               | Infix of expr * infix_operator * expr
+[@@deriving show]
+and expr = Term of term
+         | Call of (string list) * (expr list)
+         | Infix of expr * infix_operator * expr
+         | Every of (string list) * every_item * query
+         | Unary of expr (* Has to be unary negation *)
+[@@deriving show]
+and literal_head = Some of (term list) * expr
+            | Expr of expr
+            | Negate of expr
+[@@deriving show]
+and literal = literal_head * ((term * term) option) (* "with" modifier *)
+[@@deriving show]
+and query = literal list
+[@@deriving show]
+
+type assign_operator = Assign | Unify
+[@@deriving show]
+
+type rule_head_lhs = ref_target * (ref_arg list)
+[@@deriving show]
+type rule_head_rhs = Assignment of assign_operator * term
+                   | Object of term * assign_operator * term
+                   | Function of (term list) * assign_operator * term
+                   | Set of term
+[@@deriving show]
+type rule_head = rule_head_lhs * rule_head_rhs
+[@@deriving show]
+
+type rule_body = Query of query | Literal of literal
+[@@deriving show]
+
+type rule =
+  { default : bool;
+    head : rule_head;
+    body: rule_body list;
+    otherwise : rule option;
+  }
+[@@deriving show]
+
+type import =
+  { alias : string option;
+    path : ref_target * (ref_arg list);
+  }
+[@@deriving show]
+
+type package =
+  { path : ref_target * (ref_arg list);
+    imports: import list;
+    policy : rule list;
+  }
+[@@deriving show]
+
+let to_bool_or_false : Yojson.Basic.t -> bool = function
+  | `Bool b -> b
+  | _ -> false
+
+let to_list_or_empty : Yojson.Basic.t -> Yojson.Basic.t list = function
+  | `Null -> []
+  | `List xs -> xs
+  | _ -> failwith "Not a list or null"
+
+let parse_ref_target tree : ref_target =
+  match (tree |> member "type" |> to_string) with
+  | "var" -> Var (tree |> member "value" |> to_string)
+  | _ -> failwith "unimplemented"
+
+let parse_ref_arg tree =
+  match (tree |> member "type" |> to_string) with
+  | "string" -> Scalar (String (tree |> member "value" |> to_string))
+  | _ -> failwith "unimplemented"
+
+let parse_ref tree =
+  match tree with
+  | target :: args -> (parse_ref_target target, List.map ~f:parse_ref_arg args)
+  | _ -> failwith "empty reference"
+
+let parse_import_path tree =
+  match (tree |> member "type" |> to_string) with
+  | "ref" -> tree |> member "value" |> to_list |> parse_ref
+  | _ -> failwith "unimplemented"
+
+let parse_import tree =
+  { alias = tree |> member "alias" |> to_string_option;
+    path = tree |> member "path" |> parse_import_path
+  }
+
+let parse_term (tree : Yojson.Basic.t) : term =
+  match tree |> member "type" |> to_string with
+  | "boolean" -> Scalar (Bool (tree |> member "value" |> to_bool))
+  | "number" -> Scalar (Number (tree |> member "value" |> to_number))
+  | _ -> failwith "unimplemented"
+
+let parse_head tree =
+  (* Variables are desugared to empty references. *)
+  let lhs = tree |> member "ref" |> to_list |> parse_ref in
+  let rhs =
+    if tree |> member "assign" |> to_bool_or_false then
+      Assignment (Assign, (tree |> member "value" |> parse_term))
+    else
+      failwith "unimplemented"
+  in (lhs, rhs)
+
+let parse_body tree =
+  Literal (Expr (Term (tree |> member "terms" |> parse_term)), None)
+
+let parse_rule tree =
+  { default = tree |> member "default" |> to_bool_or_false;
+    head = tree |> member "head" |> parse_head;
+    body = List.map ~f:parse_body (tree |> member "body" |> to_list_or_empty);
+    otherwise = None;
+  }
+
+let parse_package tree =
+  tree |> member "path" |> to_list |> parse_ref
+
+let parse_tree tree =
+  { path = tree |> member "package" |> parse_package;
+    imports = List.map ~f:parse_import (tree |> member "imports" |> to_list_or_empty);
+    policy = List.map ~f:parse_rule (tree |> member "rules" |> to_list_or_empty)
+  }
+
+let () =
+  let file_name = Array.get (Sys.get_argv ()) 1 in
+  let policy_code = In_channel.read_all file_name in
+  let (stdout, _) = invoke ("/home/jakob/.local/bin/opa parse -f json /dev/stdin") ~stdin:policy_code ~env:[| |] in
+  Yojson.Basic.from_string stdout |> parse_tree |> show_package |> print_endline
diff --git a/rego-proofs/compiler-rewrite/compiler_rewrite.opam b/rego-proofs/compiler-rewrite/compiler_rewrite.opam
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/compiler_rewrite.opam
diff --git a/rego-proofs/compiler-rewrite/dune-project b/rego-proofs/compiler-rewrite/dune-project
new file mode 100644
index 0000000..365d9da
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.11)
+
+(name compiler_rewrite)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name compiler_rewrite)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune)
+ (tags
+  (topics "to describe" your project)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
diff --git a/rego-proofs/compiler-rewrite/lib/dune b/rego-proofs/compiler-rewrite/lib/dune
new file mode 100644
index 0000000..b97e695
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/lib/dune
@@ -0,0 +1,2 @@
+(library
+ (name compiler_rewrite))
diff --git a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
diff --git a/rego-proofs/compiler-rewrite/test/dune b/rego-proofs/compiler-rewrite/test/dune
new file mode 100644
index 0000000..d6ad7d2
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/test/dune
@@ -0,0 +1,2 @@
+(test
+ (name compiler_rewrite))
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index f904da7..a210c47 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -924,3 +924,6 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
 
 def Choice : Type := List (Decision × ResultAuxiliary)
 deriving BEq, Repr
+
+def 2asdf := 2
+#check 1-2