Partial Evaluation DRT #308

aaronjeline · 2024-05-08T14:19:27Z

Issue #, if available:
N/A
Description of changes:
Adds DRT for partial evaluation

It does find a discrepancy

cdisselkoen

Looks good to me overall

cedar-drt/fuzz/fuzz_targets/partial-eval.rs

cedar-drt/fuzz/src/lib.rs

cedar-lean/DiffTest/Parser.lean

cedar-drt/fuzz/fuzz_targets/partial-eval.rs

khieta

Some high-level comments

I imagine we'll also want to be DRT'ing policies, since the logic to compute the "definitely erroring policies" and such is a little confusing. Might make sense to add an additional target in this PR, like how we have abac-type-directed and eval_type_directed.
Let's change the name to partial-eval-type-directed for consistency with the other targets.
Can you add support for PE to Cli/Main.lean too? Should be easy since you've already set up the DRT functionality.

cedar-lean/DiffTest/Parser.lean

khieta · 2024-05-09T15:34:24Z

cedar-policy-generators/src/expr.rs

-            let unknown_type: Option<ast::Type> = target_type.clone().try_into().ok();
-            match unknown_type {
-                Some(ty) => Ok(ast::Expr::unknown(ast::Unknown::new_with_type(name, ty))),
-                None => Ok(ast::Expr::unknown(ast::Unknown::new_untyped(name))),
-            }
+            Ok(ast::Expr::unknown(ast::Unknown::new_untyped(name)))


What's the reason for this change?

Bumping this question from @khieta as well

Reverted, good catch @khieta

khieta · 2024-05-09T15:35:10Z

cedar-lean/DiffTest/Parser.lean

+    | .ok v => ValueOrExpr.value <$> (jsonToValue v)
+    | .error _ => match json.getObjVal? "Expr" with
+      | .ok e => ValueOrExpr.expr <$> (jsonToPartialExpr e)
+      | .error _ => .error "Expected either `expr` or `value`"


Suggested change

| .error _ => .error "Expected either `expr` or `value`"

| .error _ => .error "jsonToValueOrExpr: expected either `Expr` or `Value`"

did you reject this suggestion? it was resolved but it doesn't appear in the latest diff

cedar-lean/Cedar/Spec/ExtFun.lean

aaronjeline · 2024-05-09T15:43:51Z

Some high-level comments

I imagine we'll also want to be DRT'ing policies, since the logic to compute the "definitely erroring policies" and such is a little confusing. Might make sense to add an additional target in this PR, like how we have abac-type-directed and eval_type_directed.

Absolutely, just waiting for partial auth code to be merged

Let's change the name to partial-eval-type-directed for consistency with the other targets.

Will do

Can you add support for PE to Cli/Main.lean too? Should be easy since you've already set up the DRT functionality.

Sure

cdisselkoen · 2024-05-09T15:54:35Z

