rename RequestType to ActionSignature

cedar-lean/Cedar/SymCC/Env.lean

@@ -215,14 +215,14 @@ def SymEntities.ofSchema (ets : EntitySchema) (acts : ActionSchema) : SymEntitie
   Map.make (eData ++ aData)
 
 /--
-Creates a symbolic request for the given request type.
+Creates a symbolic request for the given action signature.
 -/
-def SymRequest.ofRequestType (reqTy : RequestType) : SymRequest :=
+def SymRequest.ofActionSignature (sig : ActionSignature) : SymRequest :=
   {
-    principal := .var ⟨"principal", TermType.ofType (.entity reqTy.principal)⟩,
-    action    := .prim (.entity reqTy.action),
-    resource  := .var ⟨"resource", TermType.ofType (.entity reqTy.resource)⟩,
-    context   := .var ⟨"context", TermType.ofType (.record reqTy.context)⟩
+    principal := .var ⟨"principal", TermType.ofType (.entity sig.principal)⟩,
+    action    := .prim (.entity sig.action),
+    resource  := .var ⟨"resource", TermType.ofType (.entity sig.resource)⟩,
+    context   := .var ⟨"context", TermType.ofType (.record sig.context)⟩
   }
 
 /--
@@ -231,7 +231,7 @@ type environment.
 -/
 def SymEnv.ofEnv (tyEnv : TypeEnv) : SymEnv :=
   {
-    request  := SymRequest.ofRequestType tyEnv.reqty,
+    request  := SymRequest.ofActionSignature tyEnv.sig,
     entities := SymEntities.ofSchema tyEnv.ets tyEnv.acts
   }
 

cedar-lean/Cedar/SymCC/Symbolizer.lean

@@ -74,17 +74,17 @@ where
       omega
 
 /--
-The variable ids here should match the variables in `SymRequest.ofRequestType`.
+The variable ids here should match the variables in `SymRequest.ofActionSignature`.
 -/
 def Request.symbolize? (req : Request) (Γ : TypeEnv) (var : TermVar) : Option Term :=
-  if var == { id := "principal", ty := TermType.ofType (.entity Γ.reqty.principal) } then
-    Value.symbolize? ↑req.principal (.entity Γ.reqty.principal)
-  else if var == { id := "action", ty := TermType.ofType (.entity Γ.reqty.action.ty) } then
-    Value.symbolize? ↑req.action (.entity Γ.reqty.action.ty)
-  else if var == { id := "resource", ty := TermType.ofType (.entity Γ.reqty.resource) } then
-    Value.symbolize? ↑req.resource (.entity Γ.reqty.resource)
-  else if var == { id := "context", ty := TermType.ofType (.record Γ.reqty.context) } then
-    Value.symbolize? ↑req.context (.record Γ.reqty.context)
+  if var == { id := "principal", ty := TermType.ofType (.entity Γ.sig.principal) } then
+    Value.symbolize? ↑req.principal (.entity Γ.sig.principal)
+  else if var == { id := "action", ty := TermType.ofType (.entity Γ.sig.action.ty) } then
+    Value.symbolize? ↑req.action (.entity Γ.sig.action.ty)
+  else if var == { id := "resource", ty := TermType.ofType (.entity Γ.sig.resource) } then
+    Value.symbolize? ↑req.resource (.entity Γ.sig.resource)
+  else if var == { id := "context", ty := TermType.ofType (.record Γ.sig.context) } then
+    Value.symbolize? ↑req.context (.record Γ.sig.context)
   else
     .none
 

cedar-lean/Cedar/TPE/Evaluator.lean

@@ -266,7 +266,7 @@ def evaluatePolicy (schema : Schema)
       if requestAndEntitiesIsValid env req es
       then
         do
-          let expr := substituteAction env.reqty.action p.toExpr
+          let expr := substituteAction env.sig.action p.toExpr
           let (te, _) ← (typeOf expr ∅ env).mapError Error.invalidPolicy
           .ok (evaluate (TypedExpr.toResidual te.liftBoolTypes) req es)
       else .error .invalidRequestOrEntities

cedar-lean/Cedar/TPE/Input.lean

