Level checking implementation and proof (WIP)

[john-h-kastner-aws]

Implements level checking in Lean as described in RFC 76 and implemented in Rust.

Currently contains a substantial amount of correctness proof level checking and slicing, covering getAttr, hasAttr, var, lit, and ite.

The main theorem is

theorem level_based_slicing_is_sound {e : Expr} {tx : TypedExpr} {n : Nat} {c c₁ : Capabilities} {env : Environment} {request : Request} {slice entities : Entities}
  (hs : slice = entities.sliceAtLevel request n)
  (hc : CapabilitiesInvariant c request entities)
  (hr : RequestAndEntitiesMatchEnvironment env request entities)
  (ht : typeOf e c env = Except.ok (tx, c₁))
  (hl : (checkLevel tx n).checked) :
  evaluate e request entities = evaluate e request slice

[emina]

I've sync'ed with @john-h-kastner-aws about this one. It turns out that I've written a lot of similar-looking definitions and theorems as part of internal proofs. I'll package this into a PR with useful definitions and lemmas.

For example, this code can be written without any termination clauses:

def Prim.entityUIDs : Prim → Set EntityUID
  | .entityUID uid => Set.singleton uid
  | _              => Set.empty

def Value.entityUIDs : Value → Set EntityUID
  | .prim p              => p.entityUIDs
  | .set (Set.mk vs)     => vs.attach.unionAll (λ ⟨v, _⟩ => v.entityUIDs)
  | .record (Map.mk avs) => avs.attach₃.unionAll (λ ⟨(_, v), _⟩ => v.entityUIDs)
  | .ext _               => Set.empty

[emina]

We might also want to have another higher-level theorem (which calls this one) that doesn't mention capabilities. Something along these lines:

cedar-spec/cedar-lean/Cedar/Thm/Typechecking.lean

Line 34 in ead3c16

/--

[emina]

Nice!