Skip to content

Commit

Permalink
track max level for more precise checking on guard expr
Browse files Browse the repository at this point in the history 
Signed-off-by: John Kastner <jkastner@amazon.com>
  • Loading branch information
@john-h-kastner-aws
john-h-kastner-aws committed Feb 28, 2025
1 parent 0c5f025 commit 5ca2602
Show file tree
Hide file tree
Showing 14 changed files with 208 additions and 171 deletions.
3 changes: 3 additions & 0 deletions cedar-lean/Cedar/Spec/Entities.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,9 @@ def Entities.tagsOrEmpty (es : Entities) (uid : EntityUID) : Map Tag Value :=
| some d => d.tags
| none => Map.empty

def Entities.remove (es : Entities) (uid : EntityUID) : Entities :=
es.filter (λ uid' _ => uid == uid')

----- Derivations -----

deriving instance Repr, DecidableEq, Inhabited for EntityData
Expand Down
25 changes: 13 additions & 12 deletions cedar-lean/Cedar/Thm/Validation/Levels.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,13 @@ open Cedar.Data
open Cedar.Spec
open Cedar.Validation

theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
(hs : slice = entities.sliceAtLevel request n)
theorem level_based_slicing_is_sound_expr {e : Expr} {n nmax : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
(hn : nmax ≥ n)
(hs : slice = entities.sliceAtLevel request nmax)
(hc : CapabilitiesInvariant c request entities)
(hr : RequestAndEntitiesMatchEnvironment env request entities)
(ht : typeOf e c env = Except.ok (tx, c₁))
(hl : TypedExpr.AtLevel tx n) :
(hl : TypedExpr.AtLevel tx n nmax) :
evaluate e request entities = evaluate e request slice
:= by
cases e
Expand All @@ -52,28 +53,28 @@ theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr}
have ihc := @level_based_slicing_is_sound_expr c
have iht := @level_based_slicing_is_sound_expr t
have ihe := @level_based_slicing_is_sound_expr e
exact level_based_slicing_is_sound_if hs hc hr ht hl ihc iht ihe
exact level_based_slicing_is_sound_if hn hs hc hr ht hl ihc iht ihe
case and e₁ e₂ =>
have ih₁ := @level_based_slicing_is_sound_expr e₁
have ih₂ := @level_based_slicing_is_sound_expr e₂
exact level_based_slicing_is_sound_and hs hc hr ht hl ih₁ ih₂
exact level_based_slicing_is_sound_and hn hs hc hr ht hl ih₁ ih₂
case or e₁ e₂ =>
have ih₁ := @level_based_slicing_is_sound_expr e₁
have ih₂ := @level_based_slicing_is_sound_expr e₂
exact level_based_slicing_is_sound_or hs hc hr ht hl ih₁ ih₂
exact level_based_slicing_is_sound_or hn hs hc hr ht hl ih₁ ih₂
case unaryApp op e =>
have ihe := @level_based_slicing_is_sound_expr e
exact level_based_slicing_is_sound_unary_app hs hc hr ht hl ihe
exact level_based_slicing_is_sound_unary_app hn hs hc hr ht hl ihe
case binaryApp op e₁ e₂ =>
have ihe₁ := @level_based_slicing_is_sound_expr e₁
have ihe₂ := @level_based_slicing_is_sound_expr e₂
exact level_based_slicing_is_sound_binary_app hs hc hr ht hl ihe₁ ihe₂
exact level_based_slicing_is_sound_binary_app hn hs hc hr ht hl ihe₁ ihe₂
case getAttr e _ =>
have ihe := @level_based_slicing_is_sound_expr e
exact level_based_slicing_is_sound_get_attr hs hc hr ht hl ihe
exact level_based_slicing_is_sound_get_attr hn hs hc hr ht hl ihe
case hasAttr e _ =>
have ihe := @level_based_slicing_is_sound_expr e
exact level_based_slicing_is_sound_has_attr hs hc hr ht hl ihe
exact level_based_slicing_is_sound_has_attr hn hs hc hr ht hl ihe
case set xs =>
replace ⟨ hc, txs, ty, htx, ht ⟩ := type_of_set_inversion ht
subst tx
Expand All @@ -92,7 +93,7 @@ theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr}
simp only [Expr.record.sizeOf_spec]
omega
exact @level_based_slicing_is_sound_expr x.snd
exact level_based_slicing_is_sound_record hs hc hr ht hl ih
exact level_based_slicing_is_sound_record hn hs hc hr ht hl ih
termination_by e

