Add typechecker DRT target that ensures the same typed expression is computed

[lianah]

Category

DRT target(s)

Describe the feature you'd like to request

We should add a new DRT target that ensures that the Rust typecheck_by_single_request_env and the Lean Validator.typecheckPolicy compute the same well typed expression when successful.

Describe alternatives you've considered

Do not add this target.

Additional context

See 839 for a related target that checks that the types computed for an expression match.

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[repowazdogz-droid]

Approach: add a typecheckPolicyTyped export to CedarFFI that returns the TypedExpr from Validation.typecheckPolicy for each (policy, environment) pair, and compare it in a new DRT target against Typechecker::typecheck_by_single_request_env. Environments are matched by (principal, action, resource) rather than by list position. Every disagreement goes into one named bucket, and UNCLASSIFIED is treated as a defect in the target rather than a result.

The two ASTs are not isomorphic, so a few normalisations are unavoidable and I would rather declare them than apply them quietly: Like and Is are Rust AST variants but Lean UnaryOp constructors, and Record is a sorted BTreeMap on one side and an association list on the other.

Two defaults I will proceed with unless you would prefer otherwise. I will surface Like and Is as shape mismatches so the representational difference stays visible rather than folding them into Lean's unaryApp shape, and I will skip templates the way compare_validation_results currently does for #945. Happy to flip either.

One check before I go further: I have read #511, and since #839 was closed as covered by it I want to be sure I am not re-treading. My reading is that #511's differential bullet targets arbitrary generated expressions via the eval-type-directed style, whereas this issue is at the policy level, comparing the typed expression that typecheckPolicy and typecheck_by_single_request_env produce for each policy and environment. If you see those as the same target, say so and I will fold the work into #511 instead.

[john-h-kastner-aws]

See

cedar-spec/cedar-drt/fuzz/src/tpe.rs

Line 306 in 3f09394

let lean_pst = Expr::try_from(lean_rp.residual.clone())

for how expression equality assertions are handled elsewhere

[repowazdogz-droid]

Expr::try_from(Residual) is type-erasing by construction: all 13 arms of convert_residual bind ty with .. and none of them reads it, and pst::Expr has no annotation slot to carry a type in. That is the right call for the TPE target, where the question is whether both sides evaluated to the same residual and the typing was already settled upstream. For #840 the annotation is the object under test, so routing both sides through pst::Expr would compare the erasure of the thing being compared: if Rust annotates the 1 in context.amount < 1000 as Long and Lean annotates it Bool, the trees are structurally identical, both project to pst::Expr::Lit(Long(1)), and the assertion passes. Rust's Option<Type> against Lean's total CedarType is the sharper case, since with no annotation slot None and Some(Bool) are the same value in the target type. Decoding the Lean tree into Expr<Option<Type>> does keep the types, because educe leaves data in PartialEq, but it relocates the problem rather than removing it: the decoder has to fix which Rust Type each Lean CedarType denotes, which is the correspondence under test, and a disagreement then arrives as a conversion Err behind .expect("...should succeed"), filed as harness breakage instead of as a divergence. So I render each side independently into a small neutral node type and carry ty as a compared field. I did take the surrounding pattern from tpe.rs: matching by policy id with an explicit report when one side has a key the other lacks, the assert_eq! failure-message shape, and (Err(_), Err(FfiError::LeanBackendError(_))) treated as agreement on rejection. One correction to my earlier comment: I said I would surface Like and Is as shape mismatches and I have flipped that, because folding the Rust variants into Lean's unaryApp shape can be declared as a normalisation and tested (the matching case agrees, a differing pattern is still caught), whereas the alternative reports a mismatch on every policy that uses like. Happy to restructure any of this.