@@ -65,12 +65,12 @@ def partialIsValid {α} (o : Option α) (f : α → Bool) : Bool :=
 
 def requestIsValid (env : TypeEnv) (req : PartialRequest) : Bool :=
   (partialIsValid req.principal.asEntityUID λ principal =>
-    instanceOfEntityType principal env.reqty.principal env) &&
-  req.action == env.reqty.action &&
+    instanceOfEntityType principal env.sig.principal env) &&
+  req.action == env.sig.action &&
   (partialIsValid req.resource.asEntityUID λ resource =>
-    instanceOfEntityType resource env.reqty.resource env) &&
+    instanceOfEntityType resource env.sig.resource env) &&
   (partialIsValid req.context λ m =>
-    instanceOfType (.record m) (.record env.reqty.context) env)
+    instanceOfType (.record m) (.record env.sig.context) env)
 
 def entitiesIsValid (env : TypeEnv) (es : PartialEntities) : Bool :=
   (es.toList.all entityIsValid) && (env.acts.toList.all instanceOfActionSchema)

cedar-lean/Cedar/Thm/SymCC/Compiler/WellTyped.lean

@@ -435,7 +435,7 @@ theorem compile_well_typed_var {v : Var} {ty : CedarType} {Γ : TypeEnv} {εnv :
     CompileWellTyped,
     TypedExpr.toExpr,
     SymEnv.ofEnv,
-    SymRequest.ofRequestType,
+    SymRequest.ofActionSignature,
     TermType.ofType,
     compile,
     compileVar,

cedar-lean/Cedar/Thm/SymCC/Env/Completeness.lean

@@ -504,7 +504,7 @@ private theorem ofEnv_request_completeness
   (hwf_Γ : Γ.WellFormed)
   (hwf_I : I.WellFormed (SymEnv.ofEnv Γ).entities)
   (hsame_I : env ∼ SymEnv.interpret I (SymEnv.ofEnv Γ)) :
-  InstanceOfRequestType env.request Γ
+  InstanceOfTypeEnv env.request Γ
 := by
   have ⟨hwf_I_vars, _⟩ := hwf_I
   have ⟨⟨hsame_I_princ, hsame_I_act, hsame_I_res, hsame_I_ctx⟩, _⟩ := hsame_I
@@ -520,7 +520,7 @@ private theorem ofEnv_request_completeness
     simp only [hsame_I_princ, Term.typeOf, TermPrim.typeOf] at hwt_I_princ
     simp only [
       SymEnv.ofEnv,
-      SymRequest.ofRequestType,
+      SymRequest.ofActionSignature,
       Term.typeOf,
       TermType.ofType,
     ] at hwt_I_princ
@@ -535,7 +535,7 @@ private theorem ofEnv_request_completeness
   · simp only [
       Term.interpret,
       SymEnv.ofEnv,
-      SymRequest.ofRequestType,
+      SymRequest.ofActionSignature,
     ] at hsame_I_act
     simp only [Term.prim.injEq, TermPrim.entity.injEq] at hsame_I_act
     simp [hsame_I_act]
@@ -544,7 +544,7 @@ private theorem ofEnv_request_completeness
     simp only [hsame_I_res, Term.typeOf, TermPrim.typeOf] at hwt_I_res
     simp only [
       SymEnv.ofEnv,
-      SymRequest.ofRequestType,
+      SymRequest.ofActionSignature,
       Term.typeOf,
       TermType.ofType,
     ] at hwt_I_res
@@ -558,13 +558,13 @@ private theorem ofEnv_request_completeness
   · have ⟨hwf_I_ctx, hwt_I_ctx⟩ := interpret_term_wf hwf_I hwf_sym_ctx
     simp only [
       SymEnv.ofEnv,
-      SymRequest.ofRequestType,
+      SymRequest.ofActionSignature,
       Term.typeOf,
     ] at hwt_I_ctx
     simp only [
       SameValues,
       SymEnv.ofEnv,
-      SymRequest.ofRequestType,
+      SymRequest.ofActionSignature,
     ] at hsame_I_ctx
     have ⟨_, _, _, hwt_ctx⟩ := wf_env_implies_wf_request hwf_Γ
     have hlifted_ctx := wf_env_implies_ctx_lifted hwf_Γ

cedar-lean/Cedar/Thm/SymCC/Env/Soundness.lean

@@ -49,7 +49,7 @@ private theorem env_symbolize?_same_request
     SymEnv.interpret,
     Env.symbolize?,
     SymEnv.ofEnv,
-    SymRequest.ofRequestType,
+    SymRequest.ofActionSignature,
     SymRequest.interpret,
     Request.symbolize?,
     Value.symbolize?,
@@ -67,10 +67,10 @@ private theorem env_symbolize?_same_request
   · have ⟨_, ⟨_, h, _, _⟩, _⟩ := hinst
     simp [h]
   -- Same context after interpretation
-  · have hwf_ctx_ty : (CedarType.record Γ.reqty.context).WellFormed Γ := by
+  · have hwf_ctx_ty : (CedarType.record Γ.sig.context).WellFormed Γ := by
       have ⟨_, _, _, h⟩ := wf_env_implies_wf_request hwf
       exact h
-    have hwt_ctx : InstanceOfType Γ env.request.context (.record Γ.reqty.context) := by
+    have hwt_ctx : InstanceOfType Γ env.request.context (.record Γ.sig.context) := by
       have ⟨_, ⟨_, _, _, h⟩, _⟩ := hinst
       exact h
     have hwf_ctx : (Value.record env.request.context).WellFormed env.entities := by
@@ -1162,27 +1162,27 @@ private theorem env_symbolize?_wf_vars
   have ⟨hwf_Γ, _, _⟩ := hinst
   have ⟨hwf_princ_ty, hcontains_action, hwf_resource_ty, hwf_context_ty⟩ := wf_env_implies_wf_request hwf_Γ
   replace hwf_princ_ty :
-    (CedarType.entity Γ.reqty.principal).WellFormed Γ
+    (CedarType.entity Γ.sig.principal).WellFormed Γ
   := by constructor; exact hwf_princ_ty
   replace hwf_resource_ty :
-    (CedarType.entity Γ.reqty.resource).WellFormed Γ
+    (CedarType.entity Γ.sig.resource).WellFormed Γ
   := by constructor; exact hwf_resource_ty
   have hwf_action_ty :
-    (CedarType.entity Γ.reqty.action.ty).WellFormed Γ
+    (CedarType.entity Γ.sig.action.ty).WellFormed Γ
   := by
     constructor
     apply Or.inr
     simp only [ActionSchema.IsActionEntityType]
-    exists Γ.reqty.action
+    exists Γ.sig.action
   have ⟨_, ⟨hinst_princ, hinst_action, hinst_resource, hinst_context⟩, _⟩ := hinst
   replace hinst_princ :
-    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.principal)) (CedarType.entity Γ.reqty.principal)
+    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.principal)) (CedarType.entity Γ.sig.principal)
   := by constructor; exact hinst_princ
   replace hinst_resource :
