rename RequestType to ActionSignature

[cdisselkoen]

Renames RequestType to ActionSignature, to align some names better between our Rust and Lean code. Also renames related variables and field names (e.g. reqty to sig).

[cdisselkoen]

This was arguably misnamed previously -- it defines alignment with a TypeEnv, not just a RequestType. I renamed to InstanceOfTypeEnv rather than InstanceOfActionSignature. Note that RequestType/ActionSignature is not one of the parameters here

[emina]

Renames RequestType to ActionSignature, to align some names better between our Rust and Lean code. Also renames related variables and field names (e.g. reqty to sig).

What is RequestType called in the Rust validator code?

IIRC, ActionSignature is a fairly recent name that we started using a few months ago :)

RequestType was inherited from the Dafny formalization.

[cdisselkoen]

Ha, you're right that in the main Cedar library, it's called RequestEnv. Should I rename to RequestEnv in the Lean instead?

[emina]

Ha, you're right that in the main Cedar library, it's called RequestEnv. Should I rename to RequestEnv in the Lean instead?

We have a lot of *Envs going around so not sure about the name RequestEnv (versus changing Rust to match Lean :).

In either case, I agree that having them match is preferable.

@john-h-kastner-aws Any preferences on what this should be called, in both Rust and Lean?

[john-h-kastner-aws]

ActionSignature doesn't feel right since a single action signature doesn't completely describe an action. Some variant of *Env feels better to me since it's purpose is to provide type bindings for the scope variables. RequestType would also be good. Or RequestTypeEnv.

For completeness, I see that the Rust also defines, RequestSchema, RequestType, and another RequestType.

[emina]

Interesting! The two Rust RequestTypes look just like Lean's RequestType. Should we just leave it at RequestType?

I slightly prefer RequestType over RequestEnv because we already have TypeEnv (for type environments, which contains RequestType), Env (for concrete environments), and SymEnv (for symbolic environments).

[emina]

Ah, actually, the Rust RequestTypes are missing the context field.

[cdisselkoen]

The context field is redundant because that information already exists in the schema given the other three fields.

[emina]

That's true. We keep it around in Lean because it would be pretty annoying to have to constantly lookup the context via schema (and always have schema around just to be able to look up context).

[john-h-kastner-aws]

Should we just leave it at RequestType?

I'm happy with this, but then we'll have three RequestTypes in the Rust env :P. Hopefully we could unify those

[emina]

we'll have three RequestTypes in the Rust env :P. Hopefully we could unify those

Yep, 1 > 3 in this case :))