Partial auth code was merged last week (#299) :)

aaronjeline · 2024-05-22T18:29:14Z

Blocked by: cedar-policy/cedar#898

cedar-lean/Cedar/Partial/Expr.lean

cdisselkoen

Nothing in my comments needs to be blocking

cedar-drt/fuzz/fuzz_targets/partial-eval.rs

cedar-drt/fuzz/src/lib.rs

cedar-lean/Cedar/Thm/Data/Applicative.lean

cedar-lean/Cedar/Thm/Partial/Expr/Lemmas.lean

cedar-drt/fuzz/fuzz_targets/partial-eval.rs

cdisselkoen · 2024-06-04T12:01:07Z

cedar-policy-generators/src/expr.rs

-            let unknown_type: Option<ast::Type> = target_type.clone().try_into().ok();
-            match unknown_type {
-                Some(ty) => Ok(ast::Expr::unknown(ast::Unknown::new_with_type(name, ty))),
-                None => Ok(ast::Expr::unknown(ast::Unknown::new_untyped(name))),
-            }
+            Ok(ast::Expr::unknown(ast::Unknown::new_untyped(name)))


Bumping this question from @khieta as well

Signed-off-by: Aaron Eline <[email protected]>

cdisselkoen · 2024-06-13T13:58:06Z

cedar-drt/fuzz/fuzz_targets/partial-auth.rs

+            PolicyKind::True => Expr::val(true),
+            PolicyKind::False => Expr::val(false),
+            PolicyKind::Error => Expr::add(Expr::val(1), Expr::val(false)),
+            PolicyKind::Residual => Expr::get_attr(Expr::var(ast::Var::Context), "unknown".into()),


should this expression include an actual unknown?

cdisselkoen · 2024-06-13T14:02:04Z

cedar-lean/Cedar/Thm/Partial/Expr.lean

+theorem roundtrip (e : Spec.Expr) (pe : Partial.Expr) :
+  e.asPartialExpr = pe ↔ pe.asSpec = some e := by
+  apply Iff.intro <;> intros h
+  all_goals { (first | apply roundtrip₂ | apply roundtrip₁) <;> assumption }


maybe something like this is clearer?

Suggested change

all_goals { (first | apply roundtrip₂ | apply roundtrip₁) <;> assumption }

· apply roundtrip₂ ; assumption

· apply roundtrip₁ ; assumption

Or, instead of assumption, use h directly.

Suggested change

all_goals { (first | apply roundtrip₂ | apply roundtrip₁) <;> assumption }

· exact roundtrip₂ _ _ h

· exact roundtrip₁ _ _ h

or something similar

cdisselkoen · 2024-06-13T14:06:57Z

cedar-lean/DiffTest/Parser.lean

+    | .ok v => ValueOrExpr.value <$> (jsonToValue v)
+    | .error _ => match json.getObjVal? "Expr" with
+      | .ok e => ValueOrExpr.expr <$> (jsonToPartialExpr e)
+      | .error _ => .error "Expected either `expr` or `value`"


did you reject this suggestion? it was resolved but it doesn't appear in the latest diff

aaronjeline force-pushed the aeline/partial-eval branch from 12e7ba5 to b1bc1f5 Compare May 8, 2024 14:29

aaronjeline marked this pull request as ready for review May 8, 2024 15:08

aaronjeline requested review from cdisselkoen and khieta May 8, 2024 15:08

cdisselkoen reviewed May 8, 2024

View reviewed changes

khieta reviewed May 9, 2024

View reviewed changes

aaronjeline force-pushed the aeline/partial-eval branch 5 times, most recently from 807602b to b28b0b2 Compare May 22, 2024 17:46

aaronjeline requested review from cdisselkoen and emina May 22, 2024 17:46

aaronjeline mentioned this pull request May 22, 2024

Supporting PE/PA testing cedar-policy/cedar#898

Merged

3 tasks

aaronjeline mentioned this pull request May 24, 2024

Adding stups for PE/PA trait methods #338

Merged

emina approved these changes May 24, 2024

View reviewed changes

cedar-lean/Cedar/Partial/Expr.lean Show resolved Hide resolved

cdisselkoen approved these changes May 24, 2024

View reviewed changes

aaronjeline force-pushed the aeline/partial-eval branch from 5fa3e9b to 51ed147 Compare May 24, 2024 18:50

aaronjeline requested review from cdisselkoen and emina May 29, 2024 13:17

cdisselkoen approved these changes Jun 4, 2024

View reviewed changes

aaronjeline added 2 commits June 13, 2024 09:45

DRT for partial eval/auth and roundtrip proof

4b3e9a4

Signed-off-by: Aaron Eline <[email protected]>

Small change

122d198

Signed-off-by: Aaron Eline <[email protected]>

aaronjeline force-pushed the aeline/partial-eval branch from cc79fee to 122d198 Compare June 13, 2024 13:45

aaronjeline requested a review from cdisselkoen June 13, 2024 13:45

cdisselkoen approved these changes Jun 13, 2024

View reviewed changes

aaronjeline merged commit b15dcac into main Jun 13, 2024
6 checks passed

aaronjeline deleted the aeline/partial-eval branch June 13, 2024 14:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Partial Evaluation DRT #308

Partial Evaluation DRT #308

aaronjeline commented May 8, 2024 •

edited

Loading

cdisselkoen left a comment

khieta left a comment

khieta May 9, 2024

cdisselkoen Jun 4, 2024

aaronjeline Jun 11, 2024

khieta May 9, 2024

cdisselkoen Jun 13, 2024

aaronjeline commented May 9, 2024

cdisselkoen commented May 9, 2024

aaronjeline commented May 22, 2024

cdisselkoen left a comment

cdisselkoen Jun 4, 2024

cdisselkoen Jun 13, 2024

cdisselkoen Jun 13, 2024

cdisselkoen Jun 13, 2024

cdisselkoen Jun 13, 2024

	\| .error _ => .error "Expected either `expr` or `value`"
	\| .error _ => .error "jsonToValueOrExpr: expected either `Expr` or `Value`"

	all_goals { (first \| apply roundtrip₂ \| apply roundtrip₁) <;> assumption }
	· apply roundtrip₂ ; assumption
	· apply roundtrip₁ ; assumption

	all_goals { (first \| apply roundtrip₂ \| apply roundtrip₁) <;> assumption }
	· exact roundtrip₂ _ _ h
	· exact roundtrip₁ _ _ h

Partial Evaluation DRT #308

Partial Evaluation DRT #308

Conversation

aaronjeline commented May 8, 2024 • edited Loading

cdisselkoen left a comment

Choose a reason for hiding this comment

khieta left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aaronjeline commented May 9, 2024

cdisselkoen commented May 9, 2024

aaronjeline commented May 22, 2024

cdisselkoen left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aaronjeline commented May 8, 2024 •

edited

Loading