Add typechecker DRT target comparing the typed expression (#840)

[repowazdogz-droid]

Closes #840.

The existing validator DRT compares whether Rust and Lean agree that validation
passed. This adds a target that compares the TypedExpr each side produces, so a
disagreement about the annotated AST is visible even when both sides reach the same
verdict.

Rust side is Typechecker::typecheck_by_single_request_env. Lean side is a new
typecheckPolicyTyped export over Validation.typecheckPolicy. Results are aligned
by policy id and by a (principal, action, resource) environment key that both sides
produce independently.

How the comparison works

Each side is rendered independently into a small neutral node type, with the type
annotation carried as a compared field. The Lean tree is not decoded into the Rust
AST, and neither side is projected through an untyped expression. The annotation is
the object under test here, so any representation without an annotation slot would
erase exactly what the target exists to compare, and a decoder would have to hardcode
the Type against CedarType correspondence that is under test. This is discussed
in the issue thread.

Declared normalisations, each with a test:

• Rust Like and Is are AST variants; Lean models both as unaryApp. The Rust side
  is folded to the Lean shape. A matching case agrees and a differing pattern is still
  caught.
• Record fields are compared as sorted key and value pairs, so ordering alone is never
  a divergence while a duplicated or missing key still is.
• Slot and Unknown have no Lean counterpart and are reported as unsupported rather
  than as a shape mismatch.
• A statically-true condition that Rust folds to Lit(true) and Lean keeps as a
  conjunction gets its own bucket. The folded side is a leaf, so the types the two
  sides assign to the whole condition are compared and reported instead. A folded pair
  whose types disagree stays a finding.

Six phantom-divergence classes found while building this

Each of these made the harness report a difference that was an artifact of the two
encodings rather than anything about the validators. They are in their own commit.

1. cedar-policy-core enables serde_json's preserve_order, so object key order is
   insertion order. Lean emits entity types as {"path": .., "id": ..} and the natural
   Rust construction order is the reverse, so every entity-typed node mismatched.
2. Lean's derived ToJson does not emit constructor fields in declaration order
   (and comes back as ty, b, a), so positional child comparison mismatched on every
   binary node.
3. Round-tripping a policy set through to_string and parse_policyset is not
   id-preserving: the parser assigns fresh policy0, policy1, ... and every pair then
   failed to align.
4. Display for PolicyID escapes via escape_debug while Lean emits raw, so ids
   holding control characters never matched.
5. Display for EntityUID renders the eid through Eid::escaped(), giving the action
   component of the environment key the same problem.
6. Template-linked policies were skipped on the Rust side but still returned by Lean,
   leaving pairs that were never compared reported as unmatched environments.

The guard for the first was checked by removing the fix and confirming the test fails
with the predicted output, so it is not a test that passes for the wrong reason.

What the target establishes, and what it does not

Controls are two-halved: each asserts that the clean pair produces zero divergences
and that the tampered pair produces exactly one classified divergence, in the same
run, so a control that catches its plant has also shown the correct case passing. 14
unit tests plus an end-to-end run against the real Lean backend.

No claim is made that the two typecheckers agree. The end-to-end test asserts only
that the harness ran and produced no harness problems. Asserting agreement would turn
a real disagreement into a broken test, and the point of the target is to report
disagreements rather than to encode an expected answer. Agreement is also bounded by
the shared Cedar specification: if the spec is wrong, both sides can agree and both be
wrong.

Over 40000 fuzz executions the target completes with zero harness problems, covering
71865 (policy, environment) pairs. Of those pairs, 10.65% carry the Var(Action)
against literal result described below.

That percentage needs reading carefully and I would rather state the limit than let it
be taken for more than it is. libFuzzer is coverage-guided, so the executions are not
independent draws, and the generated schemas skew small. 10.65% describes this
generator's output under this harness. It is not a prevalence estimate for real Cedar
policies, and nothing here supports treating it as one.

One result worth a maintainer decision

Validation.typecheckPolicy substitutes the concrete action EUID before typechecking:

let expr := substituteAction env.reqty.action policy.toExpr

typecheck_by_single_request_env typechecks t.condition() directly and has no
equivalent, so it keeps Var(Action) where Lean has the literal.

This is not offered as a defect in either implementation. The substitution is
deliberate and documented on the Lean side, and both sides reach the same validation
verdict, which is why a pass/fail comparison never surfaced it. It is a scope question:
whether the Rust typed expression is meant to mirror the specification's substitution
is yours to decide, and the target reports the difference rather than normalising it
away so that the decision stays with you.

Running it

cargo fuzz run typed-expression-drt

CEDAR_TYPED_EXPR_SURVEY counts and prints findings instead of asserting on them.
That downgrades the target to an observer and should stay unset in CI; it exists for
measuring how often a class appears before deciding what it is.

[victornicolet]

Thank you for the contribution!
Can you confirm you were able to run the target, and didn't find encounter any failures?

[victornicolet]

I think the notes, including the other files in this repository, should be ommitted from this PR.

[victornicolet]

nit: perhaps a better name can be found, the FFI is not specific to the DRT.

[victornicolet]

Do we need this survey mode in the final PR? Was it used to test the new target?

[repowazdogz-droid]

Yes, it runs at scale. 40,000 executions against the current corpus of 5,379 inputs, of which 34,832 reached the comparison and produced 101,401 (policy, environment) pairs.

I would rather not answer that as "no failures", because that is not what happened. Seven phantom-divergence classes came out of building and running this, every one of them the harness being wrong rather than either typechecker. The seventh only surfaced once I removed the survey switch: literal_json (typed_expr.rs:506) rendered entity eids through Eid::escaped(), so a control character became the literal text \u{7} on the Rust side, against the standard JSON escape for U+0007 from Lean. Same cause as the environment-key fix already in the PR, at a site that fix did not reach. Both halves are tested now, that the escaping alone is not a divergence and that a genuinely different eid is still caught.

After those fixes, findings() returns exactly two classes on ordinary generated input. Neither one is a defect in either implementation.

The first is mine and I will fix it. OUTCOME_MISMATCH, 3.25% of pairs. Of the cases I instrumented, 1031 of 1031 were PolicyCheck::Irrelevant on the Rust side against an error from Lean, with zero Success. The class is manufactured by my own choice at typed_expr.rs:903, where I map Irrelevant to a successful typed expression on the grounds that the policy typechecked and is only statically false. Lean's typecheckPolicy returns an error for those same pairs, so that mapping is what turns them into a disagreement. Mapping Irrelevant to None instead puts them in the arm where both sides agree on rejection. I will make that change, add the two-halved test, and confirm the class goes to zero.

The second is yours to decide and I have deliberately left it alone. SHAPE_MISMATCH, var against lit, 10.71% of pairs. This is the substituteAction behaviour at Cedar/Validation/Validator.lean:197, where Lean substitutes the concrete action EUID before typechecking and typecheck_by_single_request_env has no equivalent.

Declaring it a known difference is what makes the target green and lets it assert. Declaring it also answers the scope question this PR raises, and that answer belongs to you rather than to me. So I would rather ask than assume: should the var against lit result be declared a known representational difference, so the target asserts on everything else? Or does it stay a finding, in which case the target observes and reports rather than blocking, until you have settled whether the Rust typed expression should mirror the specification's substitution?

I have not implemented either and will follow your answer.

Your other three points are done locally, pending that answer:

• drt-840-notes/ is out of the PR.
• CedarFFI/TypedExprDRT.lean is now CedarFFI/TypedExpr.lean, matching Main.lean and ToJson.lean.
• Survey mode and CEDAR_TYPED_EXPR_SURVEY are removed. The 10.71% above was measured with a temporary local build that is not part of the PR.

[repowazdogz-droid]

The branch is at 2c6eb0a8. Summary of what changed and what is still yours to call.

I said I would map PolicyCheck::Irrelevant to None so those pairs land in the agree-on-rejection arm and OUTCOME_MISMATCH goes to zero. I implemented that, measured it, and it is wrong, so the measurement goes first.

Over the 5,379-input corpus, 26,745 compared (policy, env) pairs, the cross-tab of the Rust PolicyCheck variant against whether Lean returned a typed expression is:

Rust	Lean returns expr	Lean errors
Success	16,427	0
Irrelevant	7,969	1,007
Fail	0	1,342

There are 8,976 Irrelevant pairs, and Lean errors on 1,007 of them, which is 11.2%. For the other 7,969 it returns an expression that the target compares today. So mapping Irrelevant to None takes OUTCOME_MISMATCH from 1,007 pairs (3.77%) to 7,969 (29.80%), and it stops comparing trees that both sides produce on those 7,969 pairs, which shows up as SHAPE_MISMATCH falling from 2,676 to 1,025 and CONSTANT_FOLDED_CONDITION from 15,565 to 15,208.

The 1031/1031 figure I quoted earlier does not support the change and I should not have offered it as evidence. Under the old mapping OUTCOME_MISMATCH could only contain Irrelevant-against-Lean-error pairs, because Success-against-error and Fail-against-expression are both empty in the data. Sampling that bucket returns 100% Irrelevant-against-error whatever the other 7,969 pairs do. I measured the population already in the bucket rather than the population the change would move into it.

What is on the branch instead is to treat Rust-Irrelevant-against-Lean-error as a declared representational difference in its own bucket, STATICALLY_FALSE_POLICY, covered by is_declared_difference alongside the constant-folding case. Same corpus and same denominator:

bucket	before	after
CONSTANT_FOLDED_CONDITION	15,565	15,565
SHAPE_MISMATCH	2,676	2,676
OUTCOME_MISMATCH	1,007	0
STATICALLY_FALSE_POLICY	0	1,007

Exactly the 1,007 pairs change bucket and nothing else moves, so the reclassification costs no comparison coverage. Worth being precise about what that zero is: those pairs are not repaired, they are relabelled, and findings() is empty of them because the class is declared. The empirical part is that declaring it moved nothing else. Whether the two implementations really do agree in substance there is a judgement about what Irrelevant and a Lean typecheck error each mean, and if you would rather it stayed a finding until that is settled against the spec, say so and I will put those pairs back into OUTCOME_MISMATCH. The change is separable from the rest of the commit.

Three tests cover it, all bound to the production predicates rather than restating the rule in the test, since a test that re-implemented the mapping would have passed against the refuted version.

statically_false_against_lean_error_is_a_declared_difference is the declared case end to end against the real Lean backend, reproduced verbatim from a corpus input.

genuine_outcome_divergence_is_still_caught holds the guards against the declaration widening: a Rust Success against a Lean error is still an outcome divergence, the outcome bucket is still a finding in both directions, and a statically-false pair that Lean does type is still compared as a tree. Both of these fail if Irrelevant is remapped to None.

outcome_divergence_is_reported_through_the_driver exists because of something the first two do not cover. The corpus contains no pair where one side typechecks a policy the other rejects, so the OutcomeMismatch arm is never reached end to end by real input, and I confirmed by sentinel that no other test in the suite reaches it either. That test drives it through run_typed_expr_drt by giving the Rust and Lean views different policies under one policy id, which the driver already documents as the caller's responsibility. It is a manufactured divergence, not a discovered one: it shows the routing into that arm works, and it says nothing about the two typecheckers disagreeing, because on this corpus they never do.

The substituteAction question is unchanged and still open. Lean substitutes the concrete action EUID before typechecking (Cedar/Validation/Validator.lean:197) and typecheck_by_single_request_env has no equivalent, which is where the var against lit SHAPE_MISMATCH at 10.01% comes from. I have left it as a finding rather than normalising it away.

Two corrections to locations I gave earlier. The mapping is in cedar-drt/src/typed_expr.rs, not in the fuzz target, which is a thin shell that calls compare_typed_expressions and panics on findings. There is a second occurrence inside end_to_end_negative_control_two_halved; I left it alone because it only harvests an expression to plant a fault into and never reaches the outcome arm, which I checked with a sentinel rather than by reading. Narrowing it to Success would also risk its "at least one policy must typecheck" expectation, and that fragility is now recorded in a doc comment on the test.

Your other three points are done: drt-840-notes/ is gone, CedarFFI/TypedExprDRT.lean is now TypedExpr.lean, and survey mode and CEDAR_TYPED_EXPR_SURVEY are removed. Happy to take either call on the two open ones.