Add JSON interface for Lean code (#160)

Co-authored-by: Andrew Wells <[email protected]>
Co-authored-by: Bhakti Shah <[email protected]>

Author: 3 people

cedar-lean/Cedar/Data/Map.lean

@@ -74,6 +74,12 @@ def findOrErr {α β ε} [BEq α] (m : Map α β) (k : α) (err: ε) : Except ε
   | some v => ok v
   | _      => error err
 
+/-- Returns the binding for `k` in `m`, or panics if none is found. -/
+def find! {α β} [Repr α] [BEq α] [Inhabited β] (m : Map α β) (k : α) : β :=
+  match m.find? k with
+  | some v => v
+  | _      => panic! s!"find!: key {repr k} not found"
+
 /-- Filters `m` using `f`. -/
 def filter {α β} (f : α → β → Bool) (m : Map α β) : Map α β :=
   Map.mk (m.kvs.filter (fun ⟨k, v⟩ => f k v))

cedar-lean/Cedar/Spec/Expr.lean

@@ -66,12 +66,11 @@ inductive Expr where
 
 ----- Derivations -----
 
-deriving instance Repr, DecidableEq for Var
-deriving instance Repr, DecidableEq for UnaryOp
-deriving instance Repr, DecidableEq for BinaryOp
+deriving instance Repr, DecidableEq, Inhabited for Var
+deriving instance Repr, DecidableEq, Inhabited for UnaryOp
+deriving instance Repr, DecidableEq, Inhabited for BinaryOp
 deriving instance Repr, Inhabited for Expr
 
-
 mutual
 
 -- We should be able to get rid of this manual deriviation eventually.

cedar-lean/Cedar/Spec/Ext.lean

@@ -39,7 +39,7 @@ def Ext.lt : Ext → Ext → Bool
 
 ----- Derivations -----
 
-deriving instance Repr, DecidableEq for Ext
+deriving instance Repr, DecidableEq, Inhabited for Ext
 
 instance : LT Ext where
 lt := fun x y => Ext.lt x y

cedar-lean/Cedar/Spec/Ext/Decimal.lean

@@ -77,6 +77,9 @@ if h : Decimal.lt d₁ d₂ then isTrue h else isFalse h
 instance decLe (d₁ d₂ : Decimal) : Decidable (d₁ ≤ d₂) :=
 if h : Decimal.le d₁ d₂ then isTrue h else isFalse h
 
+instance : Inhabited Decimal where
+  default := Subtype.mk 0 (by simp)
+
 end Decimal
 
-end Cedar.Spec.Ext
+end Cedar.Spec.Ext

cedar-lean/Cedar/Spec/ExtFun.lean

@@ -64,6 +64,6 @@ def call : ExtFun → List Value → Result Value
 
 ----- Derivations -----
 
-deriving instance Repr, DecidableEq for ExtFun
+deriving instance Repr, DecidableEq, Inhabited for ExtFun
 
 end Cedar.Spec

cedar-lean/Cedar/Spec/Value.lean

@@ -131,12 +131,11 @@ instance : Coe Value (Result (Data.Set Value)) where
 
 deriving instance Repr, DecidableEq, BEq for Except
 deriving instance Repr, DecidableEq for Error
-deriving instance Repr, DecidableEq, Inhabited for Name
+deriving instance Repr, DecidableEq, Inhabited, Lean.ToJson for Name
 deriving instance Repr, DecidableEq, Inhabited for EntityType
 deriving instance Repr, DecidableEq, Inhabited for EntityUID
 deriving instance Repr, DecidableEq, Inhabited for Prim
-deriving instance Repr for Value
-
+deriving instance Repr, Inhabited for Value
 
 mutual
 
@@ -302,6 +301,4 @@ instance : LT Value where
 instance Value.decLt (n m : Value) : Decidable (n < m) :=
 if h : Value.lt n m then isTrue h else isFalse h
 
-deriving instance Inhabited for Value
-
 end Cedar.Spec

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -287,4 +287,9 @@ def typeOf (x : Expr) (c : Capabilities) (env : Environment) : ResultType :=
     let tys ← xs.mapM₁ (λ ⟨x₁, _⟩ => justType (typeOf x₁ c env))
     typeOfCall xfn tys xs
 
+---- Derivations -----
+
+deriving instance Repr for RequestType
+deriving instance Repr for Environment
+
 end Cedar.Validation

cedar-lean/Cedar/Validation/Types.lean

@@ -110,8 +110,13 @@ def ActionStore.descendentOf (as : ActionStore)  (uid₁ uid₂ : EntityUID) : B
 
 ----- Derivations -----
 
-deriving instance DecidableEq for BoolType
-deriving instance DecidableEq for ExtType
+deriving instance Repr, DecidableEq for BoolType
+deriving instance Repr, DecidableEq, Inhabited for ExtType
+deriving instance Repr, DecidableEq, Inhabited for Qualified
+deriving instance Repr, Inhabited for CedarType
+deriving instance Repr for TypeError
+deriving instance Repr for EntityTypeStoreEntry
+deriving instance Repr for ActionStoreEntry
 
 mutual
 
@@ -184,9 +189,6 @@ end
 
 instance : DecidableEq CedarType := decCedarType
 
-deriving instance DecidableEq for Qualified
 deriving instance DecidableEq for TypeError
 
-deriving instance Inhabited for CedarType
-
 end Cedar.Validation

cedar-lean/Cedar/Validation/Validator.lean

@@ -143,4 +143,32 @@ def validate (policies : Policies) (schema : Schema) : ValidationResult :=
   let envs := schema.toEnvironments
   policies.forM (typecheckPolicyWithEnvironments · envs)
 
+----- Derivations -----
+
+deriving instance Repr for SchemaActionEntry
+deriving instance Repr for Schema
+deriving instance Repr for ValidationError
+
+/-
+Lossy serialization of errors to Json. This serialization provides some extra
+information to DRT without having to derive `Lean.ToJson` for `Expr` and `CedarType`.
+-/
+def validationErrorToJson : ValidationError → Lean.Json
+  | .typeError _ (.lubErr _ _) => "lubErr"
+  | .typeError _ (.unexpectedType _) => "unexpectedType"
+  | .typeError _ (.attrNotFound _ _) => "attrNotFound"
+  | .typeError _ (.unknownEntity _) => "unknownEntity"
+  | .typeError _ (.extensionErr _) => "extensionErr"
+  | .typeError _ .emptySetErr => "emptySetErr"
+  | .typeError _ (.incompatibleSetTypes _) => "incompatibleSetTypes"
+  | .impossiblePolicy _ => "impossiblePolicy"
+
+instance : Lean.ToJson ValidationError where
+  toJson := validationErrorToJson
+
+-- Used to serialize `ValidationResult`
+deriving instance Lean.ToJson for Except
+instance : Lean.ToJson Unit where
+  toJson := λ _ => Lean.Json.null
+
 end Cedar.Validation

cedar-lean/Cli/Main.lean

@@ -0,0 +1,47 @@
+/-
+ Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Lean.Data.Json.FromToJson
+
+import DiffTest.Main
+import DiffTest.Parser
+
+/-! This file provides a basic command line interface for authorization
+    and validation. It uses the interface functions defined in `Difftest`. -/
+
+open DiffTest
+
+def readFile (filename : String) : IO String :=
+  IO.FS.readFile filename
+
+def printUsage (err : String) : IO Unit :=
+  IO.println s!"{err}\nUsage: Cli <command> <file>"
+
+def main (args : List String) : IO Unit :=
+  match args.length with
+    | 2 => do
+      let command := args.get! 0
+      let filename := args.get! 1
+      let request ← readFile filename
+      match command with
+      | "authorize" =>
+        let response := isAuthorizedDRT request
+        IO.println response
+      | "validate" =>
+        let response := validateDRT request
+        IO.println response
+      | _ => printUsage s!"Invalid command `{command}` (expected `authorize` or `validate`)"
+    | n => printUsage s!"Incorrect number of arguments (expected 2, but got {n})"