theorem level_based_slicing_is_sound {p : Policy} {n : Nat} {env : Environment} {request : Request} {entities slice : Entities}
Expand All @@ -108,4 +109,4 @@ theorem level_based_slicing_is_sound {p : Policy} {n : Nat} {env : Environment}
)
rw [←level_spec] at htl
have hc := empty_capabilities_invariant request entities
exact level_based_slicing_is_sound_expr hs hc hr ht htl
exact level_based_slicing_is_sound_expr (by omega) hs hc hr ht htl
11 changes: 6 additions & 5 deletions cedar-lean/Cedar/Thm/Validation/Levels/And.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,12 @@ open Cedar.Spec
open Cedar.Validation

theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
(hs : slice = entities.sliceAtLevel request n)
(hn : nmax ≥ n)
(hs : slice = entities.sliceAtLevel request nmax)
(hc : CapabilitiesInvariant c₀ request entities)
(hr : RequestAndEntitiesMatchEnvironment env request entities)
(ht : typeOf (.and e₁ e₂) c₀ env = Except.ok (tx, c₁))
(hl : TypedExpr.AtLevel tx n)
(hl : TypedExpr.AtLevel tx n nmax)
(ih₁ : TypedAtLevelIsSound e₁)
(ih₂ : TypedAtLevelIsSound e₂)
: evaluate (.and e₁ e₂) request entities = evaluate (.and e₁ e₂) request slice
Expand All @@ -54,7 +55,7 @@ theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁
replace hv₁ := instance_of_ff_is_false hv₁
subst v₁
cases hl ; rename_i hl₁
specialize ih₁ hs hc hr htx₁ (by assumption)
specialize ih₁ hn hs hc hr htx₁ (by assumption)
simp only [evaluate, ←ih₁]
rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
simp [he₁, Result.as, Coe.coe, Value.asBool]
Expand All @@ -63,11 +64,11 @@ theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁
replace ⟨ b₁ , hv₁⟩ := instance_of_bool_is_bool hv₁
subst v₁ tx
cases hl ; rename_i hl₁ hl₂
specialize ih₁ hs hc hr htx₁ hl₁
specialize ih₁ hn hs hc hr htx₁ hl₁
simp only [evaluate, ←ih₁]
rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
simp only [he₁, Result.as, Bool.not_eq_eq_eq_not, Bool.not_true, Coe.coe, Value.asBool, Except.bind_err]
cases b₁ <;> simp only [Except.bind_ok, ↓reduceIte]
specialize hgc he₁
specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂ hl₂
specialize ih₂ hn hs (capability_union_invariant hc hgc) hr htx₂ hl₂
simp [ih₂]
7 changes: 4 additions & 3 deletions cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,11 @@ Basic definitions for levels proof
open Cedar.Spec
open Cedar.Validation

def TypedAtLevelIsSound (e : Expr) : Prop := ∀ {n : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env :Environment} {request : Request} {entities slice : Entities},
slice = entities.sliceAtLevel request n →
def TypedAtLevelIsSound (e : Expr) : Prop := ∀ {n nmax : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env :Environment} {request : Request} {entities slice : Entities},
nmax >= n →
slice = entities.sliceAtLevel request nmax→
CapabilitiesInvariant c request entities →
RequestAndEntitiesMatchEnvironment env request entities →
typeOf e c env = Except.ok (tx, c₁) →
TypedExpr.AtLevel tx n →
TypedExpr.AtLevel tx n nmax →
evaluate e request entities = evaluate e request slice
34 changes: 21 additions & 13 deletions cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,27 +45,32 @@ theorem not_dereferencing_apply₂_invariant_entities {op : BinaryOp} {entities
cases p₁ <;> cases p₂ <;> simp
)

