Category
Lean formalization
Describe the feature you'd like to request
The current model of validation works with static policies that do not have ?principal or ?resource slots. Template linked policies are handled by substituting slots for their bindings in the FFI layer.
The Rust implementation instead does typechecking over unlinked templates by treating the slots as entity-typed variables to ensure that the policy will not error for any slot bindings. It separately checks the types of entities used in actual slots make sense for the template (i.e., the linked policy is not trivially false).
This difference means that the Rust typechecker will report errors that can only occur in type environments that aren't actually present in the policy set. The Lean typechecker never sees these errors.
For example:
entity A;
entity B { foo: Bool };
entity C;
action Act appliesTo { principal: [A, B], resource: C };
permit(principal == ?principal, action == Action::"Act", resource) when {
principal.foo
};
with one link {"?principal": "B::\"b\""}
The Lean typechecker reports no errors because the entity type B has an attribute foo. The A entity type is irrelevant. In rust, we typecheck for both A and B principal slot types, leading to an error report when we see that A does not have the attribute foo.
The Rust code is more restrictive than the Lean code, so current differential testing shows that it is sound, but we should prove this and update our differential tests to assert that the Rust and Lean are exactly equivalent on templates.
Alternatively, we could move Rust to the weaker check, only validating templates when linked, but IMO this is not the expected behavior for a typechecker. We could also keep the current workaround in place.
Describe alternatives you've considered
.
Additional context
No response
Is this something that you'd be interested in working on?
Category
Lean formalization
Describe the feature you'd like to request
The current model of validation works with static policies that do not have
?principalor?resourceslots. Template linked policies are handled by substituting slots for their bindings in the FFI layer.The Rust implementation instead does typechecking over unlinked templates by treating the slots as entity-typed variables to ensure that the policy will not error for any slot bindings. It separately checks the types of entities used in actual slots make sense for the template (i.e., the linked policy is not trivially false).
This difference means that the Rust typechecker will report errors that can only occur in type environments that aren't actually present in the policy set. The Lean typechecker never sees these errors.
For example:
with one link
{"?principal": "B::\"b\""}The Lean typechecker reports no errors because the entity type
Bhas an attributefoo. TheAentity type is irrelevant. In rust, we typecheck for bothAandBprincipal slot types, leading to an error report when we see thatAdoes not have the attributefoo.The Rust code is more restrictive than the Lean code, so current differential testing shows that it is sound, but we should prove this and update our differential tests to assert that the Rust and Lean are exactly equivalent on templates.
Alternatively, we could move Rust to the weaker check, only validating templates when linked, but IMO this is not the expected behavior for a typechecker. We could also keep the current workaround in place.
Describe alternatives you've considered
.
Additional context
No response
Is this something that you'd be interested in working on?