From 7ca8e8fdefbb86afcca0fbed3c49dc72090492b7 Mon Sep 17 00:00:00 2001 From: Craig Disselkoen Date: Wed, 20 Mar 2024 09:42:06 -0700 Subject: [PATCH] Cherry-pick #260 to 3.1.x: update for cedar#702 (RFC 57) (#261) Signed-off-by: Craig Disselkoen --- cedar | 2 +- cedar-lean/Cedar/Spec/Evaluator.lean | 16 +++--- cedar-lean/Cedar/Spec/Expr.lean | 2 +- .../Thm/Validation/Typechecker/BinaryApp.lean | 17 ++++--- .../Thm/Validation/Typechecker/UnaryApp.lean | 50 +------------------ cedar-lean/Cedar/Validation/Typechecker.lean | 2 +- cedar-lean/DiffTest/Parser.lean | 5 +- cedar-policy-generators/src/expr.rs | 28 +++++------ 8 files changed, 37 insertions(+), 85 deletions(-) diff --git a/cedar b/cedar index b16c9814e..c98b008d4 160000 --- a/cedar +++ b/cedar @@ -1 +1 @@ -Subproject commit b16c9814e2a51cd1612ebbfbd8ac01812bdffb18 +Subproject commit c98b008d43f069001dca269adb3db7e22a729a84 diff --git a/cedar-lean/Cedar/Spec/Evaluator.lean b/cedar-lean/Cedar/Spec/Evaluator.lean index 348379260..52adb56d2 100644 --- a/cedar-lean/Cedar/Spec/Evaluator.lean +++ b/cedar-lean/Cedar/Spec/Evaluator.lean @@ -33,10 +33,9 @@ def intOrErr : Option Int64 → Result Value def apply₁ : UnaryOp → Value → Result Value | .not, .prim (.bool b) => ok !b | .neg, .prim (.int i) => intOrErr i.neg? - | .mulBy c, .prim (.int i) => intOrErr (c.mul? i) - | .like p, .prim (.string s) => ok (wildcardMatch s p) - | .is ety, .prim (.entityUID uid) => ok (ety == uid.ty) - | _, _ => error .typeError + | .like p, .prim (.string s) => .ok (wildcardMatch s p) + | .is ety, .prim (.entityUID uid) => .ok (ety == uid.ty) + | _, _ => .error .typeError def inₑ (uid₁ uid₂ : EntityUID) (es : Entities) : Bool := uid₁ == uid₂ || (es.ancestorsOrEmpty uid₁).contains uid₂ @@ -52,10 +51,11 @@ def apply₂ (op₂ : BinaryOp) (v₁ v₂ : Value) (es : Entities) : Result Val | .lessEq, .prim (.int i), .prim (.int j) => ok ((i ≤ j): Bool) | .add, .prim (.int i), .prim (.int j) => intOrErr (i.add? j) | .sub, .prim (.int i), .prim (.int j) => intOrErr (i.sub? j) - | .contains, .set vs₁, _ => ok (vs₁.contains v₂) - | .containsAll, .set vs₁, .set vs₂ => ok (vs₂.subset vs₁) - | .containsAny, .set vs₁, .set vs₂ => ok (vs₁.intersects vs₂) - | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) => ok (inₑ uid₁ uid₂ es) + | .mul, .prim (.int i), .prim (.int j) => intOrErr (i.mul? j) + | .contains, .set vs₁, _ => .ok (vs₁.contains v₂) + | .containsAll, .set vs₁, .set vs₂ => .ok (vs₂.subset vs₁) + | .containsAny, .set vs₁, .set vs₂ => .ok (vs₁.intersects vs₂) + | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) => .ok (inₑ uid₁ uid₂ es) | .mem, .prim (.entityUID uid₁), .set (vs) => inₛ uid₁ vs es | _, _, _ => error .typeError diff --git a/cedar-lean/Cedar/Spec/Expr.lean b/cedar-lean/Cedar/Spec/Expr.lean index 026479d64..aa93de4f0 100644 --- a/cedar-lean/Cedar/Spec/Expr.lean +++ b/cedar-lean/Cedar/Spec/Expr.lean @@ -35,7 +35,6 @@ inductive Var where inductive UnaryOp where | not | neg - | mulBy (i : Int64) | like (p : Pattern) | is (ety : EntityType) @@ -46,6 +45,7 @@ inductive BinaryOp where | lessEq | add | sub + | mul | contains | containsAll | containsAny diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean index 2414b8bfb..e585feaad 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean @@ -214,7 +214,7 @@ theorem type_of_int_cmp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c } theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : CedarType} - (h₁ : op₂ = .add ∨ op₂ = .sub) + (h₁ : op₂ = .add ∨ op₂ = .sub ∨ op₂ = .mul) (h₂ : typeOf (Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (ty, c')) : c' = ∅ ∧ ty = .int ∧ @@ -224,7 +224,7 @@ theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' simp [typeOf] at * cases h₃ : typeOf x₁ c env <;> simp [h₃] at h₂ cases h₄ : typeOf x₂ c env <;> simp [h₄] at h₂ - rcases h₁ with h₁ | h₁ + rcases h₁ with h₁ | h₁ | h₁ all_goals { subst h₁ simp [typeOfBinaryApp, err, ok] at h₂ @@ -238,7 +238,7 @@ theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' } theorem type_of_int_arith_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities} - (h₀ : op₂ = .add ∨ op₂ = .sub) + (h₀ : op₂ = .add ∨ op₂ = .sub ∨ op₂ = .mul) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) (h₃ : typeOf (Expr.binaryApp op₂ x₁ x₂) c₁ env = Except.ok (ty, c₂)) @@ -266,15 +266,19 @@ theorem type_of_int_arith_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c have ⟨i₁, ih₁⟩ := instance_of_int_is_int ih₃ have ⟨i₂, ih₂⟩ := instance_of_int_is_int ih₄ subst ih₁ ih₂ - rcases h₀ with h₀ | h₀ <;> subst h₀ <;> simp [apply₂, intOrErr] + rcases h₀ with h₀ | h₀ | h₀ <;> subst h₀ <;> simp [apply₂, intOrErr] case inl => cases h₄ : Int64.add? i₁ i₂ <;> simp [h₄] case none => exact type_is_inhabited CedarType.int case some => simp [InstanceOfType.instance_of_int] - case inr => + case inr.inl => cases h₄ : Int64.sub? i₁ i₂ <;> simp [h₄] case none => exact type_is_inhabited CedarType.int case some => simp [InstanceOfType.instance_of_int] + case inr.inr => + cases h₄ : Int64.mul? i₁ i₂ <;> simp [h₄] + case none => exact type_is_inhabited CedarType.int + case some => simp [InstanceOfType.instance_of_int] theorem type_of_contains_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : CedarType} (h₁ : typeOf (Expr.binaryApp .contains x₁ x₂) c env = Except.ok (ty, c')) : @@ -838,7 +842,8 @@ theorem type_of_binaryApp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c | .less | .lessEq => exact type_of_int_cmp_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂ | .add - | .sub => exact type_of_int_arith_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂ + | .sub + | .mul => exact type_of_int_arith_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂ | .contains => exact type_of_contains_is_sound h₁ h₂ h₃ ih₁ ih₂ | .containsAll | .containsAny => exact type_of_containsA_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean index 0a4e3c0f5..dbdc8d25e 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean @@ -133,53 +133,6 @@ theorem type_of_neg_is_sound {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Env exact type_is_inhabited CedarType.int } -theorem type_of_mulBy_inversion {x₁ : Expr} {k : Int64} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} - (h₁ : typeOf (Expr.unaryApp (.mulBy k) x₁) c₁ env = Except.ok (ty, c₂)) : - c₂ = ∅ ∧ - ty = .int ∧ - ∃ c₁', typeOf x₁ c₁ env = Except.ok (.int, c₁') -:= by - simp [typeOf] at h₁ - cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁ - case ok res => - have ⟨ty₁, c₁'⟩ := res - simp [typeOfUnaryApp] at h₁ - split at h₁ <;> try contradiction - simp [ok] at h₁ - simp [h₁] - -theorem type_of_mulBy_is_sound {x₁ : Expr} {k : Int64} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities} - (h₁ : CapabilitiesInvariant c₁ request entities) - (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : typeOf (Expr.unaryApp (.mulBy k) x₁) c₁ env = Except.ok (ty, c₂)) - (ih : TypeOfIsSound x₁) : - GuardedCapabilitiesInvariant (Expr.unaryApp (.mulBy k) x₁) c₂ request entities ∧ - ∃ v, EvaluatesTo (Expr.unaryApp (.mulBy k) x₁) request entities v ∧ InstanceOfType v ty -:= by - have ⟨h₅, h₆, c₁', h₄⟩ := type_of_mulBy_inversion h₃ - subst h₅; subst h₆ - apply And.intro - case left => exact empty_guarded_capabilities_invariant - case right => - have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ -- IH - simp [EvaluatesTo] at h₆ - simp [EvaluatesTo, evaluate] - rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆] - case inr.inr.inr => - have ⟨i, h₈⟩ := instance_of_int_is_int h₇ - subst h₈ - simp [apply₁, intOrErr] - cases h₉ : k.mul? i - case none => - simp only [or_false, or_true, true_and] - exact type_is_inhabited CedarType.int - case some i' => - simp only [Except.ok.injEq, false_or, exists_eq_left'] - apply InstanceOfType.instance_of_int - all_goals { - exact type_is_inhabited CedarType.int - } - theorem type_of_like_inversion {x₁ : Expr} {p : Pattern} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} (h₁ : typeOf (Expr.unaryApp (.like p) x₁) c₁ env = Except.ok (ty, c₂)) : c₂ = ∅ ∧ @@ -234,7 +187,7 @@ theorem type_of_is_inversion {x₁ : Expr} {ety : EntityType} {c₁ c₂ : Capab have ⟨ty₁, c₁'⟩ := res simp [typeOfUnaryApp] at h₁ split at h₁ <;> try contradiction - case h_5 _ _ ety' h₃ => + case h_4 _ _ ety' h₃ => simp only [UnaryOp.is.injEq] at h₃ subst h₃ simp [ok] at h₁ @@ -284,7 +237,6 @@ theorem type_of_unaryApp_is_sound {op₁ : UnaryOp} {x₁ : Expr} {c₁ c₂ : C match op₁ with | .not => exact type_of_not_is_sound h₁ h₂ h₃ ih | .neg => exact type_of_neg_is_sound h₁ h₂ h₃ ih - | .mulBy k => exact type_of_mulBy_is_sound h₁ h₂ h₃ ih | .like p => exact type_of_like_is_sound h₁ h₂ h₃ ih | .is ety => exact type_of_is_is_sound h₁ h₂ h₃ ih diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index 000daaee7..b70deafd0 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -106,7 +106,6 @@ def typeOfUnaryApp (op : UnaryOp) (ty : CedarType) : ResultType := match op, ty with | .not, .bool x => ok (.bool x.not) | .neg, .int => ok .int - | .mulBy _, .int => ok .int | .like _, .string => ok (.bool .anyBool) | .is ety₁, .entity ety₂ => ok (.bool (if ety₁ = ety₂ then .tt else .ff)) | _, _ => err (.unexpectedType ty) @@ -172,6 +171,7 @@ def typeOfBinaryApp (op₂ : BinaryOp) (ty₁ ty₂ : CedarType) (x₁ x₂ : Ex | .lessEq, .int, .int => ok (.bool .anyBool) | .add, .int, .int => ok .int | .sub, .int, .int => ok .int + | .mul, .int, .int => ok .int | .contains, .set ty₃, _ => ifLubThenBool ty₂ ty₃ | .containsAll, .set ty₃, .set ty₄ => ifLubThenBool ty₃ ty₄ | .containsAny, .set ty₃, .set ty₄ => ifLubThenBool ty₃ ty₄ diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index 9d954b4b4..9ccf1b0d7 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -117,6 +117,7 @@ def jsonToBinaryOp (json : Lean.Json) : ParseResult BinaryOp := do | "LessEq" => .ok .lessEq | "Add" => .ok .add | "Sub" => .ok .sub + | "Mul" => .ok .mul | "Contains" => .ok .contains | "ContainsAll" => .ok .containsAll | "ContainsAny" => .ok .containsAny @@ -181,10 +182,6 @@ partial def jsonToExpr (json : Lean.Json) : ParseResult Expr := do let op ← getJsonField body "op" >>= jsonToUnaryOp let arg ← getJsonField body "arg" >>= jsonToExpr .ok (.unaryApp op arg) - | "MulByConst" => do - let c ← getJsonField body "constant" >>= jsonToInt64 - let arg ← getJsonField body "arg" >>= jsonToExpr - .ok (.unaryApp (.mulBy c) arg) | "Like" => do let pat ← getJsonField body "pattern" >>= jsonToPattern let expr ← getJsonField body "expr" >>= jsonToExpr diff --git a/cedar-policy-generators/src/expr.rs b/cedar-policy-generators/src/expr.rs index f1404d605..d661bf764 100644 --- a/cedar-policy-generators/src/expr.rs +++ b/cedar-policy-generators/src/expr.rs @@ -108,13 +108,10 @@ impl<'a> ExprGenerator<'a> { self.generate_expr(max_depth - 1, u)?, self.generate_expr(max_depth - 1, u)?, )), - 1 => { - // arbitrary expression, which may be a constant - let expr = self.generate_expr(max_depth - 1, u)?; - // arbitrary constant integer - let c = self.constant_pool.arbitrary_int_constant(u)?; - Ok(ast::Expr::mul(expr, c)) - }, + 1 => Ok(ast::Expr::mul( + self.generate_expr(max_depth - 1, u)?, + self.generate_expr(max_depth - 1, u)?, + )), 1 => { // negation expression Ok(ast::Expr::neg(self.generate_expr(max_depth - 1, u)?)) @@ -641,17 +638,18 @@ impl<'a> ExprGenerator<'a> { )?, )), // * expression - 1 => { - // arbitrary expression, which may be a constant - let expr = self.generate_expr_for_type( + 1 => Ok(ast::Expr::mul( + self.generate_expr_for_type( &Type::long(), max_depth - 1, u, - )?; - // arbitrary integer constant - let c = self.constant_pool.arbitrary_int_constant(u)?; - Ok(ast::Expr::mul(expr, c)) - }, + )?, + self.generate_expr_for_type( + &Type::long(), + max_depth - 1, + u, + )?, + )), // negation expression 1 => Ok(ast::Expr::neg(self.generate_expr_for_type( &Type::long(),