theorem level_based_slicing_is_sound_inₑ {e₁ : Expr} {euid₁ euid₂ : EntityUID} {n : Nat} {c₀ c₁ : Capabilities} {entities slice : Entities}
theorem level_based_slicing_is_sound_inₑ {e₁ : Expr} {euid₁ euid₂ : EntityUID} {n nmax : Nat} {c₀ c₁ : Capabilities} {entities slice : Entities}
(hn : nmax ≥ n + 1)
(hc : CapabilitiesInvariant c₀ request entities)
(hr : RequestAndEntitiesMatchEnvironment env request entities)
(ht : typeOf e₁ c₀ env = Except.ok (tx₁, c₁))
(hl : TypedExpr.AtLevel tx₁ n)
(hl : TypedExpr.AtLevel tx₁ n nmax)
(hel : ¬ TypedExpr.EntityLitViaPath tx₁ [])
(he : evaluate e₁ request entities = .ok (Value.prim (Prim.entityUID euid₁)))
(hs : some slice = entities.sliceAtLevel request (n + 1))
(hs : some slice = entities.sliceAtLevel request nmax)
: inₑ euid₁ euid₂ entities = inₑ euid₁ euid₂ slice
:= by
simp only [inₑ]
cases heq : euid₁ == euid₂ <;> simp only [Bool.false_or, Bool.true_or]
replace hl : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
check_level_greater (by omega) hl
rw [(by simp at hn ; omega : nmax = nmax - 1 + 1)] at hs
have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl hel he hs
simp [hfeq, Entities.ancestorsOrEmpty]

theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
(hs : slice = entities.sliceAtLevel request n)
(hn : nmax ≥ n)
(hs : slice = entities.sliceAtLevel request nmax)
(hc : CapabilitiesInvariant c₀ request entities)
(hr : RequestAndEntitiesMatchEnvironment env request entities)
(ht : typeOf (.binaryApp op e₁ e₂) c₀ env = Except.ok (tx, c₁))
(hl : TypedExpr.AtLevel tx n)
(hl : TypedExpr.AtLevel tx n nmax)
(ihe₁ : TypedAtLevelIsSound e₁)
(ihe₂ : TypedAtLevelIsSound e₂)
: evaluate (.binaryApp op e₁ e₂) request entities = evaluate (.binaryApp op e₁ e₂) request slice
Expand All @@ -75,10 +80,10 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
simp only [evaluate]
cases hl
case getTag hel hl₁ hl₂ | hasTag hel hl₁ hl₂ =>
specialize ihe₂ hs hc hr htx₂ hl₂
specialize ihe₂ (by omega) hs hc hr htx₂ hl₂
rw [←ihe₂]
have hl₁' := check_level_succ hl₁
specialize ihe₁ hs hc hr htx₁ hl₁'
specialize ihe₁ hn hs hc hr htx₁ hl₁'
rw [←ihe₁]
cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err]
cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err]
Expand All @@ -87,13 +92,16 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
rename_i p₁ p₂
cases p₁ <;> cases p₂ <;> simp only
rename_i euid _
replace hl₁ : TypedExpr.AtLevel tx₁ (nmax - 1) nmax :=
check_level_greater (by omega) hl₁
rw [(by simp at hn ; omega : nmax = nmax - 1 + 1)] at hs
have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr htx₁ hl₁ hel he₁ hs
simp only [hfeq, hasTag, getTag, Entities.tagsOrEmpty, Entities.tags, Map.findOrErr]
case mem hel hl₁ hl₂ =>
specialize ihe₂ hs hc hr htx₂ hl₂
specialize ihe₂ (by omega) hs hc hr htx₂ hl₂
rw [←ihe₂]
have hl₁' := check_level_succ hl₁
specialize ihe₁ hs hc hr htx₁ hl₁'
specialize ihe₁ hn hs hc hr htx₁ hl₁'
rw [←ihe₁]
cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err]
cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err]
Expand All @@ -102,13 +110,13 @@ theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {e₁ e₂ : Exp
case prim =>
rename_i p₁ p₂
cases p₁ <;> cases p₂ <;> simp only
simp [level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ hel he₁ hs]
simp [level_based_slicing_is_sound_inₑ hn hc hr htx₁ hl₁ hel he₁ hs]
case set =>
rename_i p₁ sv
cases p₁ <;> simp only
simp [inₛ, level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ hel he₁ hs]
simp [inₛ, level_based_slicing_is_sound_inₑ hn hc hr htx₁ hl₁ hel he₁ hs]
case binaryApp hop hl₁ hl₂ =>
specialize ihe₁ hs hc hr htx₁ hl₁
specialize ihe₂ hs hc hr htx₂ hl₂
specialize ihe₁ hn hs hc hr htx₁ hl₁
specialize ihe₂ hn hs hc hr htx₂ hl₂
rw [ihe₁, ihe₂]
simp [(@not_dereferencing_apply₂_invariant_entities op entities slice · · hop)]
129 changes: 68 additions & 61 deletions cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,77 +151,77 @@ def DereferencingBinaryOp : BinaryOp → Prop
| .mem | .hasTag | .getTag => True
| _ => False

inductive TypedExpr.AtLevel : TypedExpr → Nat → Prop where
| lit (p : Prim) (ty : CedarType) (n : Nat) :
AtLevel (.lit p ty) n
| var (v : Var) (ty : CedarType) (n : Nat) :
AtLevel (.var v ty) n
| ite (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ n)
(hl₃ : AtLevel tx₃ n) :
AtLevel (.ite tx₁ tx₂ tx₃ ty) n
| and (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ n) :
AtLevel (.and tx₁ tx₂ ty) n
inductive TypedExpr.AtLevel : TypedExpr → Nat → Nat → Prop where
| lit (p : Prim) (ty : CedarType) (n nmax : Nat) :
AtLevel (.lit p ty) n nmax
| var (v : Var) (ty : CedarType) (n nmax : Nat) :
AtLevel (.var v ty) n nmax
| ite (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(hl₁ : AtLevel tx₁ nmax nmax)
(hl₂ : AtLevel tx₂ n nmax)
(hl₃ : AtLevel tx₃ n nmax) :
AtLevel (.ite tx₁ tx₂ tx₃ ty) n nmax
| and (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ n nmax) :
AtLevel (.and tx₁ tx₂ ty) n nmax
| or (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ n) :
AtLevel (.or tx₁ tx₂ ty) n
| unaryApp (op : UnaryOp) (tx₁ : TypedExpr) (ty : CedarType)
(hl₁ : AtLevel tx₁ n) :
AtLevel (.unaryApp op tx₁ ty) n
| mem (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ n nmax) :
AtLevel (.or tx₁ tx₂ ty) n nmax
| unaryApp (op : UnaryOp) (tx₁ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(hl₁ : AtLevel tx₁ n nmax) :
AtLevel (.unaryApp op tx₁ ty) n nmax
| mem (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(he : ¬ EntityLitViaPath tx₁ [])
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ (n + 1)) :
AtLevel (.binaryApp .mem tx₁ tx₂ ty) (n + 1)
| getTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ nmax nmax) :
AtLevel (.binaryApp .mem tx₁ tx₂ ty) (n + 1) nmax
| getTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(he : ¬ EntityLitViaPath tx₁ [])
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ (n + 1)) :
AtLevel (.binaryApp .getTag tx₁ tx₂ ty) (n + 1)
| hasTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ nmax nmax) :
AtLevel (.binaryApp .getTag tx₁ tx₂ ty) (n + 1) nmax
| hasTag (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat)
(he : ¬ EntityLitViaPath tx₁ [])
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ (n + 1)) :
AtLevel (.binaryApp .hasTag tx₁ tx₂ ty) (n + 1)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ nmax nmax) :
AtLevel (.binaryApp .hasTag tx₁ tx₂ ty) (n + 1) nmax
| binaryApp (op : BinaryOp) (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat)
(hop : ¬ DereferencingBinaryOp op)
(hl₁ : AtLevel tx₁ n)
(hl₂ : AtLevel tx₂ n) :
AtLevel (.binaryApp op tx₁ tx₂ ty) n
| getAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hl₂ : AtLevel tx₂ n nmax) :
AtLevel (.binaryApp op tx₁ tx₂ ty) n nmax
| getAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n nmax : Nat)
(he : ¬ EntityLitViaPath tx₁ [])
(hl₁ : AtLevel tx₁ n)
(hl₁ : AtLevel tx₁ n nmax)
(hty : tx₁.typeOf = .entity ety) :
AtLevel (.getAttr tx₁ a ty) (n + 1)
| hasAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n : Nat)
AtLevel (.getAttr tx₁ a ty) (n + 1) nmax
| hasAttr (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) {ety : EntityType} (n nmax : Nat)
(he : ¬ EntityLitViaPath tx₁ [])
(hl₁ : AtLevel tx₁ n)
(hl₁ : AtLevel tx₁ n nmax)
(hty : tx₁.typeOf = .entity ety) :
AtLevel (.hasAttr tx₁ a ty) (n + 1)
| getAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n)
AtLevel (.hasAttr tx₁ a ty) (n + 1) nmax
| getAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n nmax : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hty : ∀ ety, tx₁.typeOf ≠ .entity ety) :
AtLevel (.getAttr tx₁ a ty) n
| hasAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n : Nat)
(hl₁ : AtLevel tx₁ n)
AtLevel (.getAttr tx₁ a ty) n nmax
| hasAttrRecord (tx₁ : TypedExpr) (a : Attr) (ty : CedarType) (n nmax : Nat)
(hl₁ : AtLevel tx₁ n nmax)
(hty : ∀ ety, tx₁.typeOf ≠ .entity ety) :
AtLevel (.hasAttr tx₁ a ty) n
| set (txs : List TypedExpr) (ty : CedarType) (n : Nat)
(hl : ∀ tx ∈ txs, AtLevel tx n) :
AtLevel (.set txs ty) n
| record (attrs : List (Attr × TypedExpr)) (ty : CedarType)
(hl : ∀ atx ∈ attrs, AtLevel atx.snd n) :
AtLevel (.record attrs ty) n
| call (xfn : ExtFun) (args : List TypedExpr) (ty : CedarType)
(hl : ∀ tx ∈ args, AtLevel tx n) :
AtLevel (.call xfn args ty) n
AtLevel (.hasAttr tx₁ a ty) n nmax
| set (txs : List TypedExpr) (ty : CedarType) (n nmax : Nat)
(hl : ∀ tx ∈ txs, AtLevel tx n nmax) :
AtLevel (.set txs ty) n nmax
| record (attrs : List (Attr × TypedExpr)) (ty : CedarType) (n nmax : Nat)
(hl : ∀ atx ∈ attrs, AtLevel atx.snd n nmax) :
AtLevel (.record attrs ty) n nmax
| call (xfn : ExtFun) (args : List TypedExpr) (ty : CedarType) (n nmax : Nat)
(hl : ∀ tx ∈ args, AtLevel tx n nmax) :
AtLevel (.call xfn args ty) n nmax