-    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.resource)) (CedarType.entity Γ.reqty.resource)
+    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.resource)) (CedarType.entity Γ.sig.resource)
   := by constructor; exact hinst_resource
   replace hinst_action :
-    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.action)) (CedarType.entity Γ.reqty.action.ty)
+    InstanceOfType Γ (Value.prim (Prim.entityUID env.request.action)) (CedarType.entity Γ.sig.action.ty)
   := by
     constructor
     simp only [InstanceOfEntityType, hinst_action, true_and]

cedar-lean/Cedar/Thm/SymCC/Env/ofEnv.lean

@@ -567,7 +567,7 @@ theorem ofEnv_request_is_wf
 := by
   simp only [
     SymEnv.ofEnv,
-    SymRequest.ofRequestType,
+    SymRequest.ofActionSignature,
     SymRequest.WellFormed,
     TermType.ofType,
   ]
@@ -610,7 +610,7 @@ theorem ofEnv_request_is_basic
 := by
   simp [
     SymEnv.ofEnv,
-    SymRequest.ofRequestType,
+    SymRequest.ofActionSignature,
     SymRequest.IsBasic,
     Term.isBasic,
     Term.isLiteral,

cedar-lean/Cedar/Thm/SymCC/WellTyped.lean

@@ -38,7 +38,7 @@ theorem wellTypedPolicy_some_implies_exists_typed_exprs
   ∃ tx tx' : TypedExpr, ∃ c,
     TypedExpr.WellTyped Γ tx.liftBoolTypes ∧
     TypedExpr.WellTyped Γ tx' ∧
-    typeOf (substituteAction Γ.reqty.action p.toExpr) ∅ Γ = Except.ok (tx, c) ∧
+    typeOf (substituteAction Γ.sig.action p.toExpr) ∅ Γ = Except.ok (tx, c) ∧
     p'.toExpr = tx'.toExpr ∧
     tx' =
       (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))
@@ -147,7 +147,7 @@ theorem substitute_action_preserves_valid_refs
 := by
   have ⟨hwf_Γ, _, ⟨_, hinst_sch⟩⟩ := hinst
   have ⟨_, _, ⟨act_entry, hfind_act, _⟩⟩ := hwf_Γ
