diff --git a/Plausible.lean b/Plausible.lean index a6814f32..fee4e8df 100644 --- a/Plausible.lean +++ b/Plausible.lean @@ -39,8 +39,3 @@ import Plausible.Chamelean.MExp -- https://github.com/leanprover-community/plausible/pull/35 import Plausible.DeriveArbitrary import Plausible.Arbitrary - --- Chamelean examples -import Plausible.Chamelean.Examples.ExampleInductiveRelations -import Plausible.Chamelean.Examples.STLC -import Plausible.Chamelean.Examples.Trees diff --git a/Plausible/Arbitrary.lean b/Plausible/Arbitrary.lean index 8f2e4498..445c6eb9 100644 --- a/Plausible/Arbitrary.lean +++ b/Plausible/Arbitrary.lean @@ -71,6 +71,15 @@ instance [SampleableExt α] : Arbitrary α where instance [Arbitrary α] : Arbitrary (Option α) where arbitrary := pure <$> Arbitrary.arbitrary +/-- Every `Arbitrary α` instance gives rise to an `Arbitrary (List α)` instance -/ +instance [Arbitrary α] : Arbitrary (List α) where + arbitrary := listOf Arbitrary.arbitrary + +/-- If we have `Arbitrary` instances for `α` and `β`, + cthen we get an `Arbitrary (α × β)` instance -/ +instance [Arbitrary α] [Arbitrary β] : Arbitrary (α × β) where + arbitrary := Prod.mk <$> Arbitrary.arbitrary <*> Arbitrary.arbitrary + namespace Arbitrary /-- Samples from the generator associated with the `Arbitrary` instance for a type, diff --git a/README.md b/README.md index 7e3b8579..1c9b9254 100644 --- a/README.md +++ b/README.md @@ -127,17 +127,15 @@ We provide a command elaborator which elaborates the `#derive_checker` command: - Run `lake test` to check that the derived generators in [`Test`](./Test/) typecheck, and that the code for the derived generators match the expected output. - See [`DeriveBSTGenerator.lean`](./Test/DeriveArbitrarySuchThat/DeriveBSTGenerator.lean) & [`DeriveBalancedTreeGenerator.lean`](./Test/DeriveArbitrarySuchThat/DeriveBalancedTreeGenerator.lean) for examples of snapshot tests. Follow the template in these two files to add new snapshot test file, and remember to import the new test file in [`Test.lean`](./Test.lean) afterwards. -**Common Definitions**: -- [`BinaryTree.lean`](./Test/CommonDefinitions/BinaryTree.lean): Binary tree datatype with `BST` (Binary Search Tree) and `Between` relations -- [`FunctionCallInConclusion.lean`](./Test/CommonDefinitions/FunctionCallInConclusion.lean): Example inductive relation with function calls in constructor conclusions -- [`ListRelations.lean`](./Test/CommonDefinitions/ListRelations.lean): Various inductive relations over lists, some of which require pattern-matching on multiple inputs -- [`Permutation.lean`](./Test/CommonDefinitions/Permutation.lean): Inductive relation for list permutations -- [`STLCDefinitions.lean`](./Test/CommonDefinitions/STLCDefinitions.lean): Simply-Typed Lambda Calculus (STLC) definitions including types, terms, typing judgments, and lookup relations - **Key Value Store Example**: - [`KeyValueStore.lean`](./Test/KeyValueStoreExample/KeyValueStore.lean): Definitions for a hypothetical key-value store, in which inductive types are used to encode API calls and K/V states, and inductive relations are used to define API call semantics - [`TestKeyValueStoreCheckerGenerators.lean`](./Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean): The derived checkers & generators for the K/V store example (in particular, the derived generator produces well-formed sequences of API calls) +**Cedar Example**: +- [`Cedar.lean`](./Test/CedarExample/Cedar.lean): Lean formalization of a subset of the [Cedar policy language (OOPSLA '24)](https://dl.acm.org/doi/10.1145/3649835), adapted from Mike Hicks's Coq formalization +- [`CedarCheckerGenerators.lean`](./Test/CedarExample/CedarCheckerGenerators.lean): Snapshot tests for derived checkers & generators for Cedar terms / types / schemas +- [`CedarWellTypedTermGenerator.lean`](./Test/CedarExample/CedarWellTypedTermGenerator.lean): Example generator for well-typed Cedar expressions + **Tests for Unconstrained Generators (`#derive_arbitrary`)**: - [`BitVecStructureTest.lean`](./Test/DeriveArbitrary/BitVecStructureTest.lean): Tests for structures with dependently-typed `BitVec` arguments - [`DeriveNKIBinopGenerator.lean`](./Test/DeriveArbitrary/DeriveNKIBinopGenerator.lean): Derived generator for NKI binary operators (logical, comparison, arithmetic, bitwise) @@ -193,6 +191,13 @@ We provide a command elaborator which elaborates the `#derive_checker` command: **Enumerator Infrastructure Tests**: - [`EnumInstancesTest.lean`](./Test/Enum/EnumInstancesTest.lean): Tests for basic enumerator instances on Nat, Bool, pairs, sums, lists, etc. -**Plausible Tests**: +**Auxiliary definitions for snapshot tests**: +- [`BinaryTree.lean`](./Test/CommonDefinitions/BinaryTree.lean): Binary tree datatype with `BST` (Binary Search Tree) and `Between` relations +- [`FunctionCallInConclusion.lean`](./Test/CommonDefinitions/FunctionCallInConclusion.lean): Example inductive relation with function calls in constructor conclusions +- [`ListRelations.lean`](./Test/CommonDefinitions/ListRelations.lean): Various inductive relations over lists, some of which require pattern-matching on multiple inputs +- [`Permutation.lean`](./Test/CommonDefinitions/Permutation.lean): Inductive relation for list permutations +- [`STLCDefinitions.lean`](./Test/CommonDefinitions/STLCDefinitions.lean): Simply-Typed Lambda Calculus (STLC) definitions including types, terms, typing judgments, and lookup relations + +**Plausible Tests** (inherited from the original Plausible repo): - [`Tactic.lean`](./Test/Tactic.lean): Tests the `plausible` tactic on core Lean types - [`Testable.lean`](./Test/Testable.lean): Tests for the `Testable` typeclass infrastructure with custom types \ No newline at end of file diff --git a/Test.lean b/Test.lean index 0eff91ca..9b1e478d 100644 --- a/Test.lean +++ b/Test.lean @@ -71,3 +71,8 @@ import Test.DeriveEnumSuchThat.DerivePermutationEnumerator -- Key Value Store Example import Test.KeyValueStoreExample.KeyValueStore import Test.KeyValueStoreExample.TestKeyValueStoreCheckerGenerators + +-- Cedar Example +import Test.CedarExample.Cedar +import Test.CedarExample.CedarCheckerGenerators +import Test.CedarExample.CedarWellTypedTermGenerator diff --git a/Test/CedarExample/Cedar.lean b/Test/CedarExample/Cedar.lean new file mode 100644 index 00000000..14db9b1b --- /dev/null +++ b/Test/CedarExample/Cedar.lean @@ -0,0 +1,950 @@ +-- Import linter from batteries to suppress "missing documentation" linter warnings +import Batteries.Tactic.Lint + +import Plausible.Arbitrary +import Plausible.DeriveArbitrary +import Plausible.Chamelean.GeneratorCombinators +import Plausible.Chamelean.ArbitrarySizedSuchThat +import Plausible.Chamelean.DeriveChecker +import Plausible.Chamelean.DeriveConstrainedProducer + +open Plausible + +/-! +This file contains a Lean formalization of the Cedar policy language (OOPSLA '24), +adapted from Mike Hicks's Coq formalization (not publicly available). +-/ + +------------------------------------ +-- Part One: Cedar expression syntax +------------------------------------- + +/-- The name of an entity -/ +inductive EntityName where +| MkName : String → List String → EntityName +deriving Repr, BEq, DecidableEq + +/-- Entity UIDs -/ +inductive EntityUID where +| MkEntityUID : EntityName → String → EntityUID +deriving Repr, BEq, DecidableEq + +/-- Primitive values -/ +inductive Prim where +| boolean (b : Bool) +| int (i : Int) +| stringLit (s : String) +| entityUID (e : EntityUID) +deriving Repr, BEq, DecidableEq + +/-- Variables -/ +inductive Var where +| principal +| action +| resource +| context +deriving Repr, BEq, DecidableEq + +/-- Pattern elements -/ +inductive PatElem where +| star +| justLit (s : String) +deriving Repr, BEq, DecidableEq + +/-- Unary operations -/ +inductive UnaryOp where +| not +| neg +| like (p : List PatElem) +| is (ety : EntityName) +deriving Repr, BEq, DecidableEq + +/-- Binary operations -/ +inductive BinaryOp where +| equals +| mem +| less +| lessEq +| add +| sub +| mul +| contains +| containsAll +| containsAny +deriving Repr, BEq, DecidableEq + +/-- Cedar expressions. Note: + - We call this datatype `CedarExpr` to avoid naming conflicts with Lean's `Expr` datatype + - We "inline" list constructors for sets and records to avoid issue with mutual recursion in a list/generic type -/ +inductive CedarExpr where +| lit (p : Prim) +| var (v : Var) +| ite (cond : CedarExpr) (thenExpr : CedarExpr) (elseExpr : CedarExpr) +| andExpr (a : CedarExpr) (b : CedarExpr) +| orExpr (a : CedarExpr) (b : CedarExpr) +| unaryApp (op : UnaryOp) (expr : CedarExpr) +| binaryApp (op : BinaryOp) (a : CedarExpr) (b : CedarExpr) +| getAttr (expr : CedarExpr) (attr : String) +| hasAttr (expr : CedarExpr) (attr : String) +| setExprNil +| setExprCons (e : CedarExpr) (ls : CedarExpr) +| recExprNil +| recExprCons (s : String) (e : CedarExpr) (attrs : CedarExpr) +deriving BEq, DecidableEq + +/-- Type of entity data. + Precondition: the `Expr` argument should always be a record of values -/ +inductive EntityData where +| MkEntityData : CedarExpr → List EntityUID → EntityData +deriving BEq, DecidableEq + +/-- given `MkReq P A R C`, assumes that `RecordExpr C` and `Value C` hold --/ +inductive Request where +| MkReq : EntityUID → EntityUID → EntityUID → CedarExpr → Request +deriving BEq, DecidableEq + +------------------------------------------------- +-- Part Two: Pretty Printing Cedar Expressions +------------------------------------------------- + +/-- Converts the arguments to an `EntityName` to a String -/ +def stringOfEntityName (ps : List String) (t : String) : String := + match ps with + | [] => t + | p::ps' => p ++ "::" ++ stringOfEntityName ps' t + +instance : ToString EntityName where + toString := fun b => + match b with + | .MkName t p => stringOfEntityName p t + +/-- Converts an Entity UID to a string -/ +def stringOfEntityUID (ps : List String) (t : String) (id : String) : String := + stringOfEntityName ps t ++ "::\"" ++ id ++ "\"" + +instance : ToString EntityUID where + toString := fun b => + match b with + | EntityUID.MkEntityUID (.MkName t p) id => stringOfEntityUID p t id + +/-- Converts a primitive to a string -/ +def stringOfPrim (p : Prim) : String := + match p with + | Prim.boolean b => toString b + | Prim.int i => toString i + | Prim.stringLit s => toString s + | Prim.entityUID e => toString e + +instance : ToString Prim where + toString := stringOfPrim + +instance : ToString Var where + toString := fun v => match v with + | Var.principal => "principal" + | Var.action => "action" + | Var.resource => "resource" + | Var.context => "context" + +/-- Converts a `PatElem` to a string -/ +def stringOfPatElem (p : PatElem) : String := + match p with + | PatElem.star => "*" + | PatElem.justLit s => s + +/-- Converts a List of `PatElem`s to `String`s -/ +def stringOfPats (p : List PatElem) : String := + match p with + | [] => "" + | p0::ps => stringOfPatElem p0 ++ stringOfPats ps + +/-- Converts an `Expr` to a string -/ +def stringOfExpr (e : CedarExpr) : String := + match e with + | CedarExpr.lit p => toString p + | CedarExpr.var v => toString v + | CedarExpr.ite cond thenExpr elseExpr => + "if (" ++ stringOfExpr cond ++ ") then (" ++ stringOfExpr thenExpr ++ ") else (" ++ stringOfExpr elseExpr ++ ")" + | CedarExpr.andExpr a b => "(" ++ stringOfExpr a ++ ") && (" ++ stringOfExpr b ++ ")" + | CedarExpr.orExpr a b => "(" ++ stringOfExpr a ++ ") || (" ++ stringOfExpr b ++ ")" + | CedarExpr.unaryApp op expr => + match op with + | UnaryOp.not => "not (" ++ stringOfExpr expr ++ ")" + | UnaryOp.neg => "- (" ++ stringOfExpr expr ++ ")" + | UnaryOp.like ps => "(" ++ stringOfExpr expr ++ ") like \"" ++ stringOfPats ps ++ "\"" + | UnaryOp.is e => "is (" ++ toString e ++ ")" + | CedarExpr.binaryApp op a b => + let sa := "(" ++ stringOfExpr a ++ ")" + let sb := "(" ++ stringOfExpr b ++ ")" + match op with + | BinaryOp.equals => sa ++ "==" ++ sb + | BinaryOp.mem => sa ++ "in" ++ sb + | BinaryOp.less => sa ++ "<" ++ sb + | BinaryOp.lessEq => sa ++ "<=" ++ sb + | BinaryOp.add => sa ++ "+" ++ sb + | BinaryOp.sub => sa ++ "-" ++ sb + | BinaryOp.mul => sa ++ "*" ++ sb + | BinaryOp.contains => sa ++ ".contains" ++ sb + | BinaryOp.containsAll => sa ++ ".containsAll" ++ sb + | BinaryOp.containsAny => sa ++ ".containsAny" ++ sb + | CedarExpr.getAttr expr attr => "(" ++ stringOfExpr expr ++ ")." ++ attr + | CedarExpr.hasAttr expr attr => "(" ++ stringOfExpr expr ++ ") has " ++ attr + | CedarExpr.setExprNil => "nil" + | CedarExpr.setExprCons e ls => "(" ++ stringOfExpr e ++ ")::" ++ stringOfExpr ls + | CedarExpr.recExprNil => "{}" + | CedarExpr.recExprCons s e attrs => "{ " ++ s ++ ": " ++ stringOfExpr e ++ " }" ++ stringOfExpr attrs + +instance : ToString CedarExpr where + toString := stringOfExpr + +instance : Repr CedarExpr where + reprPrec e _ := toString e + +instance : ToString Request where + toString := fun r => match r with + | Request.MkReq p a res c => + "MkReq " ++ toString p ++ " " ++ toString a ++ " " ++ toString res ++ " " ++ toString c + +/-- Computes the `depth` of an expression, useful during generation -/ +def depthExpr (e : CedarExpr) : Nat := + match e with + | CedarExpr.lit _ => 1 + | CedarExpr.var _ => 1 + | CedarExpr.ite cond thenExpr elseExpr => + 1 + max (max (depthExpr cond) (depthExpr thenExpr)) (depthExpr elseExpr) + | CedarExpr.andExpr a b => 1 + max (depthExpr a) (depthExpr b) + | CedarExpr.orExpr a b => 1 + max (depthExpr a) (depthExpr b) + | CedarExpr.unaryApp _op expr => 1 + depthExpr expr + | CedarExpr.binaryApp _op a b => 1 + max (depthExpr a) (depthExpr b) + | CedarExpr.getAttr expr _attr => 1 + depthExpr expr + | CedarExpr.hasAttr expr _attr => 1 + depthExpr expr + | CedarExpr.setExprNil => 1 + | CedarExpr.setExprCons e ls => 1 + max (depthExpr e) (depthExpr ls) + | CedarExpr.recExprNil => 1 + | CedarExpr.recExprCons _s e attrs => 1 + max (depthExpr e) (depthExpr attrs) + +/-- Computes the `size` of an expression, useful during generation -/ +def sizeExpr (e : CedarExpr) : Nat := + match e with + | CedarExpr.lit _ => 1 + | CedarExpr.var _ => 1 + | CedarExpr.ite cond thenExpr elseExpr => + 1 + sizeExpr cond + sizeExpr thenExpr + sizeExpr elseExpr + | CedarExpr.andExpr a b => 1 + sizeExpr a + sizeExpr b + | CedarExpr.orExpr a b => 1 + sizeExpr a + sizeExpr b + | CedarExpr.unaryApp _ expr => 1 + sizeExpr expr + | CedarExpr.binaryApp _ a b => 1 + sizeExpr a + sizeExpr b + | CedarExpr.getAttr expr _ => 1 + sizeExpr expr + | CedarExpr.hasAttr expr _ => 1 + sizeExpr expr + | CedarExpr.setExprNil => 1 + | CedarExpr.setExprCons e ls => 1 + sizeExpr e + sizeExpr ls + | CedarExpr.recExprNil => 1 + | CedarExpr.recExprCons _ e attrs => 1 + sizeExpr e + sizeExpr attrs + + +--------------------------------------- +-- Part Three: Cedar expression typing +--------------------------------------- +-- Some basic predicates useful for typing + +/-- predicate: When an expression is a record -/ +inductive RecordExpr : CedarExpr → Prop where +| RENil : RecordExpr CedarExpr.recExprNil +| RECons : ∀ fn e r, RecordExpr (CedarExpr.recExprCons fn e r) + +/-- predicate: When an expression is a set -/ +inductive SetExpr : CedarExpr → Prop where +| SENil : SetExpr CedarExpr.setExprNil +| SECons : ∀ e r, SetExpr (CedarExpr.setExprCons e r) + +/-- predicate: When an expression is a value -/ +inductive Value : CedarExpr → Prop where +| VLit : ∀ p, Value (CedarExpr.lit p) +| VSNil : Value CedarExpr.setExprNil +| VSCons : ∀ e ls, Value e → Value ls → Value (CedarExpr.setExprCons e ls) +| VRNil : Value CedarExpr.recExprNil +| VRCons : ∀ s e rs, Value e → Value rs → Value (CedarExpr.recExprCons s e rs) + +/-- predicate: When an expression is a set of entity values -/ +inductive SetEntityValues : CedarExpr → Prop where +| SEVNil : SetEntityValues CedarExpr.setExprNil +| SEVCons : ∀ uid r, + SetEntityValues r → + SetEntityValues (CedarExpr.setExprCons (CedarExpr.lit (Prim.entityUID uid)) r) + +------------------------------------------------------ +-- Types +------------------------------------------------------ + +/-- Boolean types -/ +inductive BoolType where +| anyBool +| tt +| ff +deriving Repr, BEq, DecidableEq + +/-- Types in Cedar -/ +inductive CedarType where +| boolType (bty : BoolType) +| intType +| stringType +| entityType (ety : EntityName) +| setType (ty : CedarType) +| recordTypeNil +| recordTypeCons (s : String) (opt : Bool) (ty : CedarType) (rest : CedarType) +deriving BEq, DecidableEq + +/-- Determines whether a `CedarType` is a `RecordType` -/ +inductive RecordType : CedarType → Prop where +| RTNil : RecordType CedarType.recordTypeNil +| RTCons : ∀ fn o T1 T2, RecordType (CedarType.recordTypeCons fn o T1 T2) + +@[nolint docBlame] +inductive DefinedName : List EntityName → EntityName → Prop where +| DNFound : ∀ L A B, + A = B → + DefinedName (A::L) B +| DNRest : ∀ L A B, + A != B → + DefinedName L A → + DefinedName (B::L) A + +@[nolint docBlame] +inductive DefinedNames : List EntityName → List EntityName → Prop where +| DNSNil : ∀ ns, DefinedNames ns [] +| DNSCons : ∀ n ns0 ns, + DefinedName ns n → + DefinedNames ns ns0 → + DefinedNames ns (n::ns0) + +/-- Inductive relation specifying well-formedness conditions for Cedar types -/ +inductive WfCedarType : List EntityName → CedarType → Prop where +| WfBoolType : ∀ ns B, WfCedarType ns (CedarType.boolType B) +| WfIntType : ∀ ns, WfCedarType ns CedarType.intType +| WfStringType : ∀ ns, WfCedarType ns CedarType.stringType +| WfEntityType : ∀ ns n, + DefinedName ns n → + WfCedarType ns (CedarType.entityType n) +| WfSetType : ∀ T ns, + WfCedarType ns T → + WfCedarType ns (CedarType.setType T) +| WfRecordTypeNil : ∀ ns, WfCedarType ns CedarType.recordTypeNil +| WfRecordTypeConsNil : ∀ fn o T1 ns, + WfCedarType ns T1 → + WfCedarType ns (CedarType.recordTypeCons fn o T1 CedarType.recordTypeNil) +| WfRecordTypeConsCons : ∀ fn o T1 ns fn1 o1 T2 r, + WfCedarType ns T1 → + WfCedarType ns (CedarType.recordTypeCons fn1 o1 T2 r) → + WfCedarType ns (CedarType.recordTypeCons fn o T1 (CedarType.recordTypeCons fn1 o1 T2 r)) + +/-- Well-formed record types are types that are both well-formed and record types. + Note: in the original Coq code, this inductive relation is produced using QuickChick's + ability to merge inductive relations (see "Merging Inductive Relations", PLDI '23). + Chamelean currently doesn't this ability, so this inductive relation has been + manually ported over to Lean based on the merged relation produced by QuickChick. -/ +inductive WfRecordType : List EntityName → CedarType → Prop where +| WfRecordTypeConsConsRTcons : ∀ fn' o' T1' ns fn1 o1 T2 r, + WfCedarType ns (.recordTypeCons fn1 o1 T2 r) → + WfCedarType ns T1' → + WfRecordType ns (.recordTypeCons fn' o' T1' (.recordTypeCons fn1 o1 T2 r)) +| WfRecordTypeConsNilRTcons : ∀ fn' o' T1' ns, + WfCedarType ns T1' → + WfRecordType ns (.recordTypeCons fn' o' T1' .recordTypeNil) +| WfRecordTypeNilRTnil : ∀ (ns : List EntityName), WfRecordType ns .recordTypeNil + +------------------------------------------------------ +-- Schemas +------------------------------------------------------ + +@[nolint docBlame] +inductive EntitySchemaEntry where +| MkEntitySchemaEntry (ancestors : List EntityName) (attrs : List (String × Bool × CedarType)) +deriving BEq, DecidableEq + +/-- Well-formed attributes -/ +inductive WfAttrs : List EntityName → List (String × Bool × CedarType) → Prop where +| WfAttrsNil : ∀ ns, WfAttrs ns [] +| WfAttrsCons : ∀ ns T s b attrs, + WfCedarType ns T → + WfAttrs ns attrs → + WfAttrs ns ((s, b, T)::attrs) + +@[nolint docBlame] +inductive WfET : List EntityName → EntitySchemaEntry → Prop where +| WfETSingle : ∀ ns ancs attrs, + DefinedNames ns ancs → + WfAttrs ns attrs → + WfET ns (EntitySchemaEntry.MkEntitySchemaEntry ancs attrs) + +@[nolint docBlame] +inductive WfETS : List EntityName → List EntityName → List (EntityName × EntitySchemaEntry) → Prop where +| WfETSSingle : ∀ ns n et, + DefinedName ns n → + WfET ns et → + WfETS ns [n] [(n, et)] +| WfETSCons : ∀ n ns ns0 et ets, + DefinedName ns n → + WfET ns et → + WfETS ns ns0 ets → + WfETS ns (n::ns0) ((n, et)::ets) + +@[nolint docBlame] +inductive ActionSchemaEntry where +| MkActionSchemaEntry (prin : List EntityName) (res : List EntityName) (contextType : List (String × Bool × CedarType)) +deriving BEq, DecidableEq + +/-- LATER: Allow more than one principal and resource -/ +inductive WfACT : List EntityName → (EntityUID × ActionSchemaEntry) → Prop where +| WfACTSingle : ∀ n p r ns s attrs, + DefinedName ns n → + DefinedName ns p → + DefinedName ns r → + WfAttrs ns attrs → + WfACT ns ((EntityUID.MkEntityUID n s), (ActionSchemaEntry.MkActionSchemaEntry [p] [r] attrs)) + +@[nolint docBlame] +inductive WfACTS : List EntityName → List (EntityUID × ActionSchemaEntry) → Prop where +| WfACTSSingle : ∀ ns act, + WfACT ns act → + WfACTS ns [act] +| WfACTSCons : ∀ ns act acts, + WfACT ns act → + WfACTS ns acts → + WfACTS ns (act::acts) + +@[nolint docBlame] +inductive Schema where +| MkSchema (ets : List (EntityName × EntitySchemaEntry)) (acts : List (EntityUID × ActionSchemaEntry)) +deriving BEq, DecidableEq + +@[nolint docBlame] +inductive WfSchema : List EntityName → Schema → Prop where +| WfS : ∀ ns ets acts, + WfETS ns ns ets → + WfACTS ns acts → + WfSchema ns (Schema.MkSchema ets acts) + +@[nolint docBlame] +inductive DefinedEntity : List (EntityName × EntitySchemaEntry) → EntityName → Prop where +| DENow : ∀ n E R, DefinedEntity ((n, E)::R) n +| DELater : ∀ n n1 E R, + n != n1 → + DefinedEntity R n → + DefinedEntity ((n1, E)::R) n + +@[nolint docBlame] +inductive DefinedEntities : List (EntityName × EntitySchemaEntry) → List EntityName → Prop where +| DESNil : DefinedEntities [] [] +| DESCons : ∀ n ns et ets, + DefinedEntities ets ns → + DefinedEntities ((n, et)::ets) (n::ns) + +/-- NB: Ideally the string*bool parameter would be two distinct parameters. + It's written this way due to current QuickChick/Chamelean limitations on generation. -/ +inductive LookupEntityAttr : List (String × Bool × CedarType) → (String × Bool) → CedarType → Prop where +| LUNow : ∀ F B FS TF, + LookupEntityAttr ((F, B, TF)::FS) (F, B) TF +| LULater : ∀ F1 B1 F2 FS TF B, + F1 != F2 → + LookupEntityAttr FS (F1, B1) TF → + LookupEntityAttr ((F2, B, TF)::FS) (F1, B1) TF + +@[nolint docBlame] +inductive GetEntityAttr : List (EntityName × EntitySchemaEntry) → (EntityName × String × Bool) → CedarType → Prop where +| GENow : ∀ n fn b A E R T, + LookupEntityAttr E (fn, b) T → + GetEntityAttr ((n, (EntitySchemaEntry.MkEntitySchemaEntry A E))::R) (n, fn, b) T +| GELater : ∀ n n1 fn b E R T, + n != n1 → + GetEntityAttr R (n, fn, b) T → + GetEntityAttr ((n1, E)::R) (n, fn, b) T + +------------------------------------------------------ +-- Environments +------------------------------------------------------ + +@[nolint docBlame] +inductive RequestType where +| MkRequest (prin : EntityName) (act : EntityUID) (res : EntityName) (ctxt : List (String × Bool × CedarType)) +deriving BEq, DecidableEq + +/-- Converts a context description in RequestType to a Cedar record type -/ +inductive ReqContextToCedarType : List (String × Bool × CedarType) → CedarType → Prop where +| RNil : ReqContextToCedarType [] CedarType.recordTypeNil +| RCons : ∀ i B T R TR, + ReqContextToCedarType R TR → + ReqContextToCedarType ((i, B, T)::R) (CedarType.recordTypeCons i B T TR) + +@[nolint docBlame] +inductive ActionToRequestTypes : EntityUID → EntityName → List EntityName → List (String × Bool × CedarType) → List RequestType → List RequestType → Prop where +| ATRTSingle : ∀ uid p r c acc, + ActionToRequestTypes uid p [r] c acc ((RequestType.MkRequest p uid r c)::acc) +| ATRTCons : ∀ uid p r rs c reqs acc, + ActionToRequestTypes uid p rs c acc reqs → + ActionToRequestTypes uid p (r::rs) c acc ((RequestType.MkRequest p uid r c)::reqs) + +@[nolint docBlame] +inductive ActionSchemaEntryToRequestTypes : EntityUID → ActionSchemaEntry → List RequestType → List RequestType → Prop where +| ASTRTSingle : ∀ uid p rs c reqs acc, + ActionToRequestTypes uid p rs c acc reqs → + ActionSchemaEntryToRequestTypes uid (ActionSchemaEntry.MkActionSchemaEntry [p] rs c) acc reqs +| ASTRTCons : ∀ uid p ps rs c acc reqs reqs', + ActionToRequestTypes uid p rs c acc reqs' → + ActionSchemaEntryToRequestTypes uid (ActionSchemaEntry.MkActionSchemaEntry ps rs c) reqs' reqs → + ActionSchemaEntryToRequestTypes uid (ActionSchemaEntry.MkActionSchemaEntry (p::ps) rs c) acc reqs + +@[nolint docBlame] +inductive ActionSchemaToRequestTypes : List (EntityUID × ActionSchemaEntry) → List RequestType → List RequestType → Prop where +| ASTESingle : ∀ uid a acc reqs, + ActionSchemaEntryToRequestTypes uid a acc reqs → + ActionSchemaToRequestTypes [(uid, a)] acc reqs +| ASTECons : ∀ uid a ass acc reqs' reqs, + ActionSchemaEntryToRequestTypes uid a acc reqs' → + ActionSchemaToRequestTypes ass reqs' reqs → + ActionSchemaToRequestTypes ((uid, a)::ass) acc reqs + +@[nolint docBlame] +inductive Environment where +| MkEnvironment (schema : Schema) (reqType : RequestType) +deriving BEq, DecidableEq + +@[nolint docBlame] +inductive SchemaToEnvironments : Schema → List RequestType → List Environment → Prop where +| MkEnvsSingle : ∀ r s, + SchemaToEnvironments s [r] [(Environment.MkEnvironment s r)] +| MkEnvsCons : ∀ r rs s envs, + SchemaToEnvironments s rs envs → + SchemaToEnvironments s (r::rs) ((Environment.MkEnvironment s r)::envs) + +------------------------------------------------------ +-- Subtyping +------------------------------------------------------ + +/-- Note: Cedar has no width subtyping, just depth -/ +inductive SubType : CedarType → CedarType → Prop where +| SBoolAny : ∀ B, + SubType (CedarType.boolType B) (CedarType.boolType BoolType.anyBool) +| SSet : ∀ T1 T2, + SubType T1 T2 → + SubType (CedarType.setType T1) (CedarType.setType T2) +| SRecEmpty : + SubType CedarType.recordTypeNil CedarType.recordTypeNil +| SRecAttr : ∀ A o T1 T2 R1 R2, + SubType T1 T2 → + RecordType R2 → + SubType R1 R2 → + RecordType R1 → + SubType (CedarType.recordTypeCons A o T1 R1) (CedarType.recordTypeCons A o T2 R2) +| ST : ∀ T, SubType T T + +------------------------------------------------------ +-- Typing: Primitives and Variables +------------------------------------------------------ + +@[nolint docBlame] +inductive HasTypePrim : Environment → Prim → CedarType → Prop where +| TTrue : ∀ V, HasTypePrim V (Prim.boolean true) (CedarType.boolType BoolType.tt) +| TFalse : ∀ V, HasTypePrim V (Prim.boolean false) (CedarType.boolType BoolType.ff) +| TInt : ∀ V i, HasTypePrim V (Prim.int i) CedarType.intType +| TString : ∀ V s, HasTypePrim V (Prim.stringLit s) CedarType.stringType +| TEntity : ∀ ETS ACTS n i R, + DefinedEntity ETS n → + HasTypePrim + (Environment.MkEnvironment (Schema.MkSchema ETS ACTS) R) + (Prim.entityUID (EntityUID.MkEntityUID n i)) + (CedarType.entityType n) + +@[nolint docBlame] +inductive HasTypeVar : Environment → Var → CedarType → Prop where +| TPrincipal : ∀ s P A R C, + HasTypeVar (Environment.MkEnvironment s (RequestType.MkRequest P A R C)) Var.principal (CedarType.entityType P) +| TAction : ∀ s P n i R C, + HasTypeVar (Environment.MkEnvironment s (RequestType.MkRequest P (EntityUID.MkEntityUID n i) R C)) Var.action (CedarType.entityType n) +| TResource : ∀ s P A R C, + HasTypeVar (Environment.MkEnvironment s (RequestType.MkRequest P A R C)) Var.resource (CedarType.entityType R) +| TContext : ∀ s P A R C T, + ReqContextToCedarType C T → + HasTypeVar (Environment.MkEnvironment s (RequestType.MkRequest P A R C)) Var.context T + +@[nolint docBlame] +inductive BindAttrType : List EntityName → (CedarType × String × Bool) → CedarType → Prop where +| BindNow : ∀ x t b r ns, + WfRecordType ns r → + BindAttrType ns ((CedarType.recordTypeCons x b t r), x, b) t +| BindLater : ∀ x y b i t1 t r ns, + x != y → + WfRecordType ns r → + BindAttrType ns (r, x, b) t1 → + BindAttrType ns ((CedarType.recordTypeCons y i t r), x, b) t1 + +/-- A PathSet is a Cedar typing "capability" -- it is a set of accessible record-access expressions, or infinity (meaning all are accessible) -/ +inductive PathSet where +| allpaths +| somepaths (paths : List CedarExpr) +deriving Repr, BEq + +------------------------------------------------------ +-- Typing: Defining "Capabilities" for record access +------------------------------------------------------ + +/-- Membership test of `x` in `ps` -/ +def validPathExpr (x : CedarExpr) (ps : PathSet) : Bool := + let rec aux (xs : List CedarExpr) : Bool := + match xs with + | [] => false + | y::ys => + if x == y then true else aux ys + match ps with + | PathSet.allpaths => true + | PathSet.somepaths xs => aux xs + +/-- Intersects two pathsets -/ +def interExprs (ps : PathSet) (ys : PathSet) : PathSet := + let rec aux (xs : List CedarExpr) : List CedarExpr := + match xs with + | [] => [] + | x::xs' => + if validPathExpr x ys then x::(aux xs') + else aux xs' + match ps with + | PathSet.allpaths => ys + | PathSet.somepaths xs => PathSet.somepaths (aux xs) + +/-- returns `l` with `x` removed -/ +def subExprs (x : CedarExpr) (l : List CedarExpr) : List CedarExpr := + match l with + | [] => [] + | y::ys => + if x == y then ys + else y::(subExprs x ys) + +/-- union of `xs` and `ys` -/ +def mergeExprs (xs : PathSet) (ys : PathSet) : PathSet := + let rec aux (xs : List CedarExpr) (ys : List CedarExpr) : List CedarExpr := + match xs with + | [] => ys + | x::xs' => x::(aux xs' (subExprs x ys)) + match xs with + | PathSet.allpaths => PathSet.allpaths + | PathSet.somepaths xs0 => + match ys with + | PathSet.allpaths => PathSet.allpaths + | PathSet.somepaths ys0 => PathSet.somepaths (aux xs0 ys0) + +------------------------- +-- Typing: Expressions +------------------------- + +/-- `HasType a v (e,x) t` is equivalent to `a,v ⊢ e : t ; x` in the paper. This is + Written assuming we will derive a generator for (e,x) given a v and t (ideally e and x would be their own parameters). + + Note: Chamelean can only handle 23 out of the 41 typing rules -- + if we give it all 41 typing rules, it takes > 5 minutes to derive a generator. I've kept the 23 typing rules + for which we can derive a generator quickly. + + (I've commented out the remaining 18 typing rules, all of which involve *multiple* constraints expressed via auxiliary relations, + e.g. Subtyping, DefinedEntities, WfCedarType.) -/ +inductive HasType : PathSet → Environment → (CedarExpr × PathSet) → CedarType → Prop where +| TLitFalse : ∀ a V P, + HasTypePrim V P (CedarType.boolType BoolType.ff) → + HasType a V ((CedarExpr.lit P), PathSet.allpaths) (CedarType.boolType BoolType.ff) +| TLitOther : ∀ a V P T, + T != (CedarType.boolType BoolType.ff) → + HasTypePrim V P T → + HasType a V ((CedarExpr.lit P), PathSet.somepaths []) T +| TVar : ∀ a V X T, + HasTypeVar V X T → + HasType a V ((CedarExpr.var X), PathSet.somepaths []) T +| TCondTrue : ∀ a V E1 E2 E3 x1 x2 T2, + HasType a V (E1, x1) (CedarType.boolType BoolType.tt) → + HasType (mergeExprs a x1) V (E2, x2) T2 → + HasType a V ((CedarExpr.ite E1 E2 E3), (mergeExprs x1 x2)) T2 +| TCondFalse : ∀ a V E1 E2 E3 x1 x3 T3, + HasType a V (E1, x1) (CedarType.boolType BoolType.ff) → + HasType a V (E3, x3) T3 → + HasType a V ((CedarExpr.ite E1 E2 E3), x3) T3 +| TAnd : ∀ a x V E1 E2 T1, + HasType a V ((CedarExpr.ite E1 E2 (CedarExpr.lit (Prim.boolean false))), x) T1 → + HasType a V ((CedarExpr.andExpr E1 E2), x) T1 +| TOr : ∀ a x V E1 E2 T1, + HasType a V ((CedarExpr.ite E1 (CedarExpr.lit (Prim.boolean true)) E2), x) T1 → + HasType a V ((CedarExpr.orExpr E1 E2), x) T1 +| TNotAny : ∀ a x V e, + HasType a V (e, x) (CedarType.boolType BoolType.anyBool) → + HasType a V ((CedarExpr.unaryApp UnaryOp.not e), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +| TNotTrue : ∀ a x V e, + HasType a V (e, x) (CedarType.boolType BoolType.tt) → + HasType a V ((CedarExpr.unaryApp UnaryOp.not e), PathSet.allpaths) (CedarType.boolType BoolType.ff) +| TNotFalse : ∀ a x V e, + HasType a V (e, x) (CedarType.boolType BoolType.ff) → + HasType a V ((CedarExpr.unaryApp UnaryOp.not e), PathSet.somepaths []) (CedarType.boolType BoolType.tt) +| TNeg : ∀ a V x e, + HasType a V (e, x) CedarType.intType → + HasType a V ((CedarExpr.unaryApp UnaryOp.neg e), PathSet.somepaths []) CedarType.intType +| TLike : ∀ a V e x P, + HasType a V (e, x) CedarType.stringType → + HasType a V ((CedarExpr.unaryApp (UnaryOp.like P) e), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +| TEqLitTrue : ∀ a V P, + HasType a V ((CedarExpr.binaryApp BinaryOp.equals (CedarExpr.lit P) (CedarExpr.lit P)), PathSet.somepaths []) (CedarType.boolType BoolType.tt) +| TEqLitFalse : ∀ a V P1 P2, + P1 != P2 → + HasType a V ((CedarExpr.binaryApp BinaryOp.equals (CedarExpr.lit P1) (CedarExpr.lit P2)), PathSet.allpaths) (CedarType.boolType BoolType.ff) +| TLessThan : ∀ a x1 x2 V E1 E2, + HasType a V (E1, x1) CedarType.intType → + HasType a V (E2, x2) CedarType.intType → + HasType a V ((CedarExpr.binaryApp BinaryOp.less E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +| TLessEqualThan : ∀ a x1 x2 V E1 E2, + HasType a V (E1, x1) CedarType.intType → + HasType a V (E2, x2) CedarType.intType → + HasType a V ((CedarExpr.binaryApp BinaryOp.lessEq E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +| TAdd : ∀ a x1 x2 V E1 E2, + HasType a V (E1, x1) CedarType.intType → + HasType a V (E2, x2) CedarType.intType → + HasType a V ((CedarExpr.binaryApp BinaryOp.add E1 E2), PathSet.somepaths []) CedarType.intType +| TSub : ∀ a x1 x2 V E1 E2, + HasType a V (E1, x1) CedarType.intType → + HasType a V (E2, x2) CedarType.intType → + HasType a V ((CedarExpr.binaryApp BinaryOp.sub E1 E2), PathSet.somepaths []) CedarType.intType +| TMul : ∀ a x1 x2 V E1 E2, + HasType a V (E1, x1) CedarType.intType → + HasType a V (E2, x2) CedarType.intType → + HasType a V ((CedarExpr.binaryApp BinaryOp.mul E1 E2), PathSet.somepaths []) CedarType.intType +| TRecNil : ∀ a V, HasType a V (CedarExpr.recExprNil, PathSet.somepaths []) CedarType.recordTypeNil +| TRecCons : ∀ a x rx V e i T R b TR, + HasType a V (e, x) T → + RecordType TR → + HasType a V (R, rx) TR → + HasType a V ((CedarExpr.recExprCons i e R), PathSet.somepaths []) (CedarType.recordTypeCons i b T TR) +| TSetSingle : ∀ a x V e T, + HasType a V (e, x) T → + HasType a V ((CedarExpr.setExprCons e CedarExpr.setExprNil), PathSet.somepaths []) (CedarType.setType T) +| TSetMany : ∀ a x rx V e T R, + HasType a V (e, x) T → + HasType a V (R, rx) (CedarType.setType T) → + HasType a V ((CedarExpr.setExprCons e R), PathSet.somepaths []) (CedarType.setType T) +-- | TIsTrue : ∀ a x V e n ets acts R ns, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns (CedarType.entityType n) → +-- HasType a V (e, x) (CedarType.entityType n) → +-- HasType a V ((CedarExpr.unaryApp (UnaryOp.is n) e), PathSet.somepaths []) (CedarType.boolType BoolType.tt) +-- | TIsFalse : ∀ a x V e N1 N2 ets acts R ns, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns (CedarType.entityType N1) → +-- HasType a V (e, x) (CedarType.entityType N2) → +-- N1 != N2 → +-- HasType a V ((CedarExpr.unaryApp (UnaryOp.is N1) e), PathSet.allpaths) (CedarType.boolType BoolType.ff) +-- | TCondBool : ∀ a V E1 E2 E3 x1 x2 x3 T2 T3 T, +-- SubType T2 T → SubType T3 T → +-- HasType a V (E1, x1) (CedarType.boolType BoolType.anyBool) → +-- HasType (mergeExprs a x1) V (E2, x2) T2 → +-- HasType a V (E3, x3) T3 → +-- HasType a V ((CedarExpr.ite E1 E2 E3), (interExprs (mergeExprs x1 x2) x3)) T +-- | TEqEntity : ∀ a x1 x2 V E1 N1 E2 N2 ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns (CedarType.entityType N1) → +-- WfCedarType ns (CedarType.entityType N2) → +-- N1 != N2 → +-- HasType a V (E1, x1) (CedarType.entityType N1) → +-- HasType a V (E2, x2) (CedarType.entityType N2) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.equals E1 E2), PathSet.allpaths) (CedarType.boolType BoolType.ff) +-- | TEqAny : ∀ a x1 x2 V E1 E2 T T1 T2 ets acts R ns, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns T → +-- SubType T1 T → SubType T2 T → +-- HasType a V (E1, x1) T1 → +-- HasType a V (E2, x2) T2 → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.equals E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | TInEntity : ∀ a x1 x2 V E1 E2 N1 N2 ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns (CedarType.entityType N1) → +-- WfCedarType ns (CedarType.entityType N2) → +-- HasType a V (E1, x1) (CedarType.entityType N1) → +-- HasType a V (E2, x2) (CedarType.entityType N2) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.mem E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | TInEntitySet : ∀ a x1 x2 V E1 E2 N1 N2 ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns (CedarType.entityType N1) → +-- WfCedarType ns (CedarType.entityType N2) → +-- HasType a V (E1, x1) (CedarType.entityType N1) → +-- HasType a V (E2, x2) (CedarType.setType (CedarType.entityType N2)) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.mem E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | TContains : ∀ a x1 x2 V E1 E2 ets acts R ns T1 T2 T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns T → +-- SubType T1 T → SubType T2 T → +-- HasType a V (E1, x1) T1 → +-- HasType a V (E2, x2) (CedarType.setType T2) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.contains E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | TContainsAll : ∀ a x1 x2 V E1 E2 ets acts R ns T1 T2 T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns T → +-- SubType T1 T → SubType T2 T → +-- HasType a V (E1, x1) (CedarType.setType T1) → +-- HasType a V (E2, x2) (CedarType.setType T2) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.containsAll E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | TContainsAny : ∀ a x1 x2 V E1 E2 ets acts R ns T1 T2 T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- WfCedarType ns T → +-- SubType T1 T → SubType T2 T → +-- HasType a V (E1, x1) (CedarType.setType T1) → +-- HasType a V (E2, x2) (CedarType.setType T2) → +-- HasType a V ((CedarExpr.binaryApp BinaryOp.containsAny E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool) +-- | THasAttrRecOpt : ∀ a x V e F T TE ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- BindAttrType ns (TE, F, true) T → +-- HasType a V (e, x) TE → +-- HasType a V ((CedarExpr.hasAttr e F), (PathSet.somepaths [CedarExpr.getAttr e F])) (CedarType.boolType BoolType.anyBool) +-- | THasAttrRecReq : ∀ a x V e F T TE ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- BindAttrType ns (TE, F, false) T → +-- HasType a V (e, x) TE → +-- HasType a V ((CedarExpr.hasAttr e F), (PathSet.somepaths [CedarExpr.getAttr e F])) (CedarType.boolType BoolType.tt) +-- | TGetAttrRecOpt : ∀ a x V e F T TE ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- BindAttrType ns (TE, F, true) T → +-- HasType a V (e, x) TE → +-- validPathExpr (CedarExpr.getAttr e F) a = true → +-- HasType a V ((CedarExpr.getAttr e F), PathSet.somepaths []) T +-- | TGetAttrRecReq : ∀ a x V e F T TE ns ets acts R, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- DefinedEntities ets ns → +-- BindAttrType ns (TE, F, false) T → +-- HasType a V (e, x) TE → +-- HasType a V ((CedarExpr.getAttr e F), PathSet.somepaths []) T +-- | THasAttrEntityOpt : ∀ a x V ets acts R e n fn T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- GetEntityAttr ets (n, fn, true) T → +-- HasType a V (e, x) (CedarType.entityType n) → +-- HasType a V ((CedarExpr.hasAttr e fn), PathSet.somepaths [CedarExpr.getAttr e fn]) (CedarType.boolType BoolType.anyBool) +-- | THasAttrEntityReq : ∀ a x V ets acts R e n fn T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- GetEntityAttr ets (n, fn, false) T → +-- HasType a V (e, x) (CedarType.entityType n) → +-- HasType a V ((CedarExpr.hasAttr e fn), PathSet.somepaths [CedarExpr.getAttr e fn]) (CedarType.boolType BoolType.tt) +-- | TGetAttrEntityOpt : ∀ a x V ets acts R e n fn T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- GetEntityAttr ets (n, fn, true) T → +-- HasType a V (e, x) (CedarType.entityType n) → +-- validPathExpr (CedarExpr.getAttr e fn) a = true → +-- HasType a V ((CedarExpr.getAttr e fn), PathSet.somepaths []) T +-- | TGetAttrEntityReq : ∀ a x V ets acts R e n fn T, +-- V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) → +-- GetEntityAttr ets (n, fn, false) T → +-- HasType a V (e, x) (CedarType.entityType n) → +-- HasType a V ((CedarExpr.getAttr e fn), PathSet.somepaths []) T + + +------------------------------ +-- Pretty printing for types +------------------------------- +def stringOfBooltype (b : BoolType) : String := + match b with + | BoolType.anyBool => "Bool" + | BoolType.tt => "True" + | BoolType.ff => "False" + +instance : ToString BoolType where + toString := stringOfBooltype + +instance : Repr BoolType where + reprPrec boolTy _ := toString boolTy + +def stringOfCedartype (t : CedarType) : String := + match t with + | CedarType.boolType b => stringOfBooltype b + | CedarType.intType => "Int" + | CedarType.stringType => "String" + | CedarType.entityType n => toString n + | CedarType.setType t => "Set<" ++ stringOfCedartype t ++ ">" + | CedarType.recordTypeNil => "{}" + | CedarType.recordTypeCons s o t' CedarType.recordTypeNil => + "{" ++ s ++ ":" ++ (if o then "?" else " ") ++ stringOfCedartype t' ++ "}" + | CedarType.recordTypeCons s o t' tr => + "{" ++ s ++ ":" ++ (if o then "?" else " ") ++ stringOfCedartype t' ++ ", " ++ stringOfRecordtype tr ++ "}" +where + stringOfRecordtype (t : CedarType) : String := + match t with + | CedarType.recordTypeNil => "" + | CedarType.recordTypeCons s o t' tr => + s ++ ":" ++ (if o then "?" else " ") ++ stringOfCedartype t' ++ ", " ++ stringOfRecordtype tr + | _ => "" + +instance : ToString CedarType where + toString := stringOfCedartype + +instance : Repr CedarType where + reprPrec ty _ := toString ty + +def stringOfAttrs (attrs : List (String × Bool × CedarType)) : String := + match attrs with + | [] => "" + | [(s, o, t')] => s ++ ":" ++ (if o then " " else "? ") ++ stringOfCedartype t' + | (s, o, t')::attrs' => s ++ ":" ++ (if o then " " else "? ") ++ stringOfCedartype t' ++ ", " ++ stringOfAttrs attrs' + +def stringOfEse (ancs : List EntityName) (attrs : List (String × Bool × CedarType)) : String := + (match ancs with + | [] => " " + | _ => " in " ++ toString ancs) ++ + (match attrs with + | [] => "" + | _ => " { " ++ stringOfAttrs attrs ++ " }") + +instance : ToString EntitySchemaEntry where + toString := fun ese => + match ese with + | EntitySchemaEntry.MkEntitySchemaEntry ancs attrs => stringOfEse ancs attrs + +instance : Repr EntitySchemaEntry where + reprPrec ese _ := toString ese + +def stringOfAse (prin : List EntityName) (res : List EntityName) (ct : List (String × Bool × CedarType)) : String := + "{ principal: " ++ toString prin ++ + "; resource: " ++ toString res ++ + (match ct with | [] => "" | _ => "; context: {" ++ stringOfAttrs ct ++ " }") ++ " }" + +instance : ToString ActionSchemaEntry where + toString := fun ase => + match ase with + | ActionSchemaEntry.MkActionSchemaEntry ps rs ct => stringOfAse ps rs ct + +instance : Repr ActionSchemaEntry where + reprPrec ase _ := toString ase + +def stringOfSchemaEts (eses : List (EntityName × EntitySchemaEntry)) : String := + match eses with + | [] => "" + | (n, ese)::eses' => "entity " ++ toString n ++ toString ese ++ "; " ++ stringOfSchemaEts eses' + +def stringOfSchemaActs (acts : List (EntityUID × ActionSchemaEntry)) : String := + match acts with + | [] => "" + | (uid, act)::acts' => "action " ++ toString uid ++ " appliesTo " ++ toString act ++ "; " ++ stringOfSchemaActs acts' + +def stringOfSchema (s : Schema) : String := + match s with + | Schema.MkSchema ets acts => stringOfSchemaEts ets ++ stringOfSchemaActs acts + +instance : ToString Schema where + toString := stringOfSchema + +instance : Repr Schema where + reprPrec s _ := toString s + +instance : ToString PathSet where + toString := fun ps => match ps with + | PathSet.allpaths => "allpaths" + | PathSet.somepaths paths => "somepaths " ++ toString paths + +instance : Repr PathSet where + reprPrec pathset _ := toString pathset diff --git a/Test/CedarExample/CedarCheckerGenerators.lean b/Test/CedarExample/CedarCheckerGenerators.lean new file mode 100644 index 00000000..ea3416d5 --- /dev/null +++ b/Test/CedarExample/CedarCheckerGenerators.lean @@ -0,0 +1,2242 @@ +import Test.CedarExample.Cedar +import Plausible.Arbitrary +import Plausible.DeriveArbitrary +import Plausible.Chamelean.GeneratorCombinators +import Plausible.Chamelean.ArbitrarySizedSuchThat +import Plausible.Chamelean.DeriveChecker +import Plausible.Chamelean.DeriveConstrainedProducer + +open Plausible + +/-! +This file contains snapshot tests for checkers & generators that +are derived by Chamelean for the inductive relations defined in `Test/CedarExample.Cedar.lean`. + +Note: the structure of this file closely follows Mike Hicks's Coq formalization of Cedar (not publicly available), +in particular the order in which he derives checkers/generators using QuickChick. +-/ + +-- Suppress warnings for unused variables in derived generators/checkers +set_option linter.unusedVariables false + +-- Suppress warnings for redundant pattern-match cases in derived generators/checkers +set_option match.ignoreUnusedAlts true + +/-- We override the default `Arbitrary` instance for `String`s with our custom generator -/ +instance : Arbitrary String where + arbitrary := GeneratorCombinators.elementsWithDefault + "Aaron" ["Aaron", "John", "Mike", "Kesha", "Hicks", "A", "B", "C", "D"] + +-- Derive `Arbitrary` instances for Cedar data/types/expressions/schemas +deriving instance Arbitrary for + EntityName, EntityUID, Prim, Var, PatElem, UnaryOp, BinaryOp, CedarExpr, + Request, BoolType, CedarType, EntitySchemaEntry, ActionSchemaEntry, Schema, + RequestType, Environment, PathSet + +-------------------------------------------------- +-- Checker & Generator for `RecordExpr` relation +-------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (RecordExpr ce_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ce_1 : CedarExpr) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.recExprNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ce_1 with + | CedarExpr.recExprCons fn e r => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.recExprNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ce_1 with + | CedarExpr.recExprCons fn e r => Option.some Bool.true + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ce_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (RecordExpr ce) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarExpr (fun ce_1 => RecordExpr ce_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) : OptionT Plausible.Gen CedarExpr := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, return CedarExpr.recExprNil), + (1, do + let e ← Plausible.Arbitrary.arbitrary; + do + let fn ← Plausible.Arbitrary.arbitrary; + do + let r ← Plausible.Arbitrary.arbitrary; + return CedarExpr.recExprCons fn e r)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return CedarExpr.recExprNil), + (1, do + let e ← Plausible.Arbitrary.arbitrary; + do + let fn ← Plausible.Arbitrary.arbitrary; + do + let r ← Plausible.Arbitrary.arbitrary; + return CedarExpr.recExprCons fn e r), + ] + fun size => aux_arb size size +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ce : CedarExpr) => RecordExpr ce) + +----------------------------------------------- +-- Checker & Generator for `SetExpr` relation +----------------------------------------------- + + +/-- +info: Try this checker: instance : DecOpt (SetExpr ce_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ce_1 : CedarExpr) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.setExprNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ce_1 with + | CedarExpr.setExprCons e r => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.setExprNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ce_1 with + | CedarExpr.setExprCons e r => Option.some Bool.true + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ce_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (SetExpr ce) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarExpr (fun ce_1 => SetExpr ce_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) : OptionT Plausible.Gen CedarExpr := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, return CedarExpr.setExprNil), + (1, do + let e ← Plausible.Arbitrary.arbitrary; + do + let r ← Plausible.Arbitrary.arbitrary; + return CedarExpr.setExprCons e r)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return CedarExpr.setExprNil), + (1, do + let e ← Plausible.Arbitrary.arbitrary; + do + let r ← Plausible.Arbitrary.arbitrary; + return CedarExpr.setExprCons e r), + ] + fun size => aux_arb size size +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ce : CedarExpr) => SetExpr ce) + +-------------------------------------------------- +-- Checker & Generator for `SetEntityValues` relation +-------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (SetEntityValues ce_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ce_1 : CedarExpr) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.setExprNil => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ce_1 with + | CedarExpr.setExprNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ce_1 with + | CedarExpr.setExprCons (CedarExpr.lit (Prim.entityUID uid)) r => aux_dec initSize size' r + | _ => Option.some Bool.false] + fun size => aux_dec size size ce_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (SetEntityValues ce) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarExpr (fun ce_1 => SetEntityValues ce_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) : OptionT Plausible.Gen CedarExpr := + match size with + | Nat.zero => OptionTGen.backtrack [(1, return CedarExpr.setExprNil)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return CedarExpr.setExprNil), + (Nat.succ size', do + let r ← aux_arb initSize size'; + do + let uid ← Plausible.Arbitrary.arbitrary; + return CedarExpr.setExprCons (CedarExpr.lit (Prim.entityUID uid)) r)] + fun size => aux_arb size size +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ce : CedarExpr) => SetEntityValues ce) + +-------------------------------------------------- +-- Checker & Generator for `DefinedName` relation +-------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (DefinedName ns_1 n_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (n_1 : EntityName) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ns_1 with + | List.cons A L => DecOpt.decOpt (Eq A n_1) initSize + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ns_1 with + | List.cons A L => DecOpt.decOpt (Eq A n_1) initSize + | _ => Option.some Bool.false, + fun _ => + match ns_1 with + | List.cons B L => + DecOpt.andOptList [DecOpt.decOpt (Eq (bne n_1 B) (Bool.true)) initSize, aux_dec initSize size' L n_1] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 n_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (DefinedName ns n) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat EntityName (fun n_1 => DefinedName ns_1 n_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen EntityName := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ns_1 with + | List.cons A L => do + let n_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n_1 => Eq A n_1) initSize; + return n_1 + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ns_1 with + | List.cons A L => do + let n_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n_1 => Eq A n_1) initSize; + return n_1 + | _ => OptionT.fail), + (Nat.succ size', + match ns_1 with + | List.cons B L => do + let n_1 ← aux_arb initSize size' L; + match DecOpt.decOpt (Eq (bne n_1 B) (Bool.true)) initSize with + | Option.some Bool.true => return n_1 + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (n : EntityName) => DefinedName ns n) + +-------------------------------------------------- +-- Checker & Generator for `DefinedNames` relation +-------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (DefinedNames ns_1 ns0_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (ns0_1 : List EntityName) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ns0_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ns0_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ns0_1 with + | List.cons n ns0 => + DecOpt.andOptList [DecOpt.decOpt (DefinedName ns_1 n) initSize, aux_dec initSize size' ns_1 ns0] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 ns0_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (DefinedNames ns ns0) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List EntityName) (fun ns0_1 => DefinedNames ns_1 ns0_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen (List EntityName) := + match size with + | Nat.zero => OptionTGen.backtrack [(1, return List.nil)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return List.nil), + (Nat.succ size', do + let n ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n => DefinedName ns_1 n) initSize; + do + let ns0 ← aux_arb initSize size' ns_1; + return List.cons n ns0)] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ns0 : List EntityName) => DefinedNames ns ns0) + +-------------------------------------------------- +-- Checker & Generator for well-formed Cedar types +-------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (WfCedarType ns_1 ct_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (ct_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ct_1 with + | CedarType.boolType B => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.intType => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.stringType => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.entityType n => DecOpt.decOpt (DefinedName ns_1 n) initSize + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ct_1 with + | CedarType.boolType B => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.intType => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.stringType => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.entityType n => DecOpt.decOpt (DefinedName ns_1 n) initSize + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.setType T => aux_dec initSize size' ns_1 T + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeCons fn o T1 (CedarType.recordTypeNil) => aux_dec initSize size' ns_1 T1 + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeCons fn o T1 (CedarType.recordTypeCons fn1 o1 T2 r) => + DecOpt.andOptList + [aux_dec initSize size' ns_1 T1, aux_dec initSize size' ns_1 (CedarType.recordTypeCons fn1 o1 T2 r)] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 ct_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfCedarType ns ct) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun ct_1 => WfCedarType ns_1 ct_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let B ← Plausible.Arbitrary.arbitrary; + return CedarType.boolType B), + (1, return CedarType.intType), (1, return CedarType.stringType), + (1, do + let n ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n => DefinedName ns_1 n) initSize; + return CedarType.entityType n), + (1, return CedarType.recordTypeNil)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let B ← Plausible.Arbitrary.arbitrary; + return CedarType.boolType B), + (1, return CedarType.intType), (1, return CedarType.stringType), + (1, do + let n ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n => DefinedName ns_1 n) initSize; + return CedarType.entityType n), + (1, return CedarType.recordTypeNil), + (Nat.succ size', do + let T ← aux_arb initSize size' ns_1; + return CedarType.setType T), + (Nat.succ size', do + let T1 ← aux_arb initSize size' ns_1; + do + let fn ← Plausible.Arbitrary.arbitrary; + do + let o ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn o T1 (CedarType.recordTypeNil)), + (Nat.succ size', do + let T1 ← aux_arb initSize size' ns_1; + do + let vfn1_o1_T2_r ← aux_arb initSize size' ns_1; + match vfn1_o1_T2_r with + | CedarType.recordTypeCons fn1 o1 T2 r => do + let fn ← Plausible.Arbitrary.arbitrary; + do + let o ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn o T1 (CedarType.recordTypeCons fn1 o1 T2 r) + | _ => OptionT.fail)] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ct : CedarType) => WfCedarType ns ct) + +---------------------------------------------------- +-- Checker & Generator for well-formed record types +---------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (WfRecordType ns_1 rt_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (rt_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match rt_1 with + | CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeCons fn1 o1 T2 r) => + DecOpt.andOptList + [DecOpt.decOpt (WfCedarType ns_1 T1') initSize, + DecOpt.decOpt (WfCedarType ns_1 (CedarType.recordTypeCons fn1 o1 T2 r)) initSize] + | _ => Option.some Bool.false, + fun _ => + match rt_1 with + | CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeNil) => + DecOpt.decOpt (WfCedarType ns_1 T1') initSize + | _ => Option.some Bool.false, + fun _ => + match rt_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match rt_1 with + | CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeCons fn1 o1 T2 r) => + DecOpt.andOptList + [DecOpt.decOpt (WfCedarType ns_1 T1') initSize, + DecOpt.decOpt (WfCedarType ns_1 (CedarType.recordTypeCons fn1 o1 T2 r)) initSize] + | _ => Option.some Bool.false, + fun _ => + match rt_1 with + | CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeNil) => + DecOpt.decOpt (WfCedarType ns_1 T1') initSize + | _ => Option.some Bool.false, + fun _ => + match rt_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ns_1 rt_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfRecordType ns rt) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun rt_1 => WfRecordType ns_1 rt_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let T1' ← ArbitrarySizedSuchThat.arbitrarySizedST (fun T1' => WfCedarType ns_1 T1') initSize; + do + let vfn1_o1_T2_r ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun vfn1_o1_T2_r => WfCedarType ns_1 vfn1_o1_T2_r) initSize; + match vfn1_o1_T2_r with + | CedarType.recordTypeCons fn1 o1 T2 r => do + let fn' ← Plausible.Arbitrary.arbitrary; + do + let o' ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeCons fn1 o1 T2 r) + | _ => OptionT.fail), + (1, do + let T1' ← ArbitrarySizedSuchThat.arbitrarySizedST (fun T1' => WfCedarType ns_1 T1') initSize; + do + let fn' ← Plausible.Arbitrary.arbitrary; + do + let o' ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeNil)), + (1, return CedarType.recordTypeNil)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let T1' ← ArbitrarySizedSuchThat.arbitrarySizedST (fun T1' => WfCedarType ns_1 T1') initSize; + do + let vfn1_o1_T2_r ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun vfn1_o1_T2_r => WfCedarType ns_1 vfn1_o1_T2_r) initSize; + match vfn1_o1_T2_r with + | CedarType.recordTypeCons fn1 o1 T2 r => do + let fn' ← Plausible.Arbitrary.arbitrary; + do + let o' ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeCons fn1 o1 T2 r) + | _ => OptionT.fail), + (1, do + let T1' ← ArbitrarySizedSuchThat.arbitrarySizedST (fun T1' => WfCedarType ns_1 T1') initSize; + do + let fn' ← Plausible.Arbitrary.arbitrary; + do + let o' ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn' o' T1' (CedarType.recordTypeNil)), + (1, return CedarType.recordTypeNil), ] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (rt : CedarType) => WfRecordType ns rt) + +---------------------------------------------------- +-- Checker & Generator for well-formed attributes +---------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (WfAttrs ns_1 attrs_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) + (attrs_1 : List (String × Bool × CedarType)) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match attrs_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match attrs_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match attrs_1 with + | List.cons (Prod.mk s (Prod.mk b T)) attrs => + DecOpt.andOptList [DecOpt.decOpt (WfCedarType ns_1 T) initSize, aux_dec initSize size' ns_1 attrs] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 attrs_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfAttrs ns attrs) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × Bool × CedarType)) (fun attrs_1 => WfAttrs ns_1 attrs_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : + OptionT Plausible.Gen (List (String × Bool × CedarType)) := + match size with + | Nat.zero => OptionTGen.backtrack [(1, return List.nil)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return List.nil), + (Nat.succ size', do + let T ← ArbitrarySizedSuchThat.arbitrarySizedST (fun T => WfCedarType ns_1 T) initSize; + do + let attrs ← aux_arb initSize size' ns_1; + do + let b ← Plausible.Arbitrary.arbitrary; + do + let s ← Plausible.Arbitrary.arbitrary; + return List.cons (Prod.mk s (Prod.mk b T)) attrs)] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (attrs : List (String × Bool × CedarType)) => WfAttrs ns attrs) + +--------------------------------------------------------------------- +-- Checker & Generator for well-formed `EntitySchemaEntry`(ies) +--------------------------------------------------------------------- +/-- +info: Try this checker: instance : DecOpt (WfET ns_1 et_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (et_1 : EntitySchemaEntry) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match et_1 with + | EntitySchemaEntry.MkEntitySchemaEntry ancs attrs => + DecOpt.andOptList + [DecOpt.decOpt (DefinedNames ns_1 ancs) initSize, DecOpt.decOpt (WfAttrs ns_1 attrs) initSize] + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match et_1 with + | EntitySchemaEntry.MkEntitySchemaEntry ancs attrs => + DecOpt.andOptList + [DecOpt.decOpt (DefinedNames ns_1 ancs) initSize, DecOpt.decOpt (WfAttrs ns_1 attrs) initSize] + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ns_1 et_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfET ns et) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat EntitySchemaEntry (fun et_1 => WfET ns_1 et_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen EntitySchemaEntry := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let ancs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun ancs => DefinedNames ns_1 ancs) initSize; + do + let attrs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun attrs => WfAttrs ns_1 attrs) initSize; + return EntitySchemaEntry.MkEntitySchemaEntry ancs attrs)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let ancs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun ancs => DefinedNames ns_1 ancs) initSize; + do + let attrs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun attrs => WfAttrs ns_1 attrs) initSize; + return EntitySchemaEntry.MkEntitySchemaEntry ancs attrs), + ] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (et : EntitySchemaEntry) => WfET ns et) + +/-- +info: Try this checker: instance : DecOpt (WfETS ns_1 ns0_1 ets_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (ns0_1 : List EntityName) + (ets_1 : List (EntityName × EntitySchemaEntry)) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ets_1 with + | List.cons (Prod.mk u_3 et) (List.nil) => + match ns0_1 with + | List.cons n (List.nil) => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 n) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 n) initSize, DecOpt.decOpt (WfET ns_1 et) initSize]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ets_1 with + | List.cons (Prod.mk u_3 et) (List.nil) => + match ns0_1 with + | List.cons n (List.nil) => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 n) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 n) initSize, DecOpt.decOpt (WfET ns_1 et) initSize]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match ets_1 with + | List.cons (Prod.mk u_3 et) ets => + match ns0_1 with + | List.cons n ns0 => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 n) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 n) initSize, + DecOpt.andOptList [DecOpt.decOpt (WfET ns_1 et) initSize, aux_dec initSize size' ns_1 ns0 ets]]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 ns0_1 ets_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfETS ns ns0 ets) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List (EntityName × EntitySchemaEntry)) (fun ets_1 => WfETS ns_1 ns0_1 ets_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (ns0_1 : List EntityName) : + OptionT Plausible.Gen (List (EntityName × EntitySchemaEntry)) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ns0_1 with + | List.cons n (List.nil) => + match DecOpt.decOpt (DefinedName ns_1 n) initSize with + | Option.some Bool.true => do + let et ← ArbitrarySizedSuchThat.arbitrarySizedST (fun et => WfET ns_1 et) initSize; + return List.cons (Prod.mk n et) (List.nil) + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ns0_1 with + | List.cons n (List.nil) => + match DecOpt.decOpt (DefinedName ns_1 n) initSize with + | Option.some Bool.true => do + let et ← ArbitrarySizedSuchThat.arbitrarySizedST (fun et => WfET ns_1 et) initSize; + return List.cons (Prod.mk n et) (List.nil) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match ns0_1 with + | List.cons n ns0 => + match DecOpt.decOpt (DefinedName ns_1 n) initSize with + | Option.some Bool.true => do + let et ← ArbitrarySizedSuchThat.arbitrarySizedST (fun et => WfET ns_1 et) initSize; + do + let ets ← aux_arb initSize size' ns_1 ns0; + return List.cons (Prod.mk n et) ets + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size ns_1 ns0_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ets : List (EntityName × EntitySchemaEntry)) => WfETS ns ns0 ets) + +--------------------------------------------------------------------- +-- Checker & Generator for well-formed `ActionSchemaEntry`(ies) +--------------------------------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (WfACT ns_1 act_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (act_1 : EntityUID × ActionSchemaEntry) : + Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match act_1 with + | + Prod.mk (EntityUID.MkEntityUID n s) + (ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) (List.cons r (List.nil)) attrs) => + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 n) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 p) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 r) initSize, DecOpt.decOpt (WfAttrs ns_1 attrs) initSize]]] + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match act_1 with + | + Prod.mk (EntityUID.MkEntityUID n s) + (ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) (List.cons r (List.nil)) attrs) => + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 n) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 p) initSize, + DecOpt.andOptList + [DecOpt.decOpt (DefinedName ns_1 r) initSize, DecOpt.decOpt (WfAttrs ns_1 attrs) initSize]]] + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ns_1 act_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfACT ns act) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (EntityUID × ActionSchemaEntry) (fun act_1 => WfACT ns_1 act_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : + OptionT Plausible.Gen (EntityUID × ActionSchemaEntry) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let n ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n => DefinedName ns_1 n) initSize; + do + let p ← ArbitrarySizedSuchThat.arbitrarySizedST (fun p => DefinedName ns_1 p) initSize; + do + let r ← ArbitrarySizedSuchThat.arbitrarySizedST (fun r => DefinedName ns_1 r) initSize; + do + let attrs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun attrs => WfAttrs ns_1 attrs) initSize; + do + let s ← Plausible.Arbitrary.arbitrary; + return + Prod.mk (EntityUID.MkEntityUID n s) + (ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) (List.cons r (List.nil)) + attrs))] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let n ← ArbitrarySizedSuchThat.arbitrarySizedST (fun n => DefinedName ns_1 n) initSize; + do + let p ← ArbitrarySizedSuchThat.arbitrarySizedST (fun p => DefinedName ns_1 p) initSize; + do + let r ← ArbitrarySizedSuchThat.arbitrarySizedST (fun r => DefinedName ns_1 r) initSize; + do + let attrs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun attrs => WfAttrs ns_1 attrs) initSize; + do + let s ← Plausible.Arbitrary.arbitrary; + return + Prod.mk (EntityUID.MkEntityUID n s) + (ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) (List.cons r (List.nil)) + attrs)), + ] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (act : EntityUID × ActionSchemaEntry) => WfACT ns act) + +/-- +info: Try this checker: instance : DecOpt (WfACTS ns_1 act_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) + (act_1 : List (EntityUID × ActionSchemaEntry)) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match act_1 with + | List.cons act (List.nil) => DecOpt.decOpt (WfACT ns_1 act) initSize + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match act_1 with + | List.cons act (List.nil) => DecOpt.decOpt (WfACT ns_1 act) initSize + | _ => Option.some Bool.false, + fun _ => + match act_1 with + | List.cons act acts => + DecOpt.andOptList [DecOpt.decOpt (WfACT ns_1 act) initSize, aux_dec initSize size' ns_1 acts] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 act_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfACTS ns act) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List (EntityUID × ActionSchemaEntry)) (fun act_1 => WfACTS ns_1 act_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : + OptionT Plausible.Gen (List (EntityUID × ActionSchemaEntry)) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let act ← ArbitrarySizedSuchThat.arbitrarySizedST (fun act => WfACT ns_1 act) initSize; + return List.cons act (List.nil))] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let act ← ArbitrarySizedSuchThat.arbitrarySizedST (fun act => WfACT ns_1 act) initSize; + return List.cons act (List.nil)), + (Nat.succ size', do + let act ← ArbitrarySizedSuchThat.arbitrarySizedST (fun act => WfACT ns_1 act) initSize; + do + let acts ← aux_arb initSize size' ns_1; + return List.cons act acts)] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (act : List (EntityUID × ActionSchemaEntry)) => WfACTS ns act) + +------------------------------------------------------------ +-- Checker & Generator for well-formed schemas +------------------------------------------------------------ +/-- +info: Try this checker: instance : DecOpt (WfSchema ns_1 s_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (s_1 : Schema) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match s_1 with + | Schema.MkSchema ets acts => + DecOpt.andOptList + [DecOpt.decOpt (WfACTS ns_1 acts) initSize, DecOpt.decOpt (WfETS ns_1 ns_1 ets) initSize] + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match s_1 with + | Schema.MkSchema ets acts => + DecOpt.andOptList + [DecOpt.decOpt (WfACTS ns_1 acts) initSize, DecOpt.decOpt (WfETS ns_1 ns_1 ets) initSize] + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ns_1 s_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (WfSchema ns s) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat Schema (fun s_1 => WfSchema ns_1 s_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) : OptionT Plausible.Gen Schema := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let acts ← ArbitrarySizedSuchThat.arbitrarySizedST (fun acts => WfACTS ns_1 acts) initSize; + do + let ets ← ArbitrarySizedSuchThat.arbitrarySizedST (fun ets => WfETS ns_1 ns_1 ets) initSize; + return Schema.MkSchema ets acts)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let acts ← ArbitrarySizedSuchThat.arbitrarySizedST (fun acts => WfACTS ns_1 acts) initSize; + do + let ets ← ArbitrarySizedSuchThat.arbitrarySizedST (fun ets => WfETS ns_1 ns_1 ets) initSize; + return Schema.MkSchema ets acts), + ] + fun size => aux_arb size size ns_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (s : Schema) => WfSchema ns s) + +------------------------------------------------------------ +-- Checker & Generator for defined entities +------------------------------------------------------------ +/-- +info: Try this checker: instance : DecOpt (DefinedEntity ets_1 n_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ets_1 : List (EntityName × EntitySchemaEntry)) (n_1 : EntityName) : + Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ets_1 with + | List.cons (Prod.mk n E) R => DecOpt.decOpt (BEq.beq n n_1) initSize + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ets_1 with + | List.cons (Prod.mk n E) R => DecOpt.decOpt (BEq.beq n n_1) initSize + | _ => Option.some Bool.false, + fun _ => + match ets_1 with + | List.cons (Prod.mk n1 E) R => + DecOpt.andOptList [DecOpt.decOpt (Eq (bne n_1 n1) (Bool.true)) initSize, aux_dec initSize size' R n_1] + | _ => Option.some Bool.false] + fun size => aux_dec size size ets_1 n_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (DefinedEntity ets n) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat EntityName (fun n_1 => DefinedEntity ets_1 n_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ets_1 : List (EntityName × EntitySchemaEntry)) : + OptionT Plausible.Gen EntityName := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.cons (Prod.mk n E) R => return n + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.cons (Prod.mk n E) R => return n + | _ => OptionT.fail), + (Nat.succ size', + match ets_1 with + | List.cons (Prod.mk n1 E) R => do + let n_1 ← aux_arb initSize size' R; + match DecOpt.decOpt (Eq (bne n_1 n1) (Bool.true)) initSize with + | Option.some Bool.true => return n_1 + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size ets_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (n : EntityName) => DefinedEntity ets n) + +/-- +info: Try this checker: instance : DecOpt (DefinedEntities ets_1 n_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ets_1 : List (EntityName × EntitySchemaEntry)) + (n_1 : List EntityName) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match n_1 with + | List.nil => + match ets_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match n_1 with + | List.nil => + match ets_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match n_1 with + | List.cons u_2 ns => + match ets_1 with + | List.cons (Prod.mk n et) ets => + DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 n) initSize, aux_dec initSize size' ets ns] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + fun size => aux_dec size size ets_1 n_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (DefinedEntities ets n) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List EntityName) (fun n_1 => DefinedEntities ets_1 n_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ets_1 : List (EntityName × EntitySchemaEntry)) : + OptionT Plausible.Gen (List EntityName) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.nil => return List.nil + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.nil => return List.nil + | _ => OptionT.fail), + (Nat.succ size', + match ets_1 with + | List.cons (Prod.mk n et) ets => do + let ns ← aux_arb initSize size' ets; + return List.cons n ns + | _ => OptionT.fail)] + fun size => aux_arb size size ets_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (n : List EntityName) => DefinedEntities ets n) + +--------------------------------------------- +-- Schema: LookupEntityAttr / GetEntityAttr +--------------------------------------------- + +/-- +info: Try this checker: instance : DecOpt (LookupEntityAttr l_1 fnb_1 t_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (l_1 : List (String × Bool × CedarType)) (fnb_1 : String × Bool) + (t_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match fnb_1 with + | Prod.mk u_3 u_4 => + match l_1 with + | List.cons (Prod.mk F (Prod.mk B TF)) FS => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 F) initSize, + DecOpt.andOptList [DecOpt.decOpt (BEq.beq TF t_1) initSize, DecOpt.decOpt (BEq.beq u_4 B) initSize]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match fnb_1 with + | Prod.mk u_3 u_4 => + match l_1 with + | List.cons (Prod.mk F (Prod.mk B TF)) FS => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 F) initSize, + DecOpt.andOptList [DecOpt.decOpt (BEq.beq TF t_1) initSize, DecOpt.decOpt (BEq.beq u_4 B) initSize]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match fnb_1 with + | Prod.mk F1 B1 => + match l_1 with + | List.cons (Prod.mk F2 (Prod.mk B TF)) FS => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq TF t_1) initSize, + DecOpt.andOptList + [DecOpt.decOpt (Eq (bne F1 F2) (Bool.true)) initSize, + aux_dec initSize size' FS (Prod.mk F1 B1) t_1]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + fun size => aux_dec size size l_1 fnb_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (LookupEntityAttr l fnb t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (String × Bool) (fun fnb_1 => LookupEntityAttr l_1 fnb_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (l_1 : List (String × Bool × CedarType)) (t_1 : CedarType) : + OptionT Plausible.Gen (String × Bool) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match l_1 with + | List.cons (Prod.mk F (Prod.mk B TF)) FS => + match DecOpt.decOpt (BEq.beq TF t_1) initSize with + | Option.some Bool.true => return Prod.mk F B + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match l_1 with + | List.cons (Prod.mk F (Prod.mk B TF)) FS => + match DecOpt.decOpt (BEq.beq TF t_1) initSize with + | Option.some Bool.true => return Prod.mk F B + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match l_1 with + | List.cons (Prod.mk F2 (Prod.mk B TF)) FS => + match DecOpt.decOpt (BEq.beq TF t_1) initSize with + | Option.some Bool.true => do + let vF1_B1 ← aux_arb initSize size' FS t_1; + match vF1_B1 with + | Prod.mk F1 B1 => + match DecOpt.decOpt (Eq (bne F1 F2) (Bool.true)) initSize with + | Option.some Bool.true => return Prod.mk F1 B1 + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size l_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (fnb : (String × Bool)) => LookupEntityAttr l fnb t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (EntityName × String × Bool) (fun nfn_1 => GetEntityAttr ets_1 nfn_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ets_1 : List (EntityName × EntitySchemaEntry)) (t_1 : CedarType) : + OptionT Plausible.Gen (EntityName × String × Bool) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.cons (Prod.mk n (EntitySchemaEntry.MkEntitySchemaEntry A E)) R => do + let vfn_b ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun vfn_b => LookupEntityAttr E vfn_b t_1) initSize; + match vfn_b with + | Prod.mk fn b => return Prod.mk n (Prod.mk fn b) + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ets_1 with + | List.cons (Prod.mk n (EntitySchemaEntry.MkEntitySchemaEntry A E)) R => do + let vfn_b ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun vfn_b => LookupEntityAttr E vfn_b t_1) initSize; + match vfn_b with + | Prod.mk fn b => return Prod.mk n (Prod.mk fn b) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match ets_1 with + | List.cons (Prod.mk n1 E) R => do + let vn_fn_b ← aux_arb initSize size' R t_1; + match vn_fn_b with + | Prod.mk n (Prod.mk fn b) => + match DecOpt.decOpt (Eq (bne n n1) (Bool.true)) initSize with + | Option.some Bool.true => return Prod.mk n (Prod.mk fn b) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size ets_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (nfn : (EntityName × String × Bool)) => GetEntityAttr ets nfn t) + +/-- +info: Try this checker: instance : DecOpt (ReqContextToCedarType c_1 t_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (c_1 : List (String × Bool × CedarType)) (t_1 : CedarType) : + Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match t_1 with + | CedarType.recordTypeNil => + match c_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match t_1 with + | CedarType.recordTypeNil => + match c_1 with + | List.nil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match t_1 with + | CedarType.recordTypeCons u_2 u_3 u_4 TR => + match c_1 with + | List.cons (Prod.mk i (Prod.mk B T)) R => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 B) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_4 T) initSize, + DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 i) initSize, aux_dec initSize size' R TR]]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + fun size => aux_dec size size c_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (ReqContextToCedarType c t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun t_1 => ReqContextToCedarType c_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (c_1 : List (String × Bool × CedarType)) : + OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match c_1 with + | List.nil => return CedarType.recordTypeNil + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match c_1 with + | List.nil => return CedarType.recordTypeNil + | _ => OptionT.fail), + (Nat.succ size', + match c_1 with + | List.cons (Prod.mk i (Prod.mk B T)) R => do + let TR ← aux_arb initSize size' R; + return CedarType.recordTypeCons i B T TR + | _ => OptionT.fail)] + fun size => aux_arb size size c_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (t : CedarType) => ReqContextToCedarType c t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List RequestType) (fun reqs_1 => ActionToRequestTypes e_1 n_1 ns_1 l_1 rs_1 reqs_1) + where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (e_1 : EntityUID) (n_1 : EntityName) (ns_1 : List EntityName) + (l_1 : List (String × Bool × CedarType)) (rs_1 : List RequestType) : OptionT Plausible.Gen (List RequestType) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ns_1 with + | List.cons r (List.nil) => return List.cons (RequestType.MkRequest n_1 e_1 r l_1) rs_1 + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ns_1 with + | List.cons r (List.nil) => return List.cons (RequestType.MkRequest n_1 e_1 r l_1) rs_1 + | _ => OptionT.fail), + (Nat.succ size', + match ns_1 with + | List.cons r rs => do + let reqs ← aux_arb initSize size' e_1 n_1 rs l_1 rs_1; + return List.cons (RequestType.MkRequest n_1 e_1 r l_1) reqs + | _ => OptionT.fail)] + fun size => aux_arb size size e_1 n_1 ns_1 l_1 rs_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (reqs : List RequestType) => ActionToRequestTypes e n ns l rs reqs) + +/-- +info: Try this generator: instance : + ArbitrarySizedSuchThat (List RequestType) (fun reqs_1 => ActionSchemaEntryToRequestTypes e_1 ae_1 ls_1 reqs_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (e_1 : EntityUID) (ae_1 : ActionSchemaEntry) + (ls_1 : List RequestType) : OptionT Plausible.Gen (List RequestType) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match ae_1 with + | ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) rs c => do + let reqs_1 ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun reqs_1 => ActionToRequestTypes e_1 p rs c ls_1 reqs_1) + initSize; + return reqs_1 + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match ae_1 with + | ActionSchemaEntry.MkActionSchemaEntry (List.cons p (List.nil)) rs c => do + let reqs_1 ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun reqs_1 => ActionToRequestTypes e_1 p rs c ls_1 reqs_1) + initSize; + return reqs_1 + | _ => OptionT.fail), + (Nat.succ size', + match ae_1 with + | ActionSchemaEntry.MkActionSchemaEntry (List.cons p ps) rs c => do + let reqs' ← + ArbitrarySizedSuchThat.arbitrarySizedST (fun reqs' => ActionToRequestTypes e_1 p rs c ls_1 reqs') + initSize; + do + let reqs_1 ← aux_arb initSize size' e_1 (ActionSchemaEntry.MkActionSchemaEntry ps rs c) reqs'; + return reqs_1 + | _ => OptionT.fail)] + fun size => aux_arb size size e_1 ae_1 ls_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (reqs : List RequestType) => ActionSchemaEntryToRequestTypes e ae ls reqs) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List RequestType) (fun reqs_1 => ActionSchemaToRequestTypes acts_1 ls_1 reqs_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (acts_1 : List (EntityUID × ActionSchemaEntry)) + (ls_1 : List RequestType) : OptionT Plausible.Gen (List RequestType) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match acts_1 with + | List.cons (Prod.mk uid a) (List.nil) => do + let reqs_1 ← + ArbitrarySizedSuchThat.arbitrarySizedST + (fun reqs_1 => ActionSchemaEntryToRequestTypes uid a ls_1 reqs_1) initSize; + return reqs_1 + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match acts_1 with + | List.cons (Prod.mk uid a) (List.nil) => do + let reqs_1 ← + ArbitrarySizedSuchThat.arbitrarySizedST + (fun reqs_1 => ActionSchemaEntryToRequestTypes uid a ls_1 reqs_1) initSize; + return reqs_1 + | _ => OptionT.fail), + (Nat.succ size', + match acts_1 with + | List.cons (Prod.mk uid a) ass => do + let reqs' ← + ArbitrarySizedSuchThat.arbitrarySizedST + (fun reqs' => ActionSchemaEntryToRequestTypes uid a ls_1 reqs') initSize; + do + let reqs_1 ← aux_arb initSize size' ass reqs'; + return reqs_1 + | _ => OptionT.fail)] + fun size => aux_arb size size acts_1 ls_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (reqs : List RequestType) => ActionSchemaToRequestTypes acts ls reqs) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (List Environment) (fun es_1 => SchemaToEnvironments s_1 l_1 es_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (s_1 : Schema) (l_1 : List RequestType) : + OptionT Plausible.Gen (List Environment) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match l_1 with + | List.cons r (List.nil) => return List.cons (Environment.MkEnvironment s_1 r) (List.nil) + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match l_1 with + | List.cons r (List.nil) => return List.cons (Environment.MkEnvironment s_1 r) (List.nil) + | _ => OptionT.fail), + (Nat.succ size', + match l_1 with + | List.cons r rs => do + let envs ← aux_arb initSize size' s_1 rs; + return List.cons (Environment.MkEnvironment s_1 r) envs + | _ => OptionT.fail)] + fun size => aux_arb size size s_1 l_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (es : List Environment) => SchemaToEnvironments s l es) + +--------------------------------------- +-- Checker & Generator for RecordTypes +--------------------------------------- +/-- +info: Try this checker: instance : DecOpt (RecordType ct_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ct_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match ct_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeCons fn o T1 T2 => Option.some Bool.true + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match ct_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false, + fun _ => + match ct_1 with + | CedarType.recordTypeCons fn o T1 T2 => Option.some Bool.true + | _ => Option.some Bool.false, + ] + fun size => aux_dec size size ct_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (RecordType ct) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun ct_1 => RecordType ct_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) : OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, return CedarType.recordTypeNil), + (1, do + let T1 ← Plausible.Arbitrary.arbitrary; + do + let T2 ← Plausible.Arbitrary.arbitrary; + do + let fn ← Plausible.Arbitrary.arbitrary; + do + let o ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn o T1 T2)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, return CedarType.recordTypeNil), + (1, do + let T1 ← Plausible.Arbitrary.arbitrary; + do + let T2 ← Plausible.Arbitrary.arbitrary; + do + let fn ← Plausible.Arbitrary.arbitrary; + do + let o ← Plausible.Arbitrary.arbitrary; + return CedarType.recordTypeCons fn o T1 T2), + ] + fun size => aux_arb size size +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ct : CedarType) => RecordType ct) + +-------------------- +-- Subtyping & Typing +-------------------- +/-- +info: Try this checker: instance : DecOpt (SubType t1_1 t2_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (t1_1 : CedarType) (t2_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match t2_1 with + | CedarType.boolType (BoolType.anyBool) => + match t1_1 with + | CedarType.boolType B => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match t2_1 with + | CedarType.recordTypeNil => + match t1_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => DecOpt.decOpt (BEq.beq t1_1 t2_1) initSize] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match t2_1 with + | CedarType.boolType (BoolType.anyBool) => + match t1_1 with + | CedarType.boolType B => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match t2_1 with + | CedarType.recordTypeNil => + match t1_1 with + | CedarType.recordTypeNil => Option.some Bool.true + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => DecOpt.decOpt (BEq.beq t1_1 t2_1) initSize, fun _ => + match t2_1 with + | CedarType.setType T2 => + match t1_1 with + | CedarType.setType T1 => aux_dec initSize size' T1 T2 + | _ => Option.some Bool.false + | _ => Option.some Bool.false, + fun _ => + match t2_1 with + | CedarType.recordTypeCons u_2 u_3 T2 R2 => + match t1_1 with + | CedarType.recordTypeCons A o T1 R1 => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_2 A) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 o) initSize, + DecOpt.andOptList + [DecOpt.decOpt (RecordType R2) initSize, + DecOpt.andOptList + [DecOpt.decOpt (RecordType R1) initSize, + DecOpt.andOptList [aux_dec initSize size' T1 T2, aux_dec initSize size' R1 R2]]]]] + | _ => Option.some Bool.false + | _ => Option.some Bool.false] + fun size => aux_dec size size t1_1 t2_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (SubType t1 t2) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun t1_1 => SubType t1_1 t2_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (t2_1 : CedarType) : OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match t2_1 with + | CedarType.boolType (BoolType.anyBool) => do + let B ← Plausible.Arbitrary.arbitrary; + return CedarType.boolType B + | _ => OptionT.fail), + (1, + match t2_1 with + | CedarType.recordTypeNil => return CedarType.recordTypeNil + | _ => OptionT.fail), + (1, return t2_1)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match t2_1 with + | CedarType.boolType (BoolType.anyBool) => do + let B ← Plausible.Arbitrary.arbitrary; + return CedarType.boolType B + | _ => OptionT.fail), + (1, + match t2_1 with + | CedarType.recordTypeNil => return CedarType.recordTypeNil + | _ => OptionT.fail), + (1, return t2_1), + (Nat.succ size', + match t2_1 with + | CedarType.setType T2 => do + let T1 ← aux_arb initSize size' T2; + return CedarType.setType T1 + | _ => OptionT.fail), + (Nat.succ size', + match t2_1 with + | CedarType.recordTypeCons A o T2 R2 => + match DecOpt.decOpt (RecordType R2) initSize with + | Option.some Bool.true => do + let R1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun R1 => RecordType R1) initSize; + match DecOpt.decOpt (SubType R1 R2) initSize with + | Option.some Bool.true => do + let T1 ← aux_arb initSize size' T2; + return CedarType.recordTypeCons A o T1 R1 + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size t2_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (t1 : CedarType) => SubType t1 t2) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat Prim (fun p_1 => HasTypePrim v_1 p_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (v_1 : Environment) (t_1 : CedarType) : OptionT Plausible.Gen Prim := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.boolType (BoolType.tt) => return Prim.boolean (Bool.true) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.boolType (BoolType.ff) => return Prim.boolean (Bool.false) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.intType => do + let i ← Plausible.Arbitrary.arbitrary; + return Prim.int i + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.stringType => do + let s ← Plausible.Arbitrary.arbitrary; + return Prim.stringLit s + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType n => + match v_1 with + | Environment.MkEnvironment (Schema.MkSchema ETS ACTS) R => + match DecOpt.decOpt (DefinedEntity ETS n) initSize with + | Option.some Bool.true => do + let i ← Plausible.Arbitrary.arbitrary; + return Prim.entityUID (EntityUID.MkEntityUID n i) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.boolType (BoolType.tt) => return Prim.boolean (Bool.true) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.boolType (BoolType.ff) => return Prim.boolean (Bool.false) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.intType => do + let i ← Plausible.Arbitrary.arbitrary; + return Prim.int i + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.stringType => do + let s ← Plausible.Arbitrary.arbitrary; + return Prim.stringLit s + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType n => + match v_1 with + | Environment.MkEnvironment (Schema.MkSchema ETS ACTS) R => + match DecOpt.decOpt (DefinedEntity ETS n) initSize with + | Option.some Bool.true => do + let i ← Plausible.Arbitrary.arbitrary; + return Prim.entityUID (EntityUID.MkEntityUID n i) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + ] + fun size => aux_arb size size v_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (p : Prim) => HasTypePrim v p t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat CedarType (fun t_1 => HasTypeVar v_1 x_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (v_1 : Environment) (x_1 : Var) : OptionT Plausible.Gen CedarType := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match x_1 with + | Var.principal => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => return CedarType.entityType P + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.action => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P (EntityUID.MkEntityUID n i) R C) => + return CedarType.entityType n + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.resource => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => return CedarType.entityType R + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.context => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => do + let t_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun t_1 => ReqContextToCedarType C t_1) initSize; + return t_1 + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match x_1 with + | Var.principal => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => return CedarType.entityType P + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.action => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P (EntityUID.MkEntityUID n i) R C) => + return CedarType.entityType n + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.resource => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => return CedarType.entityType R + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match x_1 with + | Var.context => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => do + let t_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun t_1 => ReqContextToCedarType C t_1) initSize; + return t_1 + | _ => OptionT.fail + | _ => OptionT.fail), + ] + fun size => aux_arb size size v_1 x_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (t : CedarType) => HasTypeVar v x t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat Var (fun x_1 => HasTypeVar v_1 x_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (v_1 : Environment) (t_1 : CedarType) : OptionT Plausible.Gen Var := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (BEq.beq u_3 P) initSize with + | Option.some Bool.true => return Var.principal + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P (EntityUID.MkEntityUID n i) R C) => + match DecOpt.decOpt (BEq.beq u_3 n) initSize with + | Option.some Bool.true => return Var.action + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (BEq.beq u_3 R) initSize with + | Option.some Bool.true => return Var.resource + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (ReqContextToCedarType C t_1) initSize with + | Option.some Bool.true => return Var.context + | _ => OptionT.fail + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (BEq.beq u_3 P) initSize with + | Option.some Bool.true => return Var.principal + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P (EntityUID.MkEntityUID n i) R C) => + match DecOpt.decOpt (BEq.beq u_3 n) initSize with + | Option.some Bool.true => return Var.action + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.entityType u_3 => + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (BEq.beq u_3 R) initSize with + | Option.some Bool.true => return Var.resource + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match v_1 with + | Environment.MkEnvironment s (RequestType.MkRequest P A R C) => + match DecOpt.decOpt (ReqContextToCedarType C t_1) initSize with + | Option.some Bool.true => return Var.context + | _ => OptionT.fail + | _ => OptionT.fail), + ] + fun size => aux_arb size size v_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (x : Var) => HasTypeVar v x t) + +/-- +info: Try this checker: instance : DecOpt (BindAttrType ns_1 tef_1 t_1) where + decOpt := + let rec aux_dec (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (tef_1 : CedarType × String × Bool) + (t_1 : CedarType) : Option Bool := + match size with + | Nat.zero => + DecOpt.checkerBacktrack + [fun _ => + match tef_1 with + | Prod.mk (CedarType.recordTypeCons x b t r) (Prod.mk u_3 u_4) => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 x) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq t t_1) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_4 b) initSize, DecOpt.decOpt (WfRecordType ns_1 r) initSize]]] + | _ => Option.some Bool.false] + | Nat.succ size' => + DecOpt.checkerBacktrack + [fun _ => + match tef_1 with + | Prod.mk (CedarType.recordTypeCons x b t r) (Prod.mk u_3 u_4) => + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_3 x) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq t t_1) initSize, + DecOpt.andOptList + [DecOpt.decOpt (BEq.beq u_4 b) initSize, DecOpt.decOpt (WfRecordType ns_1 r) initSize]]] + | _ => Option.some Bool.false, + fun _ => + match tef_1 with + | Prod.mk (CedarType.recordTypeCons y i t r) (Prod.mk x b) => + DecOpt.andOptList + [DecOpt.decOpt (Eq (bne x y) (Bool.true)) initSize, + DecOpt.andOptList + [DecOpt.decOpt (WfRecordType ns_1 r) initSize, + aux_dec initSize size' ns_1 (Prod.mk r (Prod.mk x b)) t_1]] + | _ => Option.some Bool.false] + fun size => aux_dec size size ns_1 tef_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_checker (BindAttrType ns tef t) + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (CedarType × String × Bool) (fun tef_1 => BindAttrType ns_1 tef_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (ns_1 : List EntityName) (t_1 : CedarType) : + OptionT Plausible.Gen (CedarType × String × Bool) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, do + let r ← ArbitrarySizedSuchThat.arbitrarySizedST (fun r => WfRecordType ns_1 r) initSize; + do + let b ← Plausible.Arbitrary.arbitrary; + do + let x ← Plausible.Arbitrary.arbitrary; + return Prod.mk (CedarType.recordTypeCons x b t_1 r) (Prod.mk x b))] + | Nat.succ size' => + OptionTGen.backtrack + [(1, do + let r ← ArbitrarySizedSuchThat.arbitrarySizedST (fun r => WfRecordType ns_1 r) initSize; + do + let b ← Plausible.Arbitrary.arbitrary; + do + let x ← Plausible.Arbitrary.arbitrary; + return Prod.mk (CedarType.recordTypeCons x b t_1 r) (Prod.mk x b)), + (Nat.succ size', do + let vr_x_b ← aux_arb initSize size' ns_1 t_1; + match vr_x_b with + | Prod.mk r (Prod.mk x b) => + match DecOpt.decOpt (WfRecordType ns_1 r) initSize with + | Option.some Bool.true => do + let i ← Plausible.Arbitrary.arbitrary; + do + let t ← Plausible.Arbitrary.arbitrary; + do + let y ← Plausible.Arbitrary.arbitrary; + match DecOpt.decOpt (Eq (bne x y) (Bool.true)) initSize with + | Option.some Bool.true => return Prod.mk (CedarType.recordTypeCons y i t r) (Prod.mk x b) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size ns_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (tef : (CedarType × String × Bool)) => BindAttrType ns tef t) + + +------------------------------------------------------------ +-- Generator for well-typed Cedar expressions +------------------------------------------------------------ + +/-- +info: Try this generator: instance : ArbitrarySizedSuchThat (CedarExpr × PathSet) (fun ex_1 => HasType a_1 v_1 ex_1 t_1) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) (a_1 : PathSet) (v_1 : Environment) (t_1 : CedarType) : + OptionT Plausible.Gen (CedarExpr × PathSet) := + match size with + | Nat.zero => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.boolType (BoolType.ff) => do + let P ← + ArbitrarySizedSuchThat.arbitrarySizedST + (fun P => HasTypePrim v_1 P (CedarType.boolType (BoolType.ff))) initSize; + return Prod.mk (CedarExpr.lit P) (PathSet.allpaths) + | _ => OptionT.fail), + (1, + match DecOpt.decOpt (Eq (bne t_1 (CedarType.boolType (BoolType.ff))) (Bool.true)) initSize with + | Option.some Bool.true => do + let P ← ArbitrarySizedSuchThat.arbitrarySizedST (fun P => HasTypePrim v_1 P t_1) initSize; + return Prod.mk (CedarExpr.lit P) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail), + (1, do + let X ← ArbitrarySizedSuchThat.arbitrarySizedST (fun X => HasTypeVar v_1 X t_1) initSize; + return Prod.mk (CedarExpr.var X) (PathSet.somepaths (List.nil))), + (1, + match t_1 with + | CedarType.boolType (BoolType.tt) => do + let P ← Plausible.Arbitrary.arbitrary; + return + Prod.mk (CedarExpr.binaryApp (BinaryOp.equals) (CedarExpr.lit P) (CedarExpr.lit P)) + (PathSet.somepaths (List.nil)) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.boolType (BoolType.ff) => do + let P1 ← Plausible.Arbitrary.arbitrary; + do + let P2 ← Plausible.Arbitrary.arbitrary; + match DecOpt.decOpt (Eq (bne P1 P2) (Bool.true)) initSize with + | Option.some Bool.true => + return + Prod.mk (CedarExpr.binaryApp (BinaryOp.equals) (CedarExpr.lit P1) (CedarExpr.lit P2)) + (PathSet.allpaths) + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.recordTypeNil => return Prod.mk (CedarExpr.recExprNil) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail)] + | Nat.succ size' => + OptionTGen.backtrack + [(1, + match t_1 with + | CedarType.boolType (BoolType.ff) => do + let P ← + ArbitrarySizedSuchThat.arbitrarySizedST + (fun P => HasTypePrim v_1 P (CedarType.boolType (BoolType.ff))) initSize; + return Prod.mk (CedarExpr.lit P) (PathSet.allpaths) + | _ => OptionT.fail), + (1, + match DecOpt.decOpt (Eq (bne t_1 (CedarType.boolType (BoolType.ff))) (Bool.true)) initSize with + | Option.some Bool.true => do + let P ← ArbitrarySizedSuchThat.arbitrarySizedST (fun P => HasTypePrim v_1 P t_1) initSize; + return Prod.mk (CedarExpr.lit P) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail), + (1, do + let X ← ArbitrarySizedSuchThat.arbitrarySizedST (fun X => HasTypeVar v_1 X t_1) initSize; + return Prod.mk (CedarExpr.var X) (PathSet.somepaths (List.nil))), + (1, + match t_1 with + | CedarType.boolType (BoolType.tt) => do + let P ← Plausible.Arbitrary.arbitrary; + return + Prod.mk (CedarExpr.binaryApp (BinaryOp.equals) (CedarExpr.lit P) (CedarExpr.lit P)) + (PathSet.somepaths (List.nil)) + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.boolType (BoolType.ff) => do + let P1 ← Plausible.Arbitrary.arbitrary; + do + let P2 ← Plausible.Arbitrary.arbitrary; + match DecOpt.decOpt (Eq (bne P1 P2) (Bool.true)) initSize with + | Option.some Bool.true => + return + Prod.mk (CedarExpr.binaryApp (BinaryOp.equals) (CedarExpr.lit P1) (CedarExpr.lit P2)) + (PathSet.allpaths) + | _ => OptionT.fail + | _ => OptionT.fail), + (1, + match t_1 with + | CedarType.recordTypeNil => return Prod.mk (CedarExpr.recExprNil) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail), + (Nat.succ size', do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.boolType (BoolType.tt)); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' (mergeExprs a_1 x1) v_1 t_1; + match vE2_x2 with + | Prod.mk E2 x2 => do + let E3 ← Plausible.Arbitrary.arbitrary; + return Prod.mk (CedarExpr.ite E1 E2 E3) (mergeExprs x1 x2) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.boolType (BoolType.ff)); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE3_x3 ← aux_arb initSize size' a_1 v_1 t_1; + match vE3_x3 with + | Prod.mk E3 x3 => do + let E2 ← Plausible.Arbitrary.arbitrary; + return Prod.mk (CedarExpr.ite E1 E2 E3) x3 + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', do + let vE1_E2_x ← aux_arb initSize size' a_1 v_1 t_1; + match vE1_E2_x with + | Prod.mk (CedarExpr.ite E1 E2 (CedarExpr.lit (Prim.boolean (Bool.false)))) x => + return Prod.mk (CedarExpr.andExpr E1 E2) x + | _ => OptionT.fail), + (Nat.succ size', do + let vE1_E2_x ← aux_arb initSize size' a_1 v_1 t_1; + match vE1_E2_x with + | Prod.mk (CedarExpr.ite E1 (CedarExpr.lit (Prim.boolean (Bool.true))) E2) x => + return Prod.mk (CedarExpr.orExpr E1 E2) x + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.anyBool) => do + let ve_x ← aux_arb initSize size' a_1 v_1 (CedarType.boolType (BoolType.anyBool)); + match ve_x with + | Prod.mk e x => return Prod.mk (CedarExpr.unaryApp (UnaryOp.not) e) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.ff) => do + let ve_x ← aux_arb initSize size' a_1 v_1 (CedarType.boolType (BoolType.tt)); + match ve_x with + | Prod.mk e x => return Prod.mk (CedarExpr.unaryApp (UnaryOp.not) e) (PathSet.allpaths) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.tt) => do + let ve_x ← aux_arb initSize size' a_1 v_1 (CedarType.boolType (BoolType.ff)); + match ve_x with + | Prod.mk e x => return Prod.mk (CedarExpr.unaryApp (UnaryOp.not) e) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.intType => do + let ve_x ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match ve_x with + | Prod.mk e x => return Prod.mk (CedarExpr.unaryApp (UnaryOp.neg) e) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.anyBool) => do + let ve_x ← aux_arb initSize size' a_1 v_1 (CedarType.stringType); + match ve_x with + | Prod.mk e x => do + let P ← Plausible.Arbitrary.arbitrary; + return Prod.mk (CedarExpr.unaryApp (UnaryOp.like P) e) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.anyBool) => do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE2_x2 with + | Prod.mk E2 x2 => + return Prod.mk (CedarExpr.binaryApp (BinaryOp.less) E1 E2) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.boolType (BoolType.anyBool) => do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE2_x2 with + | Prod.mk E2 x2 => + return Prod.mk (CedarExpr.binaryApp (BinaryOp.lessEq) E1 E2) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.intType => do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE2_x2 with + | Prod.mk E2 x2 => + return Prod.mk (CedarExpr.binaryApp (BinaryOp.add) E1 E2) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.intType => do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE2_x2 with + | Prod.mk E2 x2 => + return Prod.mk (CedarExpr.binaryApp (BinaryOp.sub) E1 E2) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.intType => do + let vE1_x1 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE1_x1 with + | Prod.mk E1 x1 => do + let vE2_x2 ← aux_arb initSize size' a_1 v_1 (CedarType.intType); + match vE2_x2 with + | Prod.mk E2 x2 => + return Prod.mk (CedarExpr.binaryApp (BinaryOp.mul) E1 E2) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.recordTypeCons i b T TR => + match DecOpt.decOpt (RecordType TR) initSize with + | Option.some Bool.true => do + let ve_x ← aux_arb initSize size' a_1 v_1 T; + match ve_x with + | Prod.mk e x => do + let vR_rx ← aux_arb initSize size' a_1 v_1 TR; + match vR_rx with + | Prod.mk R rx => return Prod.mk (CedarExpr.recExprCons i e R) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.setType T => do + let ve_x ← aux_arb initSize size' a_1 v_1 T; + match ve_x with + | Prod.mk e x => + return Prod.mk (CedarExpr.setExprCons e (CedarExpr.setExprNil)) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail), + (Nat.succ size', + match t_1 with + | CedarType.setType T => do + let ve_x ← aux_arb initSize size' a_1 v_1 T; + match ve_x with + | Prod.mk e x => do + let vR_rx ← aux_arb initSize size' a_1 v_1 (CedarType.setType T); + match vR_rx with + | Prod.mk R rx => return Prod.mk (CedarExpr.setExprCons e R) (PathSet.somepaths (List.nil)) + | _ => OptionT.fail + | _ => OptionT.fail + | _ => OptionT.fail)] + fun size => aux_arb size size a_1 v_1 t_1 +-/ +#guard_msgs(info, drop warning) in +#derive_generator (fun (ex : (CedarExpr × PathSet)) => HasType a v ex t) diff --git a/Test/CedarExample/CedarWellTypedTermGenerator.lean b/Test/CedarExample/CedarWellTypedTermGenerator.lean new file mode 100644 index 00000000..f8692436 --- /dev/null +++ b/Test/CedarExample/CedarWellTypedTermGenerator.lean @@ -0,0 +1,106 @@ +import Test.CedarExample.Cedar +import Test.CedarExample.CedarCheckerGenerators +import Plausible.Chamelean.OptionTGen +import Plausible.Gen + +open Plausible +open OptionTGen + + +/-! +This file invokes the generator for well-typed Cedar terms, defined in `Test/CedarExample.CedarCheckerGenerators.lean`. + +Note: the structure of this file closely follows Mike Hicks's Coq formalization of Cedar (not publicly available). +-/ + +/-- Schema based on one of Cedar's sample apps -/ +def schema : Schema := + -- entity types + let team := EntityName.MkName "Team" [] + let teamDef := EntitySchemaEntry.MkEntitySchemaEntry [team] [] + let user := EntityName.MkName "User" [] + let userDef := EntitySchemaEntry.MkEntitySchemaEntry [team] [("manager", true, CedarType.entityType user)] + let lst := EntityName.MkName "List" [] + let lstDef := EntitySchemaEntry.MkEntitySchemaEntry [] [ + ("owner", true, CedarType.entityType user), + ("readers", true, CedarType.entityType team), + ("editors", true, CedarType.entityType team), + ("age", true, CedarType.intType), + ("description", true, CedarType.stringType)] + let app := EntityName.MkName "Application" [] + let appDef := EntitySchemaEntry.MkEntitySchemaEntry [] [] + let action := EntityName.MkName "Action" [] + let actionDef := EntitySchemaEntry.MkEntitySchemaEntry [action] [] + let ets := [ + (user, userDef), + (team, teamDef), + (lst, lstDef), + (app, appDef), + (action, actionDef)] + -- action defs + let getAct := ActionSchemaEntry.MkActionSchemaEntry [user] [lst] [] + let createAct := ActionSchemaEntry.MkActionSchemaEntry [user] [app] [] + let updateAct := ActionSchemaEntry.MkActionSchemaEntry [user] [lst] [] + let acts := [ + ((EntityUID.MkEntityUID action "getList"), getAct), + ((EntityUID.MkEntityUID action "createList"), createAct), + ((EntityUID.MkEntityUID action "updateList"), updateAct)] + Schema.MkSchema ets acts + +/-- A generator for well-typed Cedar expressions, using the derived generators for `RequestTypes`, environments and expressions -/ +def genCedarExpr (fuel : Nat) : OptionT Gen CedarExpr := + match schema with + | .MkSchema ets acts => do + -- Generates `RequestTypes` based on the schema + let reqs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun rs => ActionSchemaToRequestTypes acts [] rs) fuel + -- Generate a list of environments `envs` + let envs ← ArbitrarySizedSuchThat.arbitrarySizedST (fun es => SchemaToEnvironments (.MkSchema ets acts) reqs es) fuel + match envs with + | v :: _ => do + -- Generate a well-typed expression from the first environment `v` in `es` + let (expr, _) ← ArbitrarySizedSuchThat.arbitrarySizedST (fun e => HasType (.somepaths []) v e (.boolType .anyBool)) fuel + return expr + | [] => OptionT.fail + +/- Below are some Cedar expressions that are produced by the generator above. +Note that these are *not* well-typed Cedar expressions, because we commented out 18 out of the 41 typing rules in `HasType` +as Chamelean took too long to derive the generators for those cases -- see `Test/CedarExample/Cedar.lean` for more details. + +``` +6 < (5 - 1) + +if (if true then John::"John" == John::"John" else action) then + Hicks like "" +else + nil + +if false then + { Mike: action }nil +else + Aaron like "" + +if (if A::Kesha::"D" == Aaron then nil else Hicks == Hicks) then + Mike like "" +else + { Hicks: if {} then nil else nil }{ D: Hicks }nil + +1 <= if false then + { B: B < true }{ B: action || principal }(2).B +else + 3 + +(0 - 0) < (0 * 3) + +if John::Kesha::Hicks::Hicks::Hicks::Hicks::A::"D" == 0 then + { D: action }if (nil::-1)::{ Hicks: nil }context.A then + resource + else + nil && action has John +else + -1 <= -3 +``` + +-/ + +-- Uncomment this line to see the output from the generator for Cedar expressions +-- #eval runSizedGenPrintOutput genCedarExpr 2 diff --git a/Test/DeriveArbitrary/DeriveNKIValueGenerator.lean b/Test/DeriveArbitrary/DeriveNKIValueGenerator.lean index d20a7169..970d43bc 100644 --- a/Test/DeriveArbitrary/DeriveNKIValueGenerator.lean +++ b/Test/DeriveArbitrary/DeriveNKIValueGenerator.lean @@ -9,7 +9,7 @@ set_option guard_msgs.diff true /-- A datatype representing values in the NKI language, adapted from https://github.com/leanprover/KLR/blob/main/KLR/NKI/Basic.lean -/ -inductive Value where +inductive NKIValue where | none | bool (value : Bool) | int (value : Int) @@ -22,70 +22,70 @@ set_option trace.plausible.deriving.arbitrary true in /-- trace: [plausible.deriving.arbitrary] ⏎ [mutual - def arbitraryValue✝ : Nat → Plausible.Gen (@Value✝) := - let rec aux_arb (fuel✝ : Nat) : Plausible.Gen (@Value✝) := + def arbitraryNKIValue✝ : Nat → Plausible.Gen (@NKIValue✝) := + let rec aux_arb (fuel✝ : Nat) : Plausible.Gen (@NKIValue✝) := match fuel✝ with | Nat.zero => - Plausible.Gen.oneOfWithDefault (pure Value.none) - [(pure Value.none), + Plausible.Gen.oneOfWithDefault (pure NKIValue.none) + [(pure NKIValue.none), (do let a✝ ← Plausible.Arbitrary.arbitrary - return Value.bool a✝), + return NKIValue.bool a✝), (do let a✝¹ ← Plausible.Arbitrary.arbitrary - return Value.int a✝¹), + return NKIValue.int a✝¹), (do let a✝² ← Plausible.Arbitrary.arbitrary - return Value.string a✝²), - (pure Value.ellipsis), + return NKIValue.string a✝²), + (pure NKIValue.ellipsis), (do let a✝³ ← Plausible.Arbitrary.arbitrary let a✝⁴ ← Plausible.Arbitrary.arbitrary - return Value.tensor a✝³ a✝⁴)] + return NKIValue.tensor a✝³ a✝⁴)] | fuel'✝ + 1 => - Plausible.Gen.frequency (pure Value.none) - [(1, (pure Value.none)), + Plausible.Gen.frequency (pure NKIValue.none) + [(1, (pure NKIValue.none)), (1, (do let a✝ ← Plausible.Arbitrary.arbitrary - return Value.bool a✝)), + return NKIValue.bool a✝)), (1, (do let a✝¹ ← Plausible.Arbitrary.arbitrary - return Value.int a✝¹)), + return NKIValue.int a✝¹)), (1, (do let a✝² ← Plausible.Arbitrary.arbitrary - return Value.string a✝²)), - (1, (pure Value.ellipsis)), + return NKIValue.string a✝²)), + (1, (pure NKIValue.ellipsis)), (1, (do let a✝³ ← Plausible.Arbitrary.arbitrary let a✝⁴ ← Plausible.Arbitrary.arbitrary - return Value.tensor a✝³ a✝⁴)), + return NKIValue.tensor a✝³ a✝⁴)), ] fun fuel✝ => aux_arb fuel✝ end, - instance : Plausible.ArbitraryFueled✝ (@Value✝) := - ⟨arbitraryValue✝⟩] + instance : Plausible.ArbitraryFueled✝ (@NKIValue✝) := + ⟨arbitraryNKIValue✝⟩] -/ #guard_msgs in -deriving instance Arbitrary for Value +deriving instance Arbitrary for NKIValue -- Test that we can successfully synthesize instances of `Arbitrary` & `ArbitraryFueled` -/-- info: instArbitraryFueledValue -/ +/-- info: instArbitraryFueledNKIValue -/ #guard_msgs in -#synth ArbitraryFueled Value +#synth ArbitraryFueled NKIValue /-- info: instArbitraryOfArbitraryFueled -/ #guard_msgs in -#synth Arbitrary Value +#synth Arbitrary NKIValue -/-- `Shrinkable` instance for `Value`s which recursively +/-- `Shrinkable` instance for `NKIValue`s which recursively shrinks each argument to a constructor -/ -instance : Shrinkable Value where - shrink (v : Value) := +instance : Shrinkable NKIValue where + shrink (v : NKIValue) := match v with | .none | .ellipsis => [] | .bool b => .bool <$> Shrinkable.shrink b @@ -96,21 +96,21 @@ instance : Shrinkable Value where let shrunkenDtypes := Shrinkable.shrink dtype (Function.uncurry .tensor) <$> List.zip shrunkenShapes shrunkenDtypes -/-- `SampleableExt` instance for `Value` -/ -instance : SampleableExt Value := +/-- `SampleableExt` instance for `NKIValue` -/ +instance : SampleableExt NKIValue := SampleableExt.mkSelfContained Arbitrary.arbitrary -- To test whether the derived generator can generate counterexamples, --- we state an (erroneous) property that states that all `Value`s are `Bool`s +-- we state an (erroneous) property that states that all `NKIValue`s are `Bool`s -- and see if the generator can refute this property. -/-- Determines whether a `Value` is a `Bool` -/ -def isBool (v : Value) : Bool := +/-- Determines whether a `NKIValue` is a `Bool` -/ +def isBool (v : NKIValue) : Bool := match v with | .bool _ => true | _ => false /-- error: Found a counter-example! -/ #guard_msgs in -#eval Testable.check (∀ v : Value, isBool v) +#eval Testable.check (∀ v : NKIValue, isBool v) (cfg := {numInst := 10, maxSize := 5, quiet := true}) diff --git a/Test/DeriveEnum/DeriveNKIValueEnumerator.lean b/Test/DeriveEnum/DeriveNKIValueEnumerator.lean index f48fbd35..d9503e50 100644 --- a/Test/DeriveEnum/DeriveNKIValueEnumerator.lean +++ b/Test/DeriveEnum/DeriveNKIValueEnumerator.lean @@ -3,56 +3,56 @@ import Plausible.Chamelean.EnumeratorCombinators import Plausible.Chamelean.DeriveEnum import Test.DeriveArbitrary.DeriveNKIValueGenerator -deriving instance Enum for Value +deriving instance Enum for NKIValue set_option guard_msgs.diff true -- Test that we can successfully synthesize instances of `Arbitrary` & `ArbitrarySized` -/-- info: instEnumSizedValue -/ +/-- info: instEnumSizedNKIValue -/ #guard_msgs in -#synth EnumSized Value +#synth EnumSized NKIValue /-- info: instEnumOfEnumSized -/ #guard_msgs in -#synth Enum Value +#synth Enum NKIValue -- We test the command elaborator frontend in a separate namespace to -- avoid overlapping typeclass instances for the same type namespace CommandElaboratorTest /-- -info: Try this enumerator: instance : EnumSized Value where +info: Try this enumerator: instance : EnumSized NKIValue where enumSized := - let rec aux_enum (size : Nat) : Enumerator Value := + let rec aux_enum (size : Nat) : Enumerator NKIValue := match size with | Nat.zero => - EnumeratorCombinators.oneOfWithDefault (pure Value.none) - [pure Value.none, do + EnumeratorCombinators.oneOfWithDefault (pure NKIValue.none) + [pure NKIValue.none, do let value_0 ← Enum.enum - return Value.bool value_0, do + return NKIValue.bool value_0, do let value_0 ← Enum.enum - return Value.int value_0, do + return NKIValue.int value_0, do let value_0 ← Enum.enum - return Value.string value_0, pure Value.ellipsis, do + return NKIValue.string value_0, pure NKIValue.ellipsis, do let shape_0 ← Enum.enum let dtype_0 ← Enum.enum - return Value.tensor shape_0 dtype_0] + return NKIValue.tensor shape_0 dtype_0] | Nat.succ size' => - EnumeratorCombinators.oneOfWithDefault (pure Value.none) - [pure Value.none, do + EnumeratorCombinators.oneOfWithDefault (pure NKIValue.none) + [pure NKIValue.none, do let value_0 ← Enum.enum - return Value.bool value_0, do + return NKIValue.bool value_0, do let value_0 ← Enum.enum - return Value.int value_0, do + return NKIValue.int value_0, do let value_0 ← Enum.enum - return Value.string value_0, pure Value.ellipsis, do + return NKIValue.string value_0, pure NKIValue.ellipsis, do let shape_0 ← Enum.enum let dtype_0 ← Enum.enum - return Value.tensor shape_0 dtype_0, ] + return NKIValue.tensor shape_0 dtype_0, ] fun size => aux_enum size -/ #guard_msgs(info, drop warning) in -#derive_enum Value +#derive_enum NKIValue end CommandElaboratorTest diff --git a/Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean b/Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean index 64739053..1295095f 100644 --- a/Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean +++ b/Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean @@ -18,7 +18,7 @@ set_option match.ignoreUnusedAlts true /-- We override the default `Arbitrary` for `String`s so that we only produce strings of length 1 where the string is a single letter from `A` to `I` -/ -instance : Arbitrary String where +instance instKeyValueStoreArbitraryString : Arbitrary String where arbitrary := GeneratorCombinators.elementsWithDefault "A" ["A", "B", "C", "D", "E", "F", "G", "H", "I"] --------------------------------------------------------------------------------------------------------------------------------------- diff --git a/scripts/nolints.json b/scripts/nolints.json index f093fb28..57286e9c 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -112,20 +112,6 @@ ["docBlame", "instEnumSizedSuchThatTypeLookup.aux_enum"], ["docBlame", "instEnumSizedType.aux_enum"], ["docBlame", "instEnumSizedTerm.aux_enum"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringRemoveKV.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringRemoveKV_1.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringAddKV.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringAddKV_1.aux_arb"], - ["docBlame", "instDecOptLookupKV.aux_dec"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringLookupKV.aux_arb"], - ["docBlame", "instDecOptAddKV.aux_dec"], - ["docBlame", "instArbitrarySizedSuchThatListProdStringEvalStateApiCall.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatStringAddKV.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatProdStateResultStringNatLookupKV.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatProdNatListStringGetBucket.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatProdStateAPICallStateResultListStringEvalStateApiCall.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatProdAPICallResultNatListStringEvalApiCall.aux_arb"], - ["docBlame", "instArbitrarySizedSuchThatProdListAPICallResultNatStringEvalApiCalls.aux_arb"], ["unusedArguments", "genTyping.aux_arb"], ["unusedArguments", "genBST.aux_arb"], ["unusedArguments", "genBalancedTree.aux_arb"], @@ -135,7 +121,6 @@ ["unusedArguments", "Plausible.RandT.down"], ["unusedArguments", "Plausible.NamedBinder"], ["unusedArguments", "Plausible.Decorations.DecorationsOf"], - ["unusedArguments", "instArbitrarySizedSuchThatListProdStringAddKV_1.aux_arb"], ["unusedArguments", "instArbitrarySizedSuchThatEqOfBEq"], ["unusedArguments", "instEnumSizedSuchThatEqOfBEq"], ["unusedArguments", "instArbitrarySizedSuchThatEqOfBEq_1"],