theorem level_spec {tx : TypedExpr} {n : Nat}:
(TypedExpr.AtLevel tx n ) ↔ (checkLevel tx n = true)
theorem level_spec {tx : TypedExpr} {n nmax : Nat}:
(TypedExpr.AtLevel tx n nmax) ↔ (checkLevel tx n nmax = true)
:= by
cases tx
case lit =>
Expand Down Expand Up @@ -378,9 +378,10 @@ theorem level_spec {tx : TypedExpr} {n : Nat}:
exact h₁
termination_by tx

theorem check_level_succ {tx : TypedExpr} {n : Nat}
(h₁ : TypedExpr.AtLevel tx n) :
TypedExpr.AtLevel tx (n + 1)

theorem check_level_succ {tx : TypedExpr} {n nmax : Nat}
(h₁ : TypedExpr.AtLevel tx n nmax) :
TypedExpr.AtLevel tx (n + 1) nmax
:= by
cases h₁
case call htx | set htx =>
Expand Down Expand Up @@ -409,3 +410,9 @@ theorem check_level_succ {tx : TypedExpr} {n : Nat}
try apply check_level_succ
try assumption
)

theorem check_level_greater {tx : TypedExpr} {n n' nmax : Nat}
(hn : n ≤ n')
(h₁ : TypedExpr.AtLevel tx n nmax) :
TypedExpr.AtLevel tx n' nmax
:= Nat.le.rec h₁ (λ _ ih => check_level_succ ih) hn
Loading

0 comments on commit 5ca2602

Please sign in to comment.