-  have heq_act : Γ.reqty.action = request.action := by
+  have heq_act : Γ.sig.action = request.action := by
     have ⟨_, ⟨_, h, _⟩, _⟩ := hinst
     simp [h]
   cases expr with
@@ -292,7 +292,7 @@ theorem wellTypedPolicy_preserves_valid_refs
   rotate_left
   repeat constructor
   apply typeOf_preserves_valid_refs entities hty
-  have : Γ.reqty.action = request.action := by
+  have : Γ.sig.action = request.action := by
     have ⟨_, ⟨_, h, _⟩, _⟩ := hinst
     simp [h]
   simp only [this]
@@ -341,18 +341,18 @@ theorem wellTypedPolicy_preserves_evaluation
   = evaluate p'.toExpr request entities
 := by
   have ⟨tx, tx', _, hwt_tx_lift, hwt_tx', hty, heq_p'_tx', heq_tx', hbool⟩ := wellTypedPolicy_some_implies_exists_typed_exprs hwt
-  have heq_action : Γ.reqty.action = request.action := by
+  have heq_action : Γ.sig.action = request.action := by
     have ⟨_, ⟨_, h, _⟩, _⟩ := hinst
     simp [h]
   have :
     evaluate p.toExpr request entities
-    = evaluate (substituteAction Γ.reqty.action p.toExpr) request entities
+    = evaluate (substituteAction Γ.sig.action p.toExpr) request entities
   := by
     simp only [heq_action]
     exact Eq.symm (substitute_action_preserves_evaluation _ _ _)
   rw [this]
   have heq :
-    evaluate (substituteAction Γ.reqty.action p.toExpr) request entities
+    evaluate (substituteAction Γ.sig.action p.toExpr) request entities
     = evaluate tx.toExpr request entities
   := type_of_preserves_evaluation_results (empty_capabilities_invariant _ _) hinst hty
   rw [heq]

cedar-lean/Cedar/Thm/TPE.lean

@@ -154,10 +154,10 @@ theorem partial_evaluate_policy_is_sound
   have h₆ := partial_evaluate_is_sound h₉ h₄ h₃
   subst h₁₂
   have h₇ := type_of_preserves_evaluation_results (empty_capabilities_invariant req es) h₄ heq₂
-  have h₈ : Spec.evaluate (substituteAction env.reqty.action policy.toExpr) req es = Spec.evaluate policy.toExpr req es := by
+  have h₈ : Spec.evaluate (substituteAction env.sig.action policy.toExpr) req es = Spec.evaluate policy.toExpr req es := by
     simp [InstanceOfWellFormedEnvironment] at h₄
     rcases h₄ with ⟨_, h₄, _⟩
-    simp [InstanceOfRequestType] at h₄
+    simp [InstanceOfTypeEnv] at h₄
     rcases h₄ with ⟨_, h₄, _⟩
     rw [←h₄]
     exact substitute_action_preserves_evaluation policy.toExpr req es

cedar-lean/Cedar/Thm/Validation/EnvironmentValidation.lean

@@ -465,12 +465,12 @@ theorem action_schema_validate_well_formed_is_sound
   exact action_schema_validate_transitive_action_hierarchy_is_sound hok
 
 theorem request_type_validate_well_formed_is_sound
-  {env : TypeEnv} {reqty : RequestType}
-  (hok : reqty.validateWellFormed env = .ok ()) :
-  RequestType.WellFormed env reqty
+  {env : TypeEnv} {sig : ActionSignature}
+  (hok : sig.validateWellFormed env = .ok ()) :
+  sig.WellFormed env
 := by
-  simp only [RequestType.WellFormed]
-  simp only [RequestType.validateWellFormed] at hok
+  simp only [ActionSignature.WellFormed]
+  simp only [ActionSignature.validateWellFormed] at hok
   split at hok
   rotate_left
   · contradiction
@@ -519,8 +519,8 @@ theorem env_validate_well_formed_is_sound
     action_schema_validate_well_formed_is_sound hwf_acts,
     true_and,
   ]
-  -- Check that the request types are well-formed
-  cases hwf_reqs : RequestType.validateWellFormed env env.reqty
+  -- Check that the action signature is well-formed
+  cases hwf_reqs : env.sig.validateWellFormed env
   · simp [hwf_reqs] at hok
   simp only [hwf_reqs] at hok
   exact request_type_validate_well_formed_is_sound hwf_reqs

cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean

@@ -46,7 +46,7 @@ inductive TypedExpr.EntityAccessAtLevel (env : TypeEnv) : TypedExpr → Nat →
   | var (v : Var) (ty : CedarType) (n nmax : Nat) (path : List Attr) :
     EntityAccessAtLevel env (.var v ty) n nmax path
   | action (ty : CedarType) (n nmax : Nat) (path : List Attr) :
-    EntityAccessAtLevel env (.lit (.entityUID env.reqty.action) ty) n nmax path
+    EntityAccessAtLevel env (.lit (.entityUID env.sig.action) ty) n nmax path
   | ite (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType)  (n nmax : Nat) (path : List Attr)
     (hl₁ : AtLevel env tx₁ nmax)
     (hl₂ : tx₂.EntityAccessAtLevel env n nmax path)

cedar-lean/Cedar/Thm/Validation/RequestEntityValidation.lean

@@ -147,11 +147,11 @@ decreasing_by
     omega
 
 theorem instance_of_request_type_refl {request : Request} {env : TypeEnv}:
-  instanceOfRequestType request env = true → InstanceOfRequestType request env
+  instanceOfTypeEnv request env = true → InstanceOfTypeEnv request env
 := by
   intro h₀
-  simp only [InstanceOfRequestType]
-  simp only [instanceOfRequestType, Bool.and_eq_true, beq_iff_eq] at h₀
+  simp only [InstanceOfTypeEnv]
+  simp only [instanceOfTypeEnv, Bool.and_eq_true, beq_iff_eq] at h₀
   have ⟨⟨⟨h₁,h₂⟩,h₃⟩, h₄⟩ := h₀
   and_intros
   · exact (instance_of_entity_type_refl h₁).1

cedar-lean/Cedar/Thm/Validation/Slice/Reachable.lean

@@ -47,7 +47,7 @@ theorem checked_eval_entity_lit_is_action {p : Prim} {n nmax : Nat} {c c' : Capa
 := by
   cases p
   case entityUID =>
-    replace he : euid = env.reqty.action := by
+    replace he : euid = env.sig.action := by
       replace ⟨ _, ht ⟩ := type_of_lit_inversion ht
       rw [ht] at hel
       cases hel

cedar-lean/Cedar/Thm/Validation/Typechecker/LitVar.lean

@@ -65,7 +65,7 @@ theorem type_of_var_is_sound {var : Var} {c₁ c₂ : Capabilities} {env : TypeE
   simp only [typeOf, typeOfVar, List.empty_eq, Function.comp_apply] at h₃
   have hwf := h₂.wf_env
   have ⟨_, h₂, _⟩ := h₂
-  simp [InstanceOfRequestType] at h₂
+  simp [InstanceOfTypeEnv] at h₂
   cases var
   <;> simp [ok] at h₃
   <;> have ⟨h₃, h₄⟩ := h₃

cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean

@@ -76,11 +76,11 @@ inductive InstanceOfType (env : TypeEnv) : Value → CedarType → Prop where
       (h₁ : InstanceOfExtType x xty) :
       InstanceOfType env (.ext x) (.ext xty)
 
-def InstanceOfRequestType (request : Request) (env : TypeEnv) : Prop :=
-  InstanceOfEntityType request.principal env.reqty.principal env ∧
-  request.action = env.reqty.action ∧
-  InstanceOfEntityType request.resource env.reqty.resource env ∧
-  InstanceOfType env request.context (.record env.reqty.context)
+def InstanceOfTypeEnv (request : Request) (env : TypeEnv) : Prop :=
+  InstanceOfEntityType request.principal env.sig.principal env ∧
+  request.action = env.sig.action ∧
+  InstanceOfEntityType request.resource env.sig.resource env ∧
+  InstanceOfType env request.context (.record env.sig.context)
 
 def InstanceOfEntityTags (data : EntityData) (entry : EntitySchemaEntry) (env : TypeEnv) : Prop :=
   match entry.tags? with
@@ -138,7 +138,7 @@ def InstanceOfSchema (entities : Entities) (env : TypeEnv) : Prop :=
 
 def InstanceOfWellFormedEnvironment (request : Request) (entities : Entities) (env : TypeEnv) : Prop :=
   env.WellFormed ∧
-  InstanceOfRequestType request env ∧
+  InstanceOfTypeEnv request env ∧
   InstanceOfSchema entities env
 
 ----- Theorems -----