RFC 53 Lean model and proofs

[shaobo-he-aws]

Issue #, if available:

Description of changes:

[emina]

Nice PR! I like this approach.

Left small comments / suggestions on the model.

[emina]

Thinking about this more, we need to change the definition of InstanceOfEntityType and fix the upstream definitions and proofs accordingly.

In particular, the definition should be this:

def InstanceOfEntityType (e : EntityUID) (ety: EntityType) (env : Environment) : Prop :=
  e.ty = ety && (env.ets.isValidEntityUID e.ty  ∨ env.acts.contains e)

Without this change, InstanceOfType admits invalid enum literals. And this means that our type soundness theorem becomes too weak. It says that the evaluator may produce invalid entity literals even for type-correct expressions. The type checker code actually prevents this, but it also needs to be reflected in the definition of InstanceOfType and the soundness theorem.

Note that we have already made the corresponding change in RequestEntityValidator and instanceOfEntityType.

[emina]

Actually, I now realize that the definition of InstanceOfEntityType has always been too weak (!).

Note that it admits entity literals of arbitrary entity types that aren’t declared in the schema.

The actual type checking algorithm doesn’t admit this.

So, even before the addition of entity enums, this definition should have taken the environment as input and looked like this instead:

def InstanceOfEntityType (e : EntityUID) (ety: EntityType) (env : Environment) : Prop :=
  e.ty = ety && (env.ets.contains e.ty  ∨ env.acts.contains e)

[shaobo-he-aws]

So, even before the addition of entity enums, this definition should have taken the environment as input and looked like this instead:

def InstanceOfEntityType (e : EntityUID) (ety: EntityType) (env : Environment) : Prop :=
  e.ty = ety && (env.ets.contains e.ty  ∨ env.acts.contains e)

To make the scope of this PR limited to RFC 53, I propose that we fix the definition first in a separate PR and rebase this PR based on it. I'll work on the fix first.

In fact, env.ets.isValidEntityUID e.ty implies env.ets.contains e.ty so we might as well fix the definition in this PR.

[emina]

In fact, env.ets.isValidEntityUID e.ty implies env.ets.contains e.ty so we might as well fix the definition in this PR.

I'll approve this PR as-is, in case you find it's easier to fix this in a separate PR.

[cdisselkoen]

Looks good, just some small nits

[shaobo-he-aws]

Will merge this PR first and then address the weakness of InstanceOfEntityType later in a separate PR because it will be quite involved.