diff --git a/cedar-lean/Cedar/Thm/Translation.lean b/cedar-lean/Cedar/Thm/Translation.lean index 550148a93..c4e7e0a52 100644 --- a/cedar-lean/Cedar/Thm/Translation.lean +++ b/cedar-lean/Cedar/Thm/Translation.lean @@ -53,14 +53,11 @@ theorem policy_satisfied_agrees (cp : Cst.Policy) (ap : Spec.Policy) Cst.satisfied cp req es = satisfied ap req es := by intro htrans obtain ⟨ae, hae⟩ := toPolicy?_implies_toAExpr? htrans - have h1 : evaluate ae req es = .ok (↑true : Value) ↔ cp.toExpr.evaluate req es = .ok (↑true : Value) := by - rw [expr_to_expr_sound hae] - have h2 := policy_to_expr_agrees cp ap cp.toExpr ae req es htrans rfl hae (val := (↑true : Value)) - have hiff : cp.toExpr.evaluate req es = .ok ↑true ↔ evaluate ap.toExpr req es = .ok ↑true := - ⟨fun hcst => h2.mp (h1.mpr hcst), fun hast => h1.mp (h2.mpr hast)⟩ + have heq : cp.toExpr.evaluate req es = evaluate ap.toExpr req es := + (expr_to_expr_sound hae).symm.trans + (policy_to_expr_sound cp ap cp.toExpr ae req es htrans rfl hae) unfold Cst.satisfied satisfied - simp only [show (cp.toExpr.evaluate req es = .ok ↑true) = (evaluate ap.toExpr req es = .ok ↑true) - from propext hiff] + rw [heq] /-- Under a successful translation, `extractScope?` succeeds, so the new scope guard in `Cst.hasError` is a no-op and it reduces to the plain @@ -86,20 +83,11 @@ theorem policy_hasError_agrees (cp : Cst.Policy) (ap : Spec.Policy) Cst.hasError cp req es = hasError ap req es := by intro htrans obtain ⟨ae, hae⟩ := toPolicy?_implies_toAExpr? htrans - have h1 : ∀ v, evaluate ae req es = .ok v ↔ cp.toExpr.evaluate req es = .ok v := - fun v => by rw [expr_to_expr_sound hae] - have h2 : ∀ v, evaluate ae req es = .ok v ↔ evaluate ap.toExpr req es = .ok v := - policy_to_expr_agrees cp ap cp.toExpr ae req es htrans rfl hae - have hiff : ∀ v, cp.toExpr.evaluate req es = .ok v ↔ evaluate ap.toExpr req es = .ok v := - fun v => ⟨fun hcst => (h2 v).mp ((h1 v).mpr hcst), fun hast => (h1 v).mp ((h2 v).mpr hast)⟩ - rw [cst_hasError_eq_of_toPolicy htrans] - unfold hasError - cases hcst : cp.toExpr.evaluate req es with - | ok v => rw [(hiff v).mp hcst] - | error e => - cases hast : evaluate ap.toExpr req es with - | ok v => rw [(hiff v).mpr hast] at hcst; cases hcst - | error e' => rfl + have heq : cp.toExpr.evaluate req es = evaluate ap.toExpr req es := + (expr_to_expr_sound hae).symm.trans + (policy_to_expr_sound cp ap cp.toExpr ae req es htrans rfl hae) + rw [cst_hasError_eq_of_toPolicy htrans, heq] + rfl /-- Per-policy agreement of the error check. -/ theorem policy_errored_agrees (cp : Cst.Policy) (ap : Spec.Policy) @@ -176,7 +164,6 @@ theorem translation_is_sound (cps : Cst.Policies) (aps : Spec.Policies) theorem noHasError_translates (cp : Cst.Policy) (req : Request) (es : Entities) : ¬ Cst.hasError cp req es → ∃ ap, cp.toPolicy? = ap := by simp - -- I don't know why simp solves this goal theorem translation_is_complete (cps : Cst.Policies) (req : Request) (es : Entities) : ∀ cp ∈ cps.ps, cp.id ∉ (Cst.isAuthorized req es cps).erroringPolicies → diff --git a/cedar-lean/Cedar/Thm/Translation/Aux.lean b/cedar-lean/Cedar/Thm/Translation/Aux.lean index 22b1148b2..deee4f0bd 100644 --- a/cedar-lean/Cedar/Thm/Translation/Aux.lean +++ b/cedar-lean/Cedar/Thm/Translation/Aux.lean @@ -16,23 +16,6 @@ theorem toExtFun?_some_isFunctionName {s : String} {xfn : ExtFun} simp only [CstCommon.String.toExtFun?] at h split at h <;> simp_all [CstCommon.String.isFunctionName?] -theorem ExprOrSpecial.toExpr?_none (eos : ExprOrSpecial) : - eos.toExpr? = none → - (∃ s, eos = .strLit s ∧ CstCommon.unescape? s = none) ∨ - (∃ n, eos = .name n) := by - intro h - match eos with - | .expr e => simp [ExprOrSpecial.toExpr?] at h - | .var v => simp [ExprOrSpecial.toExpr?] at h - | .boolLit b => simp [ExprOrSpecial.toExpr?] at h - | .strLit s => - left; exists s; constructor - · rfl - · match hs : CstCommon.unescape? s with - | none => rfl - | some s' => simp [ExprOrSpecial.toExpr?, hs] at h - | .name n => right; exists n - /- For Primary -/ theorem Cst.Ident.toUnrestrictedString?_eq_toString @@ -359,22 +342,7 @@ theorem dashN_evaluate_general /- For Relation -/ -/-- The AST expression `constructExprRel op e₁ e₂` evaluates to the same `.ok` - output as `Cst.applyRelOp op v₁ v₂ es`, when `e₁` evaluates to `v₁` and - `e₂` evaluates to `v₂`. -/ -theorem constructExprRel_applyRelOp_agrees - (op : Cst.RelOp) (e₁ e₂ : Expr) (req : Request) (es : Entities) - (v₁ v₂ : Value) : - evaluate e₁ req es = .ok v₁ → - evaluate e₂ req es = .ok v₂ → - ∀ v, evaluate (constructExprRel op e₁ e₂) req es = .ok v ↔ - Cst.applyRelOp op v₁ v₂ es = .ok v := by - intro he₁ he₂ v - cases op <;> - simp [constructExprRel, Cst.applyRelOp, evaluate, he₁, he₂, - bind, Except.bind] - -/-- Equality version of `constructExprRel_applyRelOp_agrees`. -/ +/-- `constructExprRel op e₁ e₂` and the applied relational op evaluate equally. -/ theorem constructExprRel_applyRelOp_eq (op : Cst.RelOp) (e₁ e₂ : Expr) (req : Request) (es : Entities) (v₁ v₂ : Value) : @@ -637,15 +605,6 @@ theorem addExpr_toAttrs_toHasRhs {e : Cst.AddExpr} {attrs : List Attr} : | idIn | idHas | idLike | idIs | idIf | idThen | idElse => simp [Cst.Ident.toHasHead?] at hhh | ref _ | expr _ | eList _ | rInits _ => simp at h -/-- Helper: `constructAttrs?` always returns a non-empty list when it succeeds. -/ -theorem constructAttrs?_nonempty - {first : String} {rest : List Cst.MemAccess} {result : List String} : - constructAttrs? first rest = some result → result ≠ [] := by - intro h - simp [constructAttrs?, Option.bind_eq_some_iff] at h - obtain ⟨tail, _, hresult⟩ := h - simp [← hresult] - /-- `toAttrs?` always produces a non-empty list when it succeeds: the result is either `[unescaped_lit]` or `head :: fields`. -/ theorem toAttrs?_nonempty {e : Cst.AddExpr} {fs : List Attr} : @@ -772,18 +731,6 @@ private theorem memberAux_expr_eq (e : Expr) (accs : List AstAccessor) : | nil => rfl | cons acc rest => rfl -/-- Helper: when `memberAux` takes an `.expr ...` input, it always returns - either `.expr ...` or `none` — never another `ExprOrSpecial` constructor. -/ -private theorem memberAux_expr_returns_expr - (e : Expr) (accs : List AstAccessor) (ret : ExprOrSpecial) : - memberAux (.expr e) accs = some ret → - ∃ e', ret = .expr e' := by - intro h - rw [memberAux_expr_eq] at h - simp only [Option.bind_eq_some_iff] at h - obtain ⟨e', _, hret⟩ := h - exact ⟨e', (Option.some.inj hret).symm⟩ - /-- On a non-empty accessor list, `memberAuxA` never returns `.inl` — the `.inl` (pass-through) result only arises for the empty accessor list. -/ private theorem memberAuxA_cons_ne_inl @@ -1133,72 +1080,6 @@ private theorem memberAuxB_field_index (he : Expr) (id : Cst.Ident) (id2 : Strin memberAuxB he (.field id :: .index id2 :: rest2) = memberAuxB (.getAttr he (CstCommon.Ident.toString id)) (.index id2 :: rest2) := rfl -/-- If a method-call translation succeeds and its receiver expression errors, - the resulting expression errors. -/ -private theorem toMeth?_eval_error - {req : Request} {es : Entities} {id : Cst.Ident} {he head' : Expr} - {args : List Expr} {err : Error} - (hm : Cst.Ident.toMeth? id he args = some head') - (herr : evaluate he req es = .error err) : - ∃ err', evaluate head' req es = .error err' := by - cases id with - | idIdent s => - cases hop : CstCommon.String.toMethodOp? s with - | none => simp [Cst.Ident.toMeth?, hop] at hm - | some op => - cases op with - | inl bop => - cases args with - | nil => simp [Cst.Ident.toMeth?, hop, oneArg?] at hm - | cons a as => - cases as with - | cons _ _ => simp [Cst.Ident.toMeth?, hop, oneArg?] at hm - | nil => - simp [Cst.Ident.toMeth?, hop, oneArg?] at hm - subst hm - exact ⟨err, by simp [evaluate, herr, bind, Except.bind]⟩ - | inr uop => - cases hargs : args.isEmpty with - | false => simp [Cst.Ident.toMeth?, hop, hargs] at hm - | true => - simp [Cst.Ident.toMeth?, hop, hargs] at hm - subst hm - exact ⟨err, by simp [evaluate, herr, bind, Except.bind]⟩ - | _ => simp [Cst.Ident.toMeth?] at hm - -/-- If the head expression of an AST member-access spine errors, so does the - whole spine. -/ -theorem memberAuxB_eval_error - {req : Request} {es : Entities} : - (accs : List AstAccessor) → (he bexp : Expr) → (err : Error) → - memberAuxB he accs = some bexp → evaluate he req es = .error err → - ∃ err', evaluate bexp req es = .error err' - | [], _, bexp, err, hb, herr => by - simp only [memberAuxB, Option.some.injEq] at hb; subst hb; exact ⟨err, herr⟩ - | .call args :: rest, _, bexp, _, hb, _ => by - simp [memberAuxB] at hb - | .index id :: rest, he, bexp, err, hb, herr => by - rw [memberAuxB_index] at hb - exact memberAuxB_eval_error rest _ bexp err hb (by simp [evaluate, herr, bind, Except.bind]) - | .field id :: [], he, bexp, err, hb, herr => by - rw [memberAuxB_field_nil] at hb; simp only [Option.some.injEq] at hb; subst hb - exact ⟨err, by simp [evaluate, herr, bind, Except.bind]⟩ - | .field id :: .call args :: rest2, he, bexp, err, hb, herr => by - rw [memberAuxB_field_call, Option.bind_eq_some_iff] at hb - obtain ⟨head', hmeth, hrec⟩ := hb - obtain ⟨err', herr'⟩ := toMeth?_eval_error hmeth herr - exact memberAuxB_eval_error rest2 head' bexp err' hrec herr' - | .field id :: .field id2 :: rest2, he, bexp, err, hb, herr => by - rw [memberAuxB_field_field] at hb - exact memberAuxB_eval_error (.field id2 :: rest2) _ bexp err hb - (by simp [evaluate, herr, bind, Except.bind]) - | .field id :: .index id2 :: rest2, he, bexp, err, hb, herr => by - rw [memberAuxB_field_index] at hb - exact memberAuxB_eval_error (.index id2 :: rest2) _ bexp err hb - (by simp [evaluate, herr, bind, Except.bind]) -termination_by accs => accs.length -decreasing_by all_goals (simp_wf <;> omega) - /-- Bridge: collapsing `memberAux` of a (non-name) head through `toExpr?` equals running `memberAuxB` on the collapsed head expression. -/ theorem memberAux_toExpr_eq @@ -1257,34 +1138,7 @@ theorem memberAux_toExpr_eq simp [memberAux, memberAuxA, memberAuxB_field_index] cases memberAuxB (Expr.getAttr (.var v) (CstCommon.Ident.toString id)) (.index id2 :: rest2) <;> rfl -/-- One step of the member-access agreement. `he'` is the AST expression for - this step's new head; `cstStep` is the evaluator's result for it. They need - only agree on `ok` results (method arguments agree only on `ok`). -/ -theorem evalAccessors_step - {req : Request} {es : Entities} {he' bexp : Expr} {cstStep : Result Value} - {rest_cst : List Cst.MemAccess} {rest_ast : List AstAccessor} - (hstep : ∀ w, evaluate he' req es = .ok w ↔ cstStep = .ok w) - (hbrec : memberAuxB he' rest_ast = some bexp) - (htail : ∀ hv', evaluate he' req es = .ok hv' → - ∀ v, evaluate bexp req es = .ok v ↔ Cst.Member.evalAccessors hv' rest_cst req es = .ok v) : - ∀ v, evaluate bexp req es = .ok v ↔ - (do let hv ← cstStep; Cst.Member.evalAccessors hv rest_cst req es) = .ok v := by - intro v - cases hcs : cstStep with - | error e => - have hge : ∃ e'', evaluate he' req es = .error e'' := by - cases h : evaluate he' req es with - | error e'' => exact ⟨e'', rfl⟩ - | ok w => exact absurd ((hstep w).mp h) (by rw [hcs]; simp) - obtain ⟨e'', hge⟩ := hge - obtain ⟨e', he'eq⟩ := memberAuxB_eval_error rest_ast he' bexp e'' hbrec hge - simp [he'eq, bind, Except.bind] - | ok hv' => - have hge : evaluate he' req es = .ok hv' := (hstep hv').mpr hcs - rw [htail hv' hge v] - exact Iff.rfl - -/-- Same-error version of `toMeth?_eval_error`: the method application +/-- When a method-call translation's receiver errors, the method application propagates the head error *unchanged*. -/ private theorem toMeth?_eval_error_eq {req : Request} {es : Entities} {id : Cst.Ident} {he head' : Expr} @@ -1317,8 +1171,8 @@ private theorem toMeth?_eval_error_eq simp [evaluate, herr, bind, Except.bind] | _ => simp [Cst.Ident.toMeth?] at hm -/-- Same-error version of `memberAuxB_eval_error`: when the head errors, the - whole `memberAuxB`-built expression errors with the *same* error. -/ +/-- When the head errors, the whole `memberAuxB`-built expression errors with + the *same* error. -/ theorem memberAuxB_eval_error_eq {req : Request} {es : Entities} : (accs : List AstAccessor) → (he bexp : Expr) → (err : Error) → @@ -1349,7 +1203,7 @@ theorem memberAuxB_eval_error_eq termination_by accs => accs.length decreasing_by all_goals (simp_wf <;> omega) -/-- Equality version of `evalAccessors_step`. -/ +/-- One step of the member-access agreement, as an evaluation equality. -/ theorem evalAccessors_step_eq {req : Request} {es : Entities} {he' bexp : Expr} {cstStep : Result Value} {rest_cst : List Cst.MemAccess} {rest_ast : List AstAccessor} @@ -1400,196 +1254,8 @@ private theorem mapM_toAst_index_head {ex2 : Cst.Expr} {rest2 : List Cst.MemAcce obtain ⟨s2, _, rfl⟩ := ha2 exact ⟨_, _, rfl⟩ -/-- Core member-access agreement: the AST built by `memberAuxB` over a head - expression `headExpr` evaluates in agreement (on `ok` results) with the CST - evaluator `Member.evalAccessors` run on the same accessors, provided the - head expression evaluates to the head value and every argument - sub-expression agrees (the latter supplied by the mutual `Expr` induction). -/ -theorem evalAccessors_agrees - {req : Request} {es : Entities} : - (accs_cst : List Cst.MemAccess) → (accs_ast : List AstAccessor) → - (headExpr bexp : Expr) → (head : Value) → - accs_cst.mapM Cst.MemAccess.toAstAccessor? = some accs_ast → - memberAuxB headExpr accs_ast = some bexp → - evaluate headExpr req es = .ok head → - (∀ ce : Cst.Expr, sizeOf ce < sizeOf accs_cst → ∀ ax, ce.toAExpr? = some ax → - ∀ w, evaluate ax req es = .ok w ↔ ce.evaluate req es = .ok w) → - ∀ v, evaluate bexp req es = .ok v ↔ Cst.Member.evalAccessors head accs_cst req es = .ok v - | [], accs_ast, headExpr, bexp, head, htrans, hb, hhead, _ => by - intro v - simp at htrans; subst htrans - simp only [memberAuxB, Option.some.injEq] at hb; subst hb - rw [hhead]; simp [Cst.Member.evalAccessors] - | .call args :: rest, accs_ast, headExpr, bexp, head, htrans, hb, hhead, _ => by - intro v - rw [List.mapM_cons] at htrans - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, rest_ast, _, rfl⟩ := htrans - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨xs, _, rfl⟩ := ha_ast - simp [memberAuxB] at hb - | .index ex :: rest, accs_ast, headExpr, bexp, head, htrans, hb, hhead, harg => by - intro v - rw [List.mapM_cons] at htrans - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, rest_ast, hrest, rfl⟩ := htrans - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨s, hs, rfl⟩ := ha_ast - rw [memberAuxB_index] at hb - have hev : Cst.Member.evalAccessors head (.index ex :: rest) req es - = (do let hv ← getAttr head s es; Cst.Member.evalAccessors hv rest req es) := by - simp [Cst.Member.evalAccessors, hs] - rw [hev] - exact evalAccessors_step (he' := .getAttr headExpr s) (cstStep := getAttr head s es) - (fun w => by simp [evaluate, hhead, bind, Except.bind]) hb - (fun hv' hge => evalAccessors_agrees rest rest_ast (.getAttr headExpr s) bexp hv' - hrest hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz (by simp only [List.cons.sizeOf_spec]; omega)))) v - | .field i :: [], accs_ast, headExpr, bexp, head, htrans, hb, hhead, harg => by - intro v - simp only [List.mapM_cons, List.mapM_nil, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.pure_def, - Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, rest_ast, hrest, rfl⟩ := htrans - cases i with - | idIdent s0 => - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨s, hs, rfl⟩ := ha_ast - subst hrest - rw [memberAuxB_field_nil] at hb - have hev : Cst.Member.evalAccessors head [.field (.idIdent s0)] req es - = (do let hv ← getAttr head s es; Cst.Member.evalAccessors hv [] req es) := by - simp [Cst.Member.evalAccessors, hs] - have hstep : ∀ w, evaluate (Expr.getAttr headExpr (CstCommon.Ident.toString (.idIdent s))) req es = .ok w - ↔ getAttr head s es = .ok w := by - intro w; simp [evaluate, hhead, CstCommon.Ident.toString, bind, Except.bind] - have hbrec : memberAuxB (Expr.getAttr headExpr (CstCommon.Ident.toString (.idIdent s))) [] = some bexp := hb - rw [hev] - exact evalAccessors_step hstep hbrec - (fun hv' hge => evalAccessors_agrees [] [] _ bexp hv' (by simp) hbrec hge - (fun ce hsz => harg ce (Nat.lt_trans hsz (by simp only [List.cons.sizeOf_spec]; omega)))) v - | _ => simp [Cst.MemAccess.toAstAccessor?] at ha_ast - | .field i :: .call args :: rest2, accs_ast, headExpr, bexp, head, htrans, hb, hhead, harg => by - intro v - rw [List.mapM_cons] at htrans - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, tl_ast, htl, rfl⟩ := htrans - cases i with - | idIdent s0 => - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨s, hs, rfl⟩ := ha_ast - rw [List.mapM_cons] at htl - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htl - obtain ⟨a2_ast, ha2_ast, rest2_ast, hrest2, rfl⟩ := htl - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha2_ast - obtain ⟨xs, hxs, rfl⟩ := ha2_ast - rw [memberAuxB_field_call] at hb - cases hop : CstCommon.String.toMethodOp? s with - | none => simp [Cst.Ident.toMeth?, hop] at hb - | some op => - cases op with - | inl bop => - cases args with - | nil => simp [Cst.Expr.toAExprs?] at hxs; subst hxs; simp [Cst.Ident.toMeth?, hop, oneArg?] at hb - | cons arg rest_args => - cases rest_args with - | cons a2 r2 => - simp only [Cst.Expr.toAExprs?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at hxs - obtain ⟨ax, hax, xs2, hxs2, rfl⟩ := hxs - obtain ⟨bx, hbx, xs3, hxs3, rfl⟩ := hxs2 - simp [Cst.Ident.toMeth?, hop, oneArg?] at hb - | nil => - simp only [Cst.Expr.toAExprs?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at hxs - obtain ⟨ax, hax, a, rfl, rfl⟩ := hxs - simp only [Cst.Ident.toMeth?, hop, oneArg?, Option.bind_eq_bind, Option.bind_some] at hb - have hagr := harg arg (by simp only [List.cons.sizeOf_spec, Cst.MemAccess.call.sizeOf_spec]; omega) ax hax - have hstep : ∀ w, evaluate (Expr.binaryApp bop headExpr ax) req es = .ok w - ↔ (do let argVal ← arg.evaluate req es; apply₂ bop head argVal es) = .ok w := by - intro w - cases hae : arg.evaluate req es with - | ok argVal => - have hax_ok : evaluate ax req es = .ok argVal := (hagr argVal).mpr hae - simp [evaluate, hhead, hax_ok, bind, Except.bind] - | error e => - cases hax2 : evaluate ax req es with - | ok w' => rw [(hagr w').mp hax2] at hae; simp at hae - | error e' => simp [evaluate, hhead, hax2, bind, Except.bind] - have hev : Cst.Member.evalAccessors head (.field (.idIdent s0) :: .call [arg] :: rest2) req es - = (do let hv ← (do let argVal ← arg.evaluate req es; apply₂ bop head argVal es); - Cst.Member.evalAccessors hv rest2 req es) := by - simp [Cst.Member.evalAccessors, hs, hop, bind_assoc] - rw [hev] - exact evalAccessors_step hstep hb - (fun hv' hge => evalAccessors_agrees rest2 rest2_ast (.binaryApp bop headExpr ax) bexp hv' - hrest2 hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz - (by simp only [List.cons.sizeOf_spec, Cst.MemAccess.call.sizeOf_spec]; omega)))) v - | inr uop => - cases args with - | cons arg rest_args => - simp only [Cst.Expr.toAExprs?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at hxs - obtain ⟨ax, hax, xs2, hxs2, rfl⟩ := hxs - simp [Cst.Ident.toMeth?, hop] at hb - | nil => - simp only [Cst.Expr.toAExprs?, Option.some.injEq] at hxs; subst hxs - simp only [Cst.Ident.toMeth?, hop, List.isEmpty_nil, if_true] at hb - have hstep : ∀ w, evaluate (Expr.unaryApp uop headExpr) req es = .ok w - ↔ apply₁ uop head = .ok w := by - intro w; simp [evaluate, hhead, bind, Except.bind] - have hev : Cst.Member.evalAccessors head (.field (.idIdent s0) :: .call [] :: rest2) req es - = (do let hv ← apply₁ uop head; Cst.Member.evalAccessors hv rest2 req es) := by - simp [Cst.Member.evalAccessors, hs, hop, bind, Except.bind] - rw [hev] - exact evalAccessors_step hstep hb - (fun hv' hge => evalAccessors_agrees rest2 rest2_ast (.unaryApp uop headExpr) bexp hv' - hrest2 hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz - (by simp only [List.cons.sizeOf_spec, Cst.MemAccess.call.sizeOf_spec]; omega)))) v - | _ => simp [Cst.MemAccess.toAstAccessor?] at ha_ast - | .field i :: .field i2 :: rest2, accs_ast, headExpr, bexp, head, htrans, hb, hhead, harg => by - intro v - rw [List.mapM_cons] at htrans - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, tl_ast, htl, rfl⟩ := htrans - cases i with - | idIdent s0 => - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨s, hs, rfl⟩ := ha_ast - obtain ⟨id2, r2, htl_shape⟩ := mapM_toAst_field_head htl - rw [htl_shape, memberAuxB_field_field, ← htl_shape] at hb - have hev : Cst.Member.evalAccessors head (.field (.idIdent s0) :: .field i2 :: rest2) req es - = (do let hv ← getAttr head s es; Cst.Member.evalAccessors hv (.field i2 :: rest2) req es) := by - simp [Cst.Member.evalAccessors, hs] - have hstep : ∀ w, evaluate (Expr.getAttr headExpr (CstCommon.Ident.toString (.idIdent s))) req es = .ok w - ↔ getAttr head s es = .ok w := by - intro w; simp [evaluate, hhead, CstCommon.Ident.toString, bind, Except.bind] - rw [hev] - exact evalAccessors_step hstep hb - (fun hv' hge => evalAccessors_agrees (.field i2 :: rest2) tl_ast _ bexp hv' - htl hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz (by simp only [List.cons.sizeOf_spec]; omega)))) v - | _ => simp [Cst.MemAccess.toAstAccessor?] at ha_ast - | .field i :: .index ex2 :: rest2, accs_ast, headExpr, bexp, head, htrans, hb, hhead, harg => by - intro v - rw [List.mapM_cons] at htrans - simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at htrans - obtain ⟨a_ast, ha_ast, tl_ast, htl, rfl⟩ := htrans - cases i with - | idIdent s0 => - simp only [Cst.MemAccess.toAstAccessor?, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at ha_ast - obtain ⟨s, hs, rfl⟩ := ha_ast - obtain ⟨id2, r2, htl_shape⟩ := mapM_toAst_index_head htl - rw [htl_shape, memberAuxB_field_index, ← htl_shape] at hb - have hev : Cst.Member.evalAccessors head (.field (.idIdent s0) :: .index ex2 :: rest2) req es - = (do let hv ← getAttr head s es; Cst.Member.evalAccessors hv (.index ex2 :: rest2) req es) := by - simp [Cst.Member.evalAccessors, hs] - have hstep : ∀ w, evaluate (Expr.getAttr headExpr (CstCommon.Ident.toString (.idIdent s))) req es = .ok w - ↔ getAttr head s es = .ok w := by - intro w; simp [evaluate, hhead, CstCommon.Ident.toString, bind, Except.bind] - rw [hev] - exact evalAccessors_step hstep hb - (fun hv' hge => evalAccessors_agrees (.index ex2 :: rest2) tl_ast _ bexp hv' - htl hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz (by simp only [List.cons.sizeOf_spec]; omega)))) v - | _ => simp [Cst.MemAccess.toAstAccessor?] at ha_ast -termination_by accs_cst _ _ _ _ _ _ _ _ => accs_cst.length -decreasing_by all_goals (simp_wf <;> omega) - -/-- Equality version of `evalAccessors_agrees`. -/ +/-- Core member-access agreement (evaluation equality): the AST built by + `memberAuxB` over a head evaluates as the CST member-access spine does. -/ theorem evalAccessors_eq {req : Request} {es : Entities} : (accs_cst : List Cst.MemAccess) → (accs_ast : List AstAccessor) → @@ -1802,57 +1468,6 @@ theorem toExprOrSpecial_name_func {item : Cst.Primary} {an : Spec.Name} | rInits r => simp [Cst.Primary.toExprOrSpecial?, Option.bind_eq_bind, Option.bind_eq_some_iff] at h -/-- For the `rIsIn` case: when the translator's `toEntityType?` succeeds with - `et`, the evaluator's structural `toEntityTypeName?` succeeds with the same - `et`. Both enforce the same shape (extended/mext empty, op `none` or - `.nDash 0`, access empty, item a `.name`), and both now build the entity-type - name via the shared `CstCommon.Name.toAName?`, so they agree. -/ -theorem addExpr_toEntityType_agrees - {e : Cst.AddExpr} {et : EntityType} : - Cst.AddExpr.toEntityType? e = some et → - Cst.AddExpr.toEntityTypeName? e = some et := by - intro h - simp [Cst.AddExpr.toEntityType?, Option.bind_eq_some_iff] at h - obtain ⟨eos, heos, hmatch⟩ := h - cases eos with - | expr _ | var _ | boolLit _ | strLit _ => simp at hmatch - | name an => - simp at hmatch - subst hmatch - obtain ⟨⟨⟨op, member⟩, mext⟩, ext⟩ := e - simp [Cst.AddExpr.toExprOrSpecial?, Cst.MultExpr.toExprOrSpecial?, - Cst.Unary.toExprOrSpecial?] at heos - cases ext with - | cons _ _ => simp [Option.bind_eq_some_iff] at heos - | nil => - simp at heos - cases mext with - | cons _ _ => simp [Option.bind_eq_some_iff] at heos - | nil => - simp at heos - cases op with - | none => - obtain ⟨hAccNil, n, hItem, hAName⟩ := member_toExprOrSpecial_name heos - simp [Cst.AddExpr.toEntityTypeName?, hAccNil, hItem] - exact hAName - | some op' => - cases op' with - | nDash k => - by_cases hk : k = 0 - · subst hk - obtain ⟨hAccNil, n, hItem, hAName⟩ := member_toExprOrSpecial_name heos - simp [Cst.AddExpr.toEntityTypeName?, hAccNil, hItem] - exact hAName - · simp at heos - split at heos - · split at heos - · simp at heos - · split at heos <;> simp at heos - · simp at heos - · simp [Option.bind_eq_some_iff] at heos - | nBang _ => simp [Option.bind_eq_some_iff] at heos - | nOverBang | nOverDash => simp at heos - /-- `apply₂ .mem` only ever yields a boolean value (or an error), so its result survives the `.as Bool` coercion the translated `.and` applies to it. -/ theorem apply₂_mem_returns_bool {v₁ v₂ : Value} {es : Entities} {r : Value} : @@ -1865,60 +1480,8 @@ theorem apply₂_mem_returns_bool {v₁ v₂ : Value} {es : Entities} {r : Value · simp at h · simp only [Except.ok.injEq] at h; exact ⟨_, h.symm⟩ -/-- For the `rIsIn` case with `inEntity = some ie`: the translated AST - `(is et target) && (target in ie)` agrees with the CST evaluation. Takes the - target/inEntity bridging iffs as hypotheses so the mutual recursion stays in - the main proof. -/ -theorem rIsIn_some_eval_agrees - {target ety ie : Cst.AddExpr} {mt mi : Expr} {et : EntityType} - {req : Request} {es : Entities} - (hEt : ety.toEntityType? = some et) - (htarget_iff : ∀ v, evaluate mt req es = .ok v ↔ target.evaluate req es = .ok v) - (hinEntity_iff : ∀ v, evaluate mi req es = .ok v ↔ ie.evaluate req es = .ok v) - (hie_trans : ie.toAExpr? = some mi) : - ∀ v, evaluate (Expr.and (.unaryApp (.is et) mt) (.binaryApp .mem mt mi)) req es = .ok v ↔ - (Cst.Relation.rIsIn target ety (some ie)).evaluate req es = .ok v := by - intro v - simp only [Cst.Relation.evaluate, hEt, evaluate, hie_trans, Option.isNone_some, - Bool.false_eq_true, if_false] - cases htgt : evaluate mt req es with - | error e => - cases htgtC : target.evaluate req es with - | ok vt => exact absurd ((htarget_iff vt).mpr htgtC) (by rw [htgt]; simp) - | error e' => simp [bind, Except.bind, Result.as] - | ok vt => - have htgtC : target.evaluate req es = .ok vt := (htarget_iff vt).mp htgt - simp only [htgtC, bind, Except.bind] - cases hIs : apply₁ (.is et) vt with - | error e => simp [Result.as] - | ok isVal => - cases isVal with - | prim p => - cases p with - | bool b => - cases b with - | false => simp [Result.as, Coe.coe, Value.asBool] - | true => - simp only [Result.as, Coe.coe, Value.asBool, Bool.not_true, - Bool.false_eq_true, if_false] - cases hie : evaluate mi req es with - | error e => - cases hieC : ie.evaluate req es with - | ok vi => exact absurd ((hinEntity_iff vi).mpr hieC) (by rw [hie]; simp) - | error e' => simp [] - | ok v₂ => - have hieC : ie.evaluate req es = .ok v₂ := (hinEntity_iff v₂).mp hie - simp only [hieC] - cases hmem : apply₂ .mem vt v₂ es with - | error e => simp [] - | ok memv => - have ⟨b', hb'⟩ := apply₂_mem_returns_bool hmem - subst hb' - simp [pure, Except.pure] - | int _ | string _ | entityUID _ => simp [Result.as, Coe.coe, Value.asBool] - | set _ | record _ | ext _ => simp [Result.as, Coe.coe, Value.asBool] - -/-- Equality version of `rIsIn_some_eval_agrees`. -/ +/-- For the `rIsIn` case with `inEntity = some ie`: the translated AST evaluates + equally to the applied `in` relation. -/ theorem rIsIn_some_eval_eq {target ety ie : Cst.AddExpr} {mt mi : Expr} {et : EntityType} {req : Request} {es : Entities} @@ -2128,7 +1691,7 @@ theorem expr_or_eval_eq_foldOps_step_eq | int _ | string _ | entityUID _ => simp [Value.asBool] | set _ | record _ | ext _ => simp [Value.asBool] -/-- Equality analog of `multExprFoldExtended_foldOps_agrees`, with the per-`Unary` +/-- `MultExpr.foldExtended` evaluation equality, with the per-`Unary` evaluation equality supplied as a hypothesis so the fold stays outside the mutual `_sound` cycle. -/ theorem multExprFoldExtended_foldOps_eq @@ -2160,7 +1723,7 @@ theorem multExprFoldExtended_foldOps_eq | _ => simp [Cst.MultExpr.foldExtended, hop] at hfold termination_by xs _ _ _ => xs.length -/-- Equality analog of `addExprFoldExtended_foldOps_agrees`, with the per-`MultExpr` +/-- `AddExpr.foldExtended` evaluation equality, with the per-`MultExpr` evaluation equality supplied as a hypothesis. -/ theorem addExprFoldExtended_foldOps_eq (req : Request) (es : Entities) : @@ -2201,7 +1764,7 @@ theorem addExprFoldExtended_foldOps_eq simp [evaluate, Cst.AddExpr.foldOps, bind_assoc, hm_eq] termination_by xs _ _ _ => xs.length -/-- Equality analog of `andExprFoldExtended_foldOps_agrees`, with the per-`Relation` +/-- `AndExpr.foldExtended` evaluation equality, with the per-`Relation` evaluation equality supplied as a hypothesis. -/ theorem andExprFoldExtended_foldOps_eq (req : Request) (es : Entities) : @@ -2233,7 +1796,7 @@ theorem andExprFoldExtended_foldOps_eq simp [bind, Except.bind] termination_by xs _ _ _ => xs.length -/-- Equality analog of `orExprFoldExtended_foldOps_agrees`, with the per-`AndExpr` +/-- `OrExpr.foldExtended` evaluation equality, with the per-`AndExpr` evaluation equality supplied as a hypothesis. -/ theorem orExprFoldExtended_foldOps_eq (req : Request) (es : Entities) : @@ -2419,20 +1982,8 @@ theorem toAExprs?_eq_mapM (args : List Cst.Expr) : | nil => simp [Cst.Expr.toAExprs?, List.mapM_nil] | cons ce rest ih => simp [Cst.Expr.toAExprs?, List.mapM_cons, ih] -/-- Agreement for translated argument lists: evaluating the AST args agrees (on - `ok`) with evaluating the CST args, given per-argument agreement. -/ -theorem toAExprs?_eval_agrees {req : Request} {es : Entities} - (args : List Cst.Expr) (xs : List Expr) - (htr : Cst.Expr.toAExprs? args = some xs) - (harg : ∀ ce ∈ args, ∀ ax, ce.toAExpr? = some ax → - ∀ w, evaluate ax req es = .ok w ↔ ce.evaluate req es = .ok w) : - ∀ vs, xs.mapM (fun a => evaluate a req es) = .ok vs ↔ - args.mapM (fun ce => ce.evaluate req es) = .ok vs := by - apply mapM_eval_agrees req es args xs ?_ harg - simp only [List.mapM₁_eq_mapM (fun ce : Cst.Expr => ce.toAExpr?), ← toAExprs?_eq_mapM] - exact htr - -/-- Equality version of `toAExprs?_eval_agrees`. -/ +/-- Argument-list agreement (evaluation equality): evaluating the AST args + equals evaluating the CST args. -/ theorem toAExprs?_eval_eq {req : Request} {es : Entities} (args : List Cst.Expr) (xs : List Expr) (htr : Cst.Expr.toAExprs? args = some xs) @@ -2499,12 +2050,6 @@ theorem Cst.Primary.toAttr?_consistent (p : Cst.Primary) : simp [Cst.Primary.toAttr?, Cst.Primary.toExprOrSpecial?, Option.bind] cases (rInitsToMap? r) <;> simp [ExprOrSpecial.toValidAttr?] -/-- A translation result that always produces an `.expr` is never a valid attribute. -/ -private theorem bind_validAttr_expr {α : Type} (o : Option α) (g : α → Expr) : - (o.bind (fun a => some (ExprOrSpecial.expr (g a)))).bind ExprOrSpecial.toValidAttr? = none := by - cases o <;> simp [ExprOrSpecial.toValidAttr?] - -set_option linter.unusedSimpArgs false in /-- The CST-native record-key attribute extractor on an `Expr` agrees with the translator's `toExprOrSpecial? >>= toValidAttr?`. Peeling lemma: the key must reduce to a bare primary; analogous to the `addExpr_to*_agrees` peeling proofs. -/ @@ -2633,7 +2178,7 @@ theorem Cst.Expr.toAttr?_consistent (e : Cst.Expr) : · have hL : Cst.Expr.toAttr? (.expr ⟨.edOr o⟩) = none := by simp [Cst.Expr.toAttr?, hoe, hae, hrel, hext, hax, hmx, hop, hn] rw [hL] - simp only [hn] + simp repeat' split all_goals simp [ExprOrSpecial.toValidAttr?, Option.bind_assoc] | nBang n => @@ -2651,123 +2196,8 @@ theorem Cst.Expr.toAttr?_consistent (e : Cst.Expr) : rw [hL]; simp -/-- Lift an element-wise `Except`-result agreement through one `mapM` cons step. -/ -private theorem except_bind_cons_iff {β γ : Type} {X Y : Except γ (List β)} {hd : β} - {vs : List β} (h : ∀ vs', X = .ok vs' ↔ Y = .ok vs') : - (X >>= fun tl => Except.ok (hd :: tl)) = .ok vs ↔ - (Y >>= fun tl => Except.ok (hd :: tl)) = .ok vs := by - cases hX : X with - | error e => - cases hY : Y with - | error e' => simp [bind, Except.bind] - | ok vsy => have := (h vsy).mpr hY; rw [hX] at this; cases this - | ok vsx => - have hY := (h vsx).mp hX - rw [hY] - -/-- Record-level bridge: when `rInitsToMap? r = some map`, evaluating the - translated AST record entries (`map`) agrees element-wise with the CST - `.rInits` evaluation, given the per-value evaluation agreement. -/ -theorem rInits_eval_agrees (req : Request) (es : Entities) : - ∀ (r : List Cst.RecInit) (map : List (Attr × Expr)), - rInitsToMap? r = some map → - (∀ ri ∈ r, ∀ ax, ri.value.toAExpr? = some ax → - ∀ v, evaluate ax req es = .ok v ↔ ri.value.evaluate req es = .ok v) → - ∀ vs, map.mapM (fun x => bindAttr x.fst (evaluate x.snd req es)) = .ok vs ↔ - r.mapM (fun ri => - match ri.key.toAttr? with - | none => Except.error (Error.cstError CstError.stringError) - | some attr => do let val ← ri.value.evaluate req es; .ok (attr, val)) = .ok vs := by - intro r - induction r with - | nil => - intro map hmap _ vs - simp [rInitsToMap?] at hmap - subst hmap - simp [List.mapM_nil] - | cons ri rs ih => - intro map hmap hperElt vs - simp [rInitsToMap?, Option.bind_eq_some_iff] at hmap - obtain ⟨attr_eos, hattr_eos, attr, hattr, vexpr, hvexpr, rest, hrest, hmapeq⟩ := hmap - subst hmapeq - -- attr consistency: `ri.key.toAttr? = some attr` - have hkey : ri.key.toAttr? = some attr := by - rw [Cst.Expr.toAttr?_consistent, hattr_eos]; simpa using hattr - -- per-value iff for the head - have hhd_iff : ∀ vp, evaluate vexpr req es = .ok vp ↔ ri.value.evaluate req es = .ok vp := - hperElt ri List.mem_cons_self vexpr hvexpr - -- IH for the tail - have htl_perElt : ∀ x ∈ rs, ∀ ax, x.value.toAExpr? = some ax → - ∀ v, evaluate ax req es = .ok v ↔ x.value.evaluate req es = .ok v := by - intro x hx ax hax v - exact hperElt x (List.mem_cons_of_mem _ hx) ax hax v - have ih' := ih rest hrest htl_perElt - -- head-element agreement (attr + value) - have head_iff : ∀ p, bindAttr attr (evaluate vexpr req es) = .ok p ↔ - (do let val ← ri.value.evaluate req es; Except.ok (attr, val)) = .ok p := by - intro p - simp only [bindAttr, bind, Except.bind, pure, Except.pure] - cases hev : evaluate vexpr req es with - | error e => - cases hev2 : ri.value.evaluate req es with - | error e' => simp - | ok v => have := (hhd_iff v).mpr hev2; rw [this] at hev; cases hev - | ok hv => have := (hhd_iff hv).mp hev; rw [this] - simp only [List.mapM_cons, hkey] - cases hHd : bindAttr attr (evaluate vexpr req es) with - | error e => - cases hCst : (do let val ← ri.value.evaluate req es; Except.ok (attr, val)) with - | ok p => have := (head_iff p).mpr hCst; rw [this] at hHd; cases hHd - | error e' => simp [bind, Except.bind] - | ok p => - have hCst := (head_iff p).mp hHd - rw [hCst] - exact except_bind_cons_iff (hd := p) (vs := vs) ih' - -/-- Lift an element-wise `Except`-result agreement through a common wrapper. -/ -private theorem except_bind_iff {β δ γ : Type} {X Y : Except γ β} {g : β → δ} {v : δ} - (h : ∀ b, X = .ok b ↔ Y = .ok b) : - (X >>= fun b => Except.ok (g b)) = .ok v ↔ (Y >>= fun b => Except.ok (g b)) = .ok v := by - cases hX : X with - | error e => - cases hY : Y with - | error e' => simp [bind, Except.bind] - | ok b => have := (h b).mpr hY; rw [hX] at this; cases this - | ok b => - have hY := (h b).mp hX - rw [hY] - -/-- Evaluate-level record bridge: the translated AST record `Expr.record map` - and the CST `.rInits r` evaluate to the same value. -/ -theorem rInits_record_eval_agrees (req : Request) (es : Entities) - (r : List Cst.RecInit) (map : List (Attr × Expr)) - (hmap : rInitsToMap? r = some map) - (hperElt : ∀ ri ∈ r, ∀ ax, ri.value.toAExpr? = some ax → - ∀ v, evaluate ax req es = .ok v ↔ ri.value.evaluate req es = .ok v) : - ∀ v, evaluate (Expr.record map) req es = .ok v ↔ - (Cst.Primary.rInits r).evaluate req es = .ok v := by - intro v - have hbridge := rInits_eval_agrees req es r map hmap hperElt - have hAST : evaluate (Expr.record map) req es = - (map.mapM (fun x => bindAttr x.fst (evaluate x.snd req es))) >>= - fun avs => Except.ok (Value.record (Map.make avs)) := by - simp only [evaluate, List.mapM₂_eq_mapM (fun x => bindAttr x.fst (evaluate x.snd req es))] - have hCST : (Cst.Primary.rInits r).evaluate req es = - (r.mapM (fun ri => - match ri.key.toAttr? with - | none => Except.error (Error.cstError CstError.stringError) - | some attr => do let val ← ri.value.evaluate req es; Except.ok (attr, val))) >>= - fun avs => Except.ok (Value.record (Map.make avs)) := by - simp only [Cst.Primary.evaluate] - congr 1 - exact List.mapM₁_eq_mapM (fun ri : Cst.RecInit => - match ri.key.toAttr? with - | none => Except.error (Error.cstError CstError.stringError) - | some attr => do let val ← ri.value.evaluate req es; Except.ok (attr, val)) r - rw [hAST, hCST] - exact except_bind_iff hbridge - -/-- Equality analog of `rInits_eval_agrees`. -/ +/-- Record-level bridge (evaluation equality): when `rInitsToMap? r = some map`, + evaluating the translated inits equals evaluating the CST record inits. -/ theorem rInits_eval_eq (req : Request) (es : Entities) : ∀ (r : List Cst.RecInit) (map : List (Attr × Expr)), rInitsToMap? r = some map → @@ -2804,7 +2234,8 @@ theorem rInits_eval_eq (req : Request) (es : Entities) : simp only [List.mapM_cons, hkey] rw [hhead, ih'] -/-- Equality analog of `rInits_record_eval_agrees`. -/ +/-- Evaluate-level record bridge (evaluation equality): the translated AST record + `Expr.record map` evaluates as the CST record does. -/ theorem rInits_record_eval_eq (req : Request) (es : Entities) (r : List Cst.RecInit) (map : List (Attr × Expr)) (hmap : rInitsToMap? r = some map) diff --git a/cedar-lean/Cedar/Thm/Translation/ExprTranslation.lean b/cedar-lean/Cedar/Thm/Translation/ExprTranslation.lean index 534663c0e..434d01afd 100644 --- a/cedar-lean/Cedar/Thm/Translation/ExprTranslation.lean +++ b/cedar-lean/Cedar/Thm/Translation/ExprTranslation.lean @@ -30,24 +30,6 @@ theorem Cst.ExprOrSpecial.toExpr?_sound {eos : ExprOrSpecial} {aexp : Expr} req | some s' => simp only [hsome] at h ⊢; simp at h; subst h; simp [evaluate] · rename_i b; subst h; simp [evaluate] -theorem Cst.ExprOrSpecial.toExpr?_evaluate {eos : ExprOrSpecial} {aexp : Expr} req es : - eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - (match eos with - | .expr e => evaluate e req es - | .var var => evaluate (Expr.var var) req es - | .strLit s => (CstCommon.unescape? s).elim - (.error (.cstError .stringError)) - (fun s' => .ok (.prim (.string s'))) - | .boolLit b => .ok (.prim (.bool b)) - | .name _ => .error (.cstError .nameError)) = .ok v := by - cases eos <;> intro h <;> simp_all [ExprOrSpecial.toExpr?] - · rename_i lit; cases hsome : CstCommon.unescape? lit with - | none => rw [hsome] at h; simp at h - | some s' => rw [hsome] at h; simp at *; rw [← h]; simp [evaluate] - · rename_i b; rw [← h]; simp [evaluate] - - mutual theorem Cst.Primary.toAExpr?_sound @@ -984,1337 +966,3 @@ theorem expr_to_expr_sound simp [heos] at h; exact h end - - - -mutual - -theorem Cst.Primary.toAExpr?_evaluate - {prim : Cst.Primary} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - prim.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - prim.evaluate req es = .ok v := by - - cases prim with - | literal lit => - intro hprim aexp heos v - have haexp_iff := Cst.ExprOrSpecial.toExpr?_evaluate req es heos v - rw [haexp_iff]; clear haexp_iff - simp [Cst.Primary.toExprOrSpecial?, Cst.Literal.toExprOrSpecial?] at hprim - cases lit with - | liTrue | liFalse => - simp at hprim; rw [← hprim]; unfold Cst.Primary.evaluate; simp - | liNum n => - simp at hprim - cases hn : Int64.ofInt? ↑n.toNat with - | none => rw [hn] at hprim; simp at hprim - | some n' => - rw [hn] at hprim; simp at hprim; rw [← hprim] - simp [evaluate, Cst.Primary.evaluate, hn] - | liStr s => - simp at hprim; rw [← hprim] - simp [Cst.Primary.evaluate, Cst.Str.toUnescapedString, bind, Except.bind] - cases hs : CstCommon.unescape? s <;> simp - - | ref r => - intro href aexp heos v - have haexp_iff := Cst.ExprOrSpecial.toExpr?_evaluate req es heos v - rw [haexp_iff]; clear haexp_iff - simp [Cst.Primary.toExprOrSpecial?] at href - cases r with - | uid path eid => - let (.string s) := eid - simp [Cst.Ref.toExprOrSpecial?] at href - simp only [Option.bind_eq_some_iff] at href - obtain ⟨ty, hty, su, hsu1, hsu2⟩ := href - simp at hsu2; rw [← hsu2] - simp [Cst.Primary.evaluate, Cst.Str.toUnescapedString] - cases hs : CstCommon.unescape? s with - | none => rw [hs] at hsu1; contradiction - | some su' => - rw [hs] at hsu1; simp at hsu1 - simp [hsu1, bind, Except.bind] - simp only [Cst.Name.toAName?] at hty - simp [evaluate, hty] - | ref path rinits => simp [Cst.Ref.toExprOrSpecial?] at href - - | name n => - intro hname aexp heos v - have haexp_iff := Cst.ExprOrSpecial.toExpr?_evaluate req es heos v - rw [haexp_iff]; clear haexp_iff - simp [Cst.Primary.toExprOrSpecial?] at hname - unfold Cst.Primary.evaluate - cases hvar : n.toVar? with - | none => - simp [hvar] at hname - simp only [Option.bind_eq_some_iff] at hname - obtain ⟨name, hname1, hname2⟩ := hname - simp at hname2; rw [← hname2] at heos - simp [ExprOrSpecial.toExpr?] at heos - | some var => - simp [hvar] at hname; simp [← hname] - cases hpath : n.path with - | nil => - simp - have ⟨hvn1, hvn2⟩ := Cst.Name.toVar?_agrees hvar - cases hv : var with - | principal => simp [hv] at hvn2; simp [evaluate, hvn2] - | action => simp [hv] at hvn2; simp [evaluate, hvn2] - | resource => simp [hv] at hvn2; simp [evaluate, hvn2] - | context => simp [hv] at hvn2; simp [evaluate, hvn2] - | cons hd tl => - have ⟨hvn1, _⟩ := Cst.Name.toVar?_agrees hvar - simp [hvn1] at hpath - - | expr e => - intro hprim aexp heos v - simp [Cst.Primary.toExprOrSpecial?, Option.bind_eq_some_iff] at hprim - obtain ⟨ae, hae, heq⟩ := hprim - rw [← heq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - simp [Cst.Primary.evaluate] - simp [Cst.Expr.toAExpr?, Option.bind_eq_some_iff] at hae - obtain ⟨eEos, heEos, heExpr⟩ := hae - exact Cst.Expr.toAExpr?_evaluate heEos ae heExpr v - | eList xs => - intro hprim aexp heos v - simp [Cst.Primary.toExprOrSpecial?, Option.bind_eq_some_iff] at hprim - obtain ⟨aes, haes, heq⟩ := hprim - rw [← heq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - have hperElt : ∀ x ∈ xs, ∀ ax, - x.toAExpr? = some ax → - ∀ v, evaluate ax req es = .ok v ↔ x.evaluate req es = .ok v := by - intro x hx ax hax v - simp [Cst.Expr.toAExpr?, Option.bind_eq_some_iff] at hax - obtain ⟨xEos, hxEos, hxExpr⟩ := hax - exact Cst.Expr.toAExpr?_evaluate hxEos ax hxExpr v - have hbridge := mapM_eval_agrees req es xs aes haes hperElt - simp [evaluate, Cst.Primary.evaluate, bind, Except.bind, - List.mapM₁_eq_mapM (evaluate · req es)] - cases hmes : aes.mapM (fun a => evaluate a req es) with - | error err => - cases hxes : xs.mapM (fun x => x.evaluate req es) with - | ok vs => - have := (hbridge vs).mpr hxes - rw [this] at hmes; cases hmes - | error _ => simp - | ok vs => - have := (hbridge vs).mp hmes - rw [this] - | rInits r => - intro hprim aexp heos v - simp [Cst.Primary.toExprOrSpecial?, Option.bind_eq_some_iff] at hprim - obtain ⟨map, hmap, heq⟩ := hprim - rw [← heq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - -- per-value evaluation agreement (mutual IH on each record value) - have hperElt : ∀ ri ∈ r, ∀ ax, ri.value.toAExpr? = some ax → - ∀ v, evaluate ax req es = .ok v ↔ ri.value.evaluate req es = .ok v := by - intro ri hmem ax hax v - have hsz : sizeOf ri.value < 1 + sizeOf r := by - have h1 := List.sizeOf_lt_of_mem hmem - have hval : sizeOf ri.value < sizeOf ri := by - cases ri; simp only [Cst.RecInit.mk.sizeOf_spec]; omega - omega - simp [Cst.Expr.toAExpr?, Option.bind_eq_some_iff] at hax - obtain ⟨vEos, hvEos, hvExpr⟩ := hax - exact Cst.Expr.toAExpr?_evaluate hvEos ax hvExpr v - exact rInits_record_eval_agrees req es r map hmap hperElt v -termination_by (sizeOf prim, 0) -decreasing_by - all_goals simp_wf - all_goals first - | (apply Prod.Lex.left; omega) - | (apply Prod.Lex.left - rename_i _ _ - have := List.sizeOf_lt_of_mem hx - omega) - -theorem Cst.Member.toAExpr?_evaluate - {mem : Cst.Member} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - mem.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - mem.evaluate req es = .ok v := by - - intro hmem aexp heos v - simp only [Cst.Member.toExprOrSpecial?, Option.bind_eq_bind, Option.bind_eq_some_iff] at hmem - obtain ⟨peos, hitem, accs, haccs, hmem⟩ := hmem - have harg : ∀ ce : Cst.Expr, sizeOf ce < sizeOf mem.access → ∀ ax, ce.toAExpr? = some ax → - ∀ w, evaluate ax req es = .ok w ↔ ce.evaluate req es = .ok w := by - intro ce hsz ax hax w - simp only [Cst.Expr.toAExpr?, Option.bind_eq_bind, Option.bind_eq_some_iff] at hax - obtain ⟨ceos, hceos, hax2⟩ := hax - exact Cst.Expr.toAExpr?_evaluate hceos ax hax2 w - unfold Cst.Member.evaluate - split - case h_1 _ s args rest => - simp only [Cst.Primary.toExprOrSpecial?, Cst.Name.toVar?, Cst.Name.toAName?, - CstCommon.Name.toAName?, - CstCommon.Ident.toUnrestrictedString?, List.isEmpty_nil, Bool.not_true, Bool.false_eq_true, - reduceIte, Option.pure_def, List.mapM_nil, Option.bind_eq_bind, Option.bind_some, - Option.some.injEq] at hitem - subst hitem - rw [List.mapM_cons] at haccs - simp only [Cst.MemAccess.toAstAccessor?, Option.pure_def, Option.bind_eq_bind, - Option.bind_eq_some_iff, Option.some.injEq] at haccs - obtain ⟨a_ast, ha_ast, rest_ast, hrest_ast, rfl⟩ := haccs - obtain ⟨xs, hxs, rfl⟩ := ha_ast - have hargm : ∀ ce ∈ args, ∀ ax, ce.toAExpr? = some ax → - ∀ w, evaluate ax req es = .ok w ↔ ce.evaluate req es = .ok w := by - intro ce hce ax hax w - exact harg ce (by - have := List.sizeOf_lt_of_mem hce - simp only [Cst.MemAccess.call.sizeOf_spec, - List.cons.sizeOf_spec]; omega) ax hax w - cases hfn : CstCommon.String.toExtFun? s with - | none => - have htf : Name.toFunc? { id := s, path := [] } xs = none := by - simp [Name.toFunc?, hfn] - rw [memberAux, memberAuxA, htf] at hmem - simp at hmem - | some xfn => - have htf : Name.toFunc? { id := s, path := [] } xs = some (.call xfn xs) := by - simp [Name.toFunc?, hfn, toExtFun?_some_isFunctionName hfn] - have hb : memberAuxB (.call xfn xs) rest_ast = some aexp := by - have hmeq : memberAux (.name { id := s, path := [] }) (.call xs :: rest_ast) - = (memberAuxB (.call xfn xs) rest_ast).bind (fun r => some (.expr r)) := by - simp [memberAux, memberAuxA, htf] - rw [hmeq] at hmem - simp only [Option.bind_eq_some_iff] at hmem - obtain ⟨ret, hret, heq2⟩ := hmem - rw [← Option.some.inj heq2] at heos - simp only [ExprOrSpecial.toExpr?, Option.some.injEq] at heos - rw [heos] at hret; exact hret - have hstep : ∀ w, evaluate (Expr.call xfn xs) req es = .ok w ↔ - (do let argVals ← args.mapM (fun a : Cst.Expr => a.evaluate req es); call xfn argVals) = .ok w := by - intro w - simp only [evaluate, List.mapM₁_eq_mapM (fun a => evaluate a req es)] - cases hxe : xs.mapM (fun a => evaluate a req es) with - | ok vs => - rw [(toAExprs?_eval_agrees args xs hxs hargm vs).mp hxe] - | error e => - have hne : ∀ vs, args.mapM (fun ce => ce.evaluate req es) ≠ .ok vs := by - intro vs hvs - rw [(toAExprs?_eval_agrees args xs hxs hargm vs).mpr hvs] at hxe; simp at hxe - cases hae : args.mapM (fun ce => ce.evaluate req es) with - | ok vs => exact absurd hae (hne vs) - | error e' => simp [bind, Except.bind] - rw [evalAccessors_step hstep hb - (fun hv' hge => evalAccessors_agrees rest rest_ast (.call xfn xs) aexp hv' - hrest_ast hb hge (fun ce hsz => harg ce (Nat.lt_trans hsz (by - simp only [Cst.MemAccess.call.sizeOf_spec, List.cons.sizeOf_spec]; omega)))) v] - simp [bind_assoc] - case h_2 item access hnfc => - simp only [] at hitem haccs harg - match hpe : peos.toExpr? with - | some headExpr => - have hb : memberAuxB headExpr accs = some aexp := by - have he := memberAux_toExpr_eq accs hpe - rw [hmem, Option.bind_some, heos] at he; exact he.symm - have hheadIff := @Cst.Primary.toAExpr?_evaluate item peos req es hitem headExpr hpe - cases h_item : item.evaluate req es with - | error e => - have hge : ∃ e', evaluate headExpr req es = .error e' := by - cases hh : evaluate headExpr req es with - | error e' => exact ⟨e', rfl⟩ - | ok hv => exact absurd ((hheadIff hv).mp hh) (by rw [h_item]; simp) - obtain ⟨e', hge⟩ := hge - obtain ⟨e'', he''⟩ := memberAuxB_eval_error accs headExpr aexp e' hb hge - simp [he'', bind, Except.bind] - | ok hv => - have hge : evaluate headExpr req es = .ok hv := (hheadIff hv).mpr h_item - rw [evalAccessors_agrees access accs headExpr aexp hv haccs hb hge harg v] - simp [bind, Except.bind] - | none => - exfalso - cases memberAux_some_cases hmem with - | inl hl => obtain ⟨_, heq⟩ := hl; subst heq; rw [hpe] at heos; simp at heos - | inr hr => - obtain ⟨e, heq⟩ := hr - subst heq - cases peos with - | expr _ => simp [ExprOrSpecial.toExpr?] at hpe - | var _ => simp [ExprOrSpecial.toExpr?] at hpe - | boolLit _ => simp [ExprOrSpecial.toExpr?] at hpe - | strLit ss => - cases accs with - | nil => rw [memberAux_nil] at hmem; simp at hmem - | cons a r => simp [memberAux, memberAuxA, hpe] at hmem - | name an => - cases accs with - | nil => rw [memberAux_nil] at hmem; simp at hmem - | cons a rest_ast => - cases a with - | field id => - cases rest_ast with - | nil => simp [memberAux, memberAuxA] at hmem - | cons a2 r2 => cases a2 <;> simp [memberAux, memberAuxA] at hmem - | index id => simp [memberAux, memberAuxA] at hmem - | call xs => - cases hfunc : Name.toFunc? an xs with - | none => simp [memberAux, memberAuxA, hfunc] at hmem - | some e'' => - simp only [Name.toFunc?] at hfunc - split at hfunc - · rename_i hcond - simp only [Bool.and_eq_true] at hcond - obtain ⟨hpath, hfn⟩ := hcond - obtain ⟨ss, hs⟩ := toExprOrSpecial_name_func hitem (by simpa using hpath) hfn - cases haccess : access with - | nil => rw [haccess] at haccs; simp at haccs - | cons aa rr => - cases aa with - | call cargs => exact hnfc ss cargs rr hs haccess - | field f => - rw [haccess] at haccs - cases f <;> - simp [List.mapM_cons, Cst.MemAccess.toAstAccessor?, - Option.bind_eq_bind, Option.bind_eq_some_iff] at haccs - | index _ => - rw [haccess] at haccs - simp [List.mapM_cons, Cst.MemAccess.toAstAccessor?, - Option.bind_eq_bind, Option.bind_eq_some_iff] at haccs - · simp at hfunc -termination_by (sizeOf mem, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - first - | (subst_vars; simp only [Cst.Member.mk.sizeOf_spec]; omega) - | (cases mem; simp only [Cst.Member.mk.sizeOf_spec] at *; omega)) - -theorem Cst.Unary.toAExpr?_evaluate - {u : Cst.Unary} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - u.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - u.evaluate req es = .ok v := by - - intro hu aexp heos v - match hop : u.op with - | none => - simp [Cst.Unary.toExprOrSpecial?, hop] at hu - simp [Cst.Unary.evaluate, hop] - exact Cst.Member.toAExpr?_evaluate hu aexp heos v - | some (.nDash 0) => - simp [Cst.Unary.toExprOrSpecial?, hop] at hu - simp [Cst.Unary.evaluate, hop] - exact Cst.Member.toAExpr?_evaluate hu aexp heos v - | some (.nBang n) => - simp [Cst.Unary.toExprOrSpecial?, hop] at hu - simp [Cst.Unary.evaluate, hop] - cases hitem_trans : u.item.toExprOrSpecial? with - | none => simp [hitem_trans] at hu - | some ieos => - simp [hitem_trans] at hu - cases hioes_trans : ieos.toExpr? with - | none => simp [hioes_trans] at hu - | some iexp => - simp [hioes_trans] at hu - simp [← hu, ExprOrSpecial.toExpr?] at heos - rw [← heos] - have hitem_iff : ∀ vp, evaluate iexp req es = .ok vp ↔ u.item.evaluate req es = .ok vp := - Cst.Member.toAExpr?_evaluate hitem_trans iexp hioes_trans - rw [bangN_evaluate_general iexp n.toNat req es] - have h_zero : (n.toNat = 0) ↔ (n = 0) := by - constructor - · intro h; exact UInt8.toNat_inj.mp (by simp [h]) - · intro h; rw [h]; rfl - have h_par : (n.toNat % 2 = 0) ↔ (n % 2 = 0) := by - rw [show n.toNat % 2 = (n % 2).toNat from by rw [UInt8.toNat_mod]; rfl] - constructor - · intro h; exact UInt8.toNat_inj.mp (by simp [h]) - · intro h; rw [h]; rfl - simp [h_zero, h_par] - -- Forward and backward of the iff together — build it via constructor. - constructor - · intro hev_ok - -- Discriminate by what evaluate iexp produced. - cases h_iexp : evaluate iexp req es with - | error err => - rw [h_iexp] at hev_ok; simp at hev_ok - | ok vp => - rw [h_iexp] at hev_ok - have h_item := (hitem_iff vp).mp h_iexp - simp [h_item, bind, Except.bind] - by_cases hn : n = 0 - · simp [hn] at hev_ok ⊢ - exact hev_ok - · simp [hn] at hev_ok ⊢ - -- The match on vp yields .ok ... or .error. - cases vp with - | prim p => - cases p with - | bool b => simp at hev_ok ⊢; exact hev_ok - | _ => simp at hev_ok - | _ => simp at hev_ok - · intro hev_ok - cases h_item : u.item.evaluate req es with - | error err => rw [h_item] at hev_ok; simp [bind, Except.bind] at hev_ok - | ok vp => - rw [h_item] at hev_ok - have h_iexp := (hitem_iff vp).mpr h_item - rw [h_iexp] - simp [bind, Except.bind] at hev_ok ⊢ - by_cases hn : n = 0 - · simp [hn] at hev_ok ⊢; exact hev_ok - · simp [hn] at hev_ok ⊢ - cases vp with - | prim p => - cases p with - | bool b => simp at hev_ok ⊢; exact hev_ok - | _ => simp at hev_ok - | _ => simp at hev_ok - | some (.nDash n) => - by_cases hn0 : n = 0 - · simp [hn0, Cst.Unary.toExprOrSpecial?, hop] at hu - simp [Cst.Unary.evaluate, hop, hn0] - exact Cst.Member.toAExpr?_evaluate hu aexp heos v - · simp [Cst.Unary.toExprOrSpecial?, hop] at hu - simp [Cst.Unary.evaluate, hop, hn0] - have h_zero : (n.toNat = 0) ↔ (n = 0) := by - constructor - · intro h; exact UInt8.toNat_inj.mp (by simp [h]) - · intro h; rw [h]; rfl - have h_par : (n.toNat % 2 = 0) ↔ (n % 2 = 0) := by - rw [show n.toNat % 2 = (n % 2).toNat from by rw [UInt8.toNat_mod]; rfl] - constructor - · intro h; exact UInt8.toNat_inj.mp (by simp [h]) - · intro h; rw [h]; rfl - have hpos : n.toNat > 0 := by - by_contra h0; apply hn0; apply h_zero.mp; omega - have h_sub : (n - 1).toNat = n.toNat - 1 := by - have h1 : (UInt8.toNat 1) = 1 := by decide - rw [UInt8.toNat_sub, h1] - have hbnd : n.toNat < 256 := n.toNat_lt - omega - match hlit : CstCommon.Member.toLit? u.item with - | some (.liNum x) => - simp [hlit] at hu - match hcmp : compare x.toNat (Int64.MAX + 1).toNat with - | .gt => - rw [hcmp] at hu; simp at hu - | .eq => - rw [hcmp] at hu - simp at hu - simp [← hu, ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [dashN_evaluate_general (Expr.lit (.int Int64.MIN.toInt64)) (n - 1).toNat req es] - simp [evaluate] - have hMIN_neg : Int64.MIN.toInt64.neg? = none := by decide - rw [hMIN_neg] - have h_eq1 : ((n - 1).toNat = 0) ↔ (n = 1) := by - constructor - · intro h - have : n - 1 = 0 := UInt8.toNat_inj.mp (by simp; exact h) - have h2 := congrArg (· + 1) this - simp at h2 - omega - · intro h; rw [h]; rfl - simp [h_eq1, hcmp] - | .lt => - rw [hcmp] at hu - simp at hu - cases hofInt : Int64.ofInt? (x.toNat : Int) with - | none => rw [hofInt] at hu; cases hu - | some y => - rw [hofInt] at hu - simp at hu - simp [← hu, ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [dashN_evaluate_general (Expr.lit (.int (-y))) (n - 1).toNat req es] - simp [evaluate] - have hy_neg : y.neg? = some (-y) := by - show Int64.ofInt? (-y.toInt) = some (-y) - have hround : Int64.ofInt? ((-y).toInt) = some (-y) := Int64.ofInt?_toInt (-y) - have hy_range : Int64.MIN ≤ y.toInt ∧ y.toInt ≤ Int64.MAX := by - by_contra hnr - have : Int64.ofInt? y.toInt = none := by - apply Int64.ofInt?_none_iff.mp - by_cases hlo : Int64.MIN ≤ y.toInt - · right; by_contra hhi; apply hnr; exact ⟨hlo, by omega⟩ - · left; omega - rw [Int64.ofInt?_toInt] at this; cases this - have hyti_x : y.toInt = Int.ofNat x.toNat := by - have hofInt' : Int64.ofInt? (Int.ofNat x.toNat) = some y := hofInt - have hrange' : Int64.MIN ≤ Int.ofNat x.toNat ∧ Int.ofNat x.toNat ≤ Int64.MAX := by - by_contra hnr - have : Int64.ofInt? (Int.ofNat x.toNat) = none := by - apply Int64.ofInt?_none_iff.mp - by_cases hlo : Int64.MIN ≤ Int.ofNat x.toNat - · right; by_contra hhi; apply hnr; exact ⟨hlo, by omega⟩ - · left; omega - rw [this] at hofInt'; cases hofInt' - have hsome : Int64.ofInt? (Int.ofNat x.toNat) = - some (Int64.ofInt (Int.ofNat x.toNat)) := - Int64.ofInt?_some_iff.mp hrange' - rw [hsome] at hofInt'; injection hofInt' with hyeq - rw [← hyeq] - show BitVec.toInt (BitVec.ofInt 64 (Int.ofNat x.toNat)) = Int.ofNat x.toNat - rw [BitVec.toInt_ofInt] - have hmaxv : Int64.MAX = 9223372036854775807 := by decide - have hbound : Int.ofNat x.toNat ≤ 9223372036854775807 := by - have := hrange'.2; rw [hmaxv] at this; exact this - have h1 : -(2:Int)^63 ≤ Int.ofNat x.toNat := by - have hnn : (Int.ofNat x.toNat : Int) ≥ 0 := Int.natCast_nonneg _ - have : -(2:Int)^63 = -9223372036854775808 := by decide - rw [this]; omega - have h2 : Int.ofNat x.toNat < (2:Int)^63 := by - have : (2:Int)^63 = 9223372036854775808 := by decide - rw [this]; omega - exact Int.bmod_eq_of_le h1 h2 - have hy_nonneg : y.toInt ≥ 0 := by - rw [hyti_x]; exact Int.natCast_nonneg _ - have hneg_range : Int64.MIN ≤ -y.toInt ∧ -y.toInt ≤ Int64.MAX := by - simp [Int64.MIN, Int64.MAX] at hy_range ⊢; omega - have hyti : (-y).toInt = -y.toInt := by - show BitVec.toInt (-(y.toBitVec)) = -BitVec.toInt y.toBitVec - rw [BitVec.toInt_neg] - have hy : Int64.toInt y = BitVec.toInt y.toBitVec := rfl - rw [← hy] - apply Int.bmod_eq_of_le - · simp [Int64.MIN] at hneg_range; omega - · simp [Int64.MAX] at hneg_range; omega - rw [← hyti]; exact hround - have hneg_y : (-y).neg? = some y := Int64.neg?_neg? hy_neg - rw [hneg_y] - rw [h_sub] - rcases Nat.mod_two_eq_zero_or_one n.toNat with hpar | hpar - · have hge2 : n.toNat ≥ 2 := by omega - have h1 : n.toNat - 1 ≠ 0 := by omega - have h2 : (n.toNat - 1) % 2 = 1 := by omega - have h3 : (n % 2 = 0) := h_par.mp hpar - simp [h1, h2, h3, hcmp, hofInt] - · have h3 : n % 2 ≠ 0 := by - intro hcontra - have : n.toNat % 2 = 0 := h_par.mpr hcontra - omega - by_cases h1 : n.toNat - 1 = 0 - · simp [h1, h3, hcmp, hofInt] - · have h2 : (n.toNat - 1) % 2 = 0 := by omega - simp [h1, h2, h3, hcmp, hofInt] - | some .liTrue | some .liFalse | some (.liStr _) | none => - all_goals - simp [hlit] at hu - cases hitem_trans : u.item.toExprOrSpecial? with - | none => simp [hitem_trans] at hu - | some ieos => - simp [hitem_trans] at hu - cases hioes_trans : ieos.toExpr? with - | none => simp [hioes_trans] at hu - | some iexp => - simp [hioes_trans] at hu - simp [← hu, ExprOrSpecial.toExpr?] at heos - rw [← heos] - have hitem_iff : ∀ vp, evaluate iexp req es = .ok vp ↔ u.item.evaluate req es = .ok vp := - Cst.Member.toAExpr?_evaluate hitem_trans iexp hioes_trans - rw [dashN_evaluate_general iexp n.toNat req es] - simp [h_zero, h_par, hn0] - constructor - · intro hev_ok - cases h_iexp : evaluate iexp req es with - | error err => rw [h_iexp] at hev_ok; simp at hev_ok - | ok vp => - rw [h_iexp] at hev_ok - have h_item := (hitem_iff vp).mp h_iexp - simp [h_item, bind, Except.bind] - cases vp with - | prim p => - cases p with - | int i => simp at hev_ok ⊢; exact hev_ok - | _ => simp at hev_ok - | _ => simp at hev_ok - · intro hev_ok - cases h_item : u.item.evaluate req es with - | error err => rw [h_item] at hev_ok; simp [bind, Except.bind] at hev_ok - | ok vp => - rw [h_item] at hev_ok - have h_iexp := (hitem_iff vp).mpr h_item - rw [h_iexp] - simp [bind, Except.bind] at hev_ok ⊢ - cases vp with - | prim p => - cases p with - | int i => simp at hev_ok ⊢; exact hev_ok - | _ => simp at hev_ok - | _ => simp at hev_ok - | some .nOverBang => simp [Cst.Unary.toExprOrSpecial?, hop] at hu - | some .nOverDash => simp [Cst.Unary.toExprOrSpecial?, hop] at hu -termination_by (sizeOf u, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases u; simp only [Cst.Unary.mk.sizeOf_spec]; omega) - -theorem multExprFoldExtended_foldOps_agrees - (req : Request) (es : Entities) - (xs : List (Cst.MultOp × Cst.Unary)) - {acc_ast : Expr} {result : Expr} : - Cst.MultExpr.foldExtended acc_ast xs = some result → - ∀ v, evaluate result req es = .ok v ↔ - (do let acc_v ← evaluate acc_ast req es - Cst.MultExpr.foldOps acc_v xs req es) = .ok v := by - - intro hfold v - match xs with - | [] => - simp [Cst.MultExpr.foldExtended] at hfold - simp [hfold]; constructor <;> intro h - · simp [h, bind, Except.bind] - simp [Cst.MultExpr.foldOps] - · cases hres : evaluate result req es with - | error err => - simp [bind, Except.bind, hres] at h - | ok v' => - simp [bind, Except.bind, hres] at h - simp [Cst.MultExpr.foldOps] at h - rw [h] - - | (op, u) :: rest => - -- Translator only succeeds on .mTimes; other ops fail and contradict hfold. - cases hop : op with - | mTimes => - simp [Cst.MultExpr.foldExtended, hop] at hfold - cases hu : u.toAExpr? with - | none => rw [hu] at hfold; simp at hfold - | some eu => - rw [hu] at hfold - simp at hfold - have ih' := multExprFoldExtended_foldOps_agrees req es rest hfold v - rw [ih'] - simp [Cst.Unary.toAExpr?, Option.bind_eq_some_iff] at hu - obtain ⟨ueos, hueos, heu⟩ := hu - have hu_iff : ∀ vp, evaluate eu req es = .ok vp ↔ u.evaluate req es = .ok vp := - Cst.Unary.toAExpr?_evaluate hueos eu heu - -- Reduce both sides' do-notation and align via case splits. - simp [evaluate, bind, Except.bind, Cst.MultExpr.foldOps] - cases h_acc : evaluate acc_ast req es with - | error err => simp - | ok acc_v => - simp - cases h_eu : evaluate eu req es with - | error err => - simp - -- evaluate eu errors ⇒ u.evaluate also errors (or returns non-ok); RHS shorts. - cases h_u : u.evaluate req es with - | error _ => simp - | ok u_v => - -- contradiction: hu_iff u_v says evaluate eu = .ok u_v but h_eu = .error. - have := (hu_iff u_v).mpr h_u - rw [this] at h_eu; cases h_eu - | ok eu_v => - simp - have hu_v := (hu_iff eu_v).mp h_eu - rw [hu_v] - | _ => - simp [Cst.MultExpr.foldExtended, hop] at hfold -termination_by (sizeOf xs, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - simp only [List.cons.sizeOf_spec, Prod.mk.sizeOf_spec] at * - omega) - -theorem Cst.MultExpr.toAExpr?_evaluate - {mult : Cst.MultExpr} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - mult.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - mult.evaluate req es = .ok v := by - - intro hmult aexp heos v - match hext : mult.extended with - | [] => - simp only [Cst.MultExpr.toExprOrSpecial?, hext] at hmult - have hu_iff := @Cst.Unary.toAExpr?_evaluate mult.initial eos req es hmult aexp heos v - rw [hu_iff] - simp [Cst.MultExpr.evaluate] - cases h_init : mult.initial.evaluate req es with - | error err => simp [bind, Except.bind] - | ok iv => simp [bind, Except.bind, Cst.MultExpr.foldOps, hext] - | hd :: tl => - simp [Cst.MultExpr.toExprOrSpecial?, hext, Option.bind_eq_some_iff] at hmult - obtain ⟨first, hfirst, result, hres, heos_eq⟩ := hmult - rw [← heos_eq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [multExprFoldExtended_foldOps_agrees req es _ hres v] - simp [Cst.Unary.toAExpr?, Option.bind_eq_some_iff] at hfirst - obtain ⟨ueos, hueos, hfeu⟩ := hfirst - have hu_iff : ∀ vp, evaluate first req es = .ok vp ↔ mult.initial.evaluate req es = .ok vp := - Cst.Unary.toAExpr?_evaluate hueos first hfeu - simp [Cst.MultExpr.evaluate] - cases h_init : mult.initial.evaluate req es with - | error err => - simp [bind, Except.bind] - cases h_first : evaluate first req es with - | ok vp => - have := (hu_iff vp).mp h_first - rw [this] at h_init; cases h_init - | error _ => simp - | ok iv => - simp [bind, Except.bind, hext] - have h_first : evaluate first req es = .ok iv := (hu_iff iv).mpr h_init - rw [h_first] -termination_by (sizeOf mult, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases mult - simp only [Cst.MultExpr.mk.sizeOf_spec] - try (have h := hext; subst h) - omega) - -/-- Fold-helper analog for `AddExpr`. Mirrors `multExprFoldExtended_foldOps_agrees` - with `aPlus`/`aMinus` instead of `mTimes`, `MultExpr` instead of `Unary`, - and `apply₂ .add`/`apply₂ .sub` instead of `apply₂ .mul`. -/ -theorem addExprFoldExtended_foldOps_agrees - (req : Request) (es : Entities) - (xs : List (Cst.AddOp × Cst.MultExpr)) - {acc_ast : Expr} {result : Expr} : - Cst.AddExpr.foldExtended acc_ast xs = some result → - ∀ v, evaluate result req es = .ok v ↔ - (do let acc_v ← evaluate acc_ast req es - Cst.AddExpr.foldOps acc_v xs req es) = .ok v := by - intro hfold v - match xs with - | [] => - simp [Cst.AddExpr.foldExtended] at hfold - simp [hfold]; constructor <;> intro h - · simp [h, bind, Except.bind, Cst.AddExpr.foldOps] - · cases hres : evaluate result req es with - | error err => simp [bind, Except.bind, hres] at h - | ok v' => - simp [bind, Except.bind, hres] at h - simp [Cst.AddExpr.foldOps] at h - rw [h] - | (op, m) :: rest => - cases hop : op with - | aPlus => - simp [Cst.AddExpr.foldExtended, hop] at hfold - cases hm : m.toAExpr? with - | none => rw [hm] at hfold; simp at hfold - | some em => - rw [hm] at hfold - simp at hfold - have ih' := addExprFoldExtended_foldOps_agrees req es rest hfold v - rw [ih'] - simp [Cst.MultExpr.toAExpr?, Option.bind_eq_some_iff] at hm - obtain ⟨meos, hmeos, hmem⟩ := hm - have hm_iff : ∀ vp, evaluate em req es = .ok vp ↔ m.evaluate req es = .ok vp := - Cst.MultExpr.toAExpr?_evaluate hmeos em hmem - simp [evaluate, bind, Except.bind, Cst.AddExpr.foldOps] - cases h_acc : evaluate acc_ast req es with - | error err => simp - | ok acc_v => - simp - cases h_em : evaluate em req es with - | error err => - simp - cases h_m : m.evaluate req es with - | error _ => simp - | ok m_v => - have := (hm_iff m_v).mpr h_m - rw [this] at h_em; cases h_em - | ok em_v => - simp - have hm_v := (hm_iff em_v).mp h_em - rw [hm_v] - | aMinus => - simp [Cst.AddExpr.foldExtended, hop] at hfold - cases hm : m.toAExpr? with - | none => rw [hm] at hfold; simp at hfold - | some em => - rw [hm] at hfold - simp at hfold - have ih' := addExprFoldExtended_foldOps_agrees req es rest hfold v - rw [ih'] - simp [Cst.MultExpr.toAExpr?, Option.bind_eq_some_iff] at hm - obtain ⟨meos, hmeos, hmem⟩ := hm - have hm_iff : ∀ vp, evaluate em req es = .ok vp ↔ m.evaluate req es = .ok vp := - Cst.MultExpr.toAExpr?_evaluate hmeos em hmem - simp [evaluate, bind, Except.bind, Cst.AddExpr.foldOps] - cases h_acc : evaluate acc_ast req es with - | error err => simp - | ok acc_v => - simp - cases h_em : evaluate em req es with - | error err => - simp - cases h_m : m.evaluate req es with - | error _ => simp - | ok m_v => - have := (hm_iff m_v).mpr h_m - rw [this] at h_em; cases h_em - | ok em_v => - simp - have hm_v := (hm_iff em_v).mp h_em - rw [hm_v] -termination_by (sizeOf xs, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - simp only [List.cons.sizeOf_spec, Prod.mk.sizeOf_spec] at * - omega) - -theorem Cst.AddExpr.toAExpr?_evaluate - {add : Cst.AddExpr} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - add.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - add.evaluate req es = .ok v := by - intro hadd aexp heos v - match hext : add.extended with - | [] => - simp only [Cst.AddExpr.toExprOrSpecial?, hext] at hadd - have hm_iff := @Cst.MultExpr.toAExpr?_evaluate add.initial eos req es hadd aexp heos v - rw [hm_iff] - simp [Cst.AddExpr.evaluate] - cases h_init : add.initial.evaluate req es with - | error err => simp [bind, Except.bind] - | ok iv => simp [bind, Except.bind, Cst.AddExpr.foldOps, hext] - | hd :: tl => - simp [Cst.AddExpr.toExprOrSpecial?, hext, Option.bind_eq_some_iff] at hadd - obtain ⟨first, hfirst, result, hres, heos_eq⟩ := hadd - rw [← heos_eq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [addExprFoldExtended_foldOps_agrees req es _ hres v] - simp [Cst.MultExpr.toAExpr?, Option.bind_eq_some_iff] at hfirst - obtain ⟨ueos, hueos, hfeu⟩ := hfirst - have hu_iff : ∀ vp, evaluate first req es = .ok vp ↔ add.initial.evaluate req es = .ok vp := - Cst.MultExpr.toAExpr?_evaluate hueos first hfeu - simp [Cst.AddExpr.evaluate] - cases h_init : add.initial.evaluate req es with - | error err => - simp [bind, Except.bind] - cases h_first : evaluate first req es with - | ok vp => - have := (hu_iff vp).mp h_first - rw [this] at h_init; cases h_init - | error _ => simp - | ok iv => - simp [bind, Except.bind, hext] - have h_first : evaluate first req es = .ok iv := (hu_iff iv).mpr h_init - rw [h_first] -termination_by (sizeOf add, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases add - simp only [Cst.AddExpr.mk.sizeOf_spec] - try (have h := hext; subst h) - omega) - - -theorem Cst.Relation.toAExpr?_evaluate - {rel : Cst.Relation} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - rel.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - rel.evaluate req es = .ok v := by - intro hrel aexp heos v - cases rel with - | rCommon initial extended => - match hext : extended with - | [] => - simp [Cst.Relation.toExprOrSpecial?] at hrel - have hadd_iff := @Cst.AddExpr.toAExpr?_evaluate initial eos req es hrel aexp heos v - simp [Cst.Relation.evaluate] - exact hadd_iff - | [(op, x)] => - simp [Cst.Relation.toExprOrSpecial?] at hrel - simp only [Option.bind_eq_some_iff] at hrel - obtain ⟨ieos, hieos, eFirst, hFirst, eSecond, hSecond, hres⟩ := hrel - injection hres with hres - rw [← hres] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - have hinit_iff := - @Cst.AddExpr.toAExpr?_evaluate initial ieos req es hieos eFirst hFirst - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hSecond - obtain ⟨xeos, hxeos, hxsecond⟩ := hSecond - have hx_iff : ∀ vp, evaluate eSecond req es = .ok vp ↔ x.evaluate req es = .ok vp := - Cst.AddExpr.toAExpr?_evaluate hxeos eSecond hxsecond - simp [Cst.Relation.evaluate] - cases h_init : initial.evaluate req es with - | error err => - simp [bind, Except.bind] - cases h_first : evaluate eFirst req es with - | ok vp => - have := (hinit_iff vp).mp h_first - rw [this] at h_init; cases h_init - | error _ => - cases op <;> - simp [constructExprRel, evaluate, h_first, bind, Except.bind] - | ok iv => - simp [bind, Except.bind] - have h_first : evaluate eFirst req es = .ok iv := (hinit_iff iv).mpr h_init - cases h_x : x.evaluate req es with - | error err => - cases h_second : evaluate eSecond req es with - | ok xv => - have := (hx_iff xv).mp h_second - rw [this] at h_x; cases h_x - | error err' => - constructor - · intro hev - exfalso - cases op <;> simp [constructExprRel, evaluate, h_first, h_second, - bind, Except.bind] at hev - · intro hev - simp_all - | ok xv => - have h_second : evaluate eSecond req es = .ok xv := (hx_iff xv).mpr h_x - rw [constructExprRel_applyRelOp_agrees op eFirst eSecond req es iv xv h_first h_second] - | _ :: _ :: _ => - simp [Cst.Relation.toExprOrSpecial?] at hrel - | rHas target field => - simp [Cst.Relation.toExprOrSpecial?, Option.bind_eq_some_iff] at hrel - obtain ⟨mt, hmt, mf, hmf, hres⟩ := hrel - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hmt - obtain ⟨tEos, htEos, htExpr⟩ := hmt - have htarget_iff := - @Cst.AddExpr.toAExpr?_evaluate target tEos req es htEos mt htExpr - have hfield_attrs := addExpr_toHasRhs_toAttrs_agrees hmf - have hfield_nonempty := hasRhsToList_nonempty hmf - simp [Cst.Relation.evaluate, hfield_attrs] - cases mf with - | inl f => - simp at hres - rw [← hres] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - simp [hasRhsToList] - cases htgt : target.evaluate req es with - | error err => - simp [bind, Except.bind] - cases htgt' : evaluate mt req es with - | ok vt => - have := (htarget_iff vt).mp htgt' - rw [this] at htgt; cases htgt - | error _ => simp [evaluate, htgt', bind, Except.bind] - | ok vt => - have htgtMt : evaluate mt req es = .ok vt := (htarget_iff vt).mpr htgt - simp [evaluate, htgtMt, bind, Except.bind, Cst.rHasChain] - | inr fs => - simp at hres - rw [← hres] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - simp [hasRhsToList] at hfield_attrs hfield_nonempty - cases hfs : fs with - | nil => rw [hfs] at hfield_nonempty; simp at hfield_nonempty - | cons a as => - rw [hfs] at hfield_attrs - cases htgt : target.evaluate req es with - | error err => - simp [bind, Except.bind] - cases htgt' : evaluate mt req es with - | ok vt => - have := (htarget_iff vt).mp htgt' - rw [this] at htgt; cases htgt - | error _ => - cases as with - | nil => simp [extendedHasAttr, evaluate, htgt', bind, Except.bind] - | cons b bs => simp [extendedHasAttr, evaluate, htgt', bind, Except.bind, - Result.as] - | ok vt => - have htgtMt : evaluate mt req es = .ok vt := (htarget_iff vt).mpr htgt - rw [extendedHasAttr_evaluate_agrees mt a as req es vt htgtMt] - simp [hasRhsToList, bind, Except.bind] - | rLike target pattern => - simp [Cst.Relation.toExprOrSpecial?, Option.bind_eq_some_iff] at hrel - obtain ⟨mt, hmt, mp, hmp, hres⟩ := hrel - rw [← hres] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - -- Bridge target via Cst.AddExpr.toAExpr?_evaluate. - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hmt - obtain ⟨tEos, htEos, htExpr⟩ := hmt - have htarget_iff := - @Cst.AddExpr.toAExpr?_evaluate target tEos req es htEos mt htExpr - -- Bridge pattern via addExpr_toPattern_toPatternString_agrees. - obtain ⟨s, hpStr, hpToPattern⟩ := addExpr_toPattern_toPatternString_agrees hmp - simp [Cst.Relation.evaluate, hpStr] - cases htgt : target.evaluate req es with - | error err => - simp [bind, Except.bind] - cases htgt' : evaluate mt req es with - | ok vt => - have := (htarget_iff vt).mp htgt' - rw [this] at htgt; cases htgt - | error _ => - simp [evaluate, htgt', bind, Except.bind] - | ok vt => - have htgtMt : evaluate mt req es = .ok vt := (htarget_iff vt).mpr htgt - simp [evaluate, htgtMt, bind, Except.bind, hpToPattern] - | rIsIn target ety inEntity => - simp [Cst.Relation.toExprOrSpecial?, Option.bind_eq_some_iff] at hrel - have ⟨mt, hmt, et, hEt, hMatch⟩ := hrel - match hinE : inEntity, hMatch with - | none, hMatch => - simp at hMatch - subst hMatch - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - have hEtyName := addExpr_toEntityType_agrees hEt - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hmt - have ⟨tEos, htEos, htExpr⟩ := hmt - have htarget_iff := - @Cst.AddExpr.toAExpr?_evaluate target tEos req es htEos mt htExpr - simp [Cst.Relation.evaluate, hEt] - cases htgt : target.evaluate req es with - | error err => - simp [bind, Except.bind] - cases htgt' : evaluate mt req es with - | ok vt => - have := (htarget_iff vt).mp htgt' - rw [this] at htgt; cases htgt - | error _ => - simp [evaluate, htgt', bind, Except.bind] - | ok vt => - have htgtMt : evaluate mt req es = .ok vt := (htarget_iff vt).mpr htgt - simp only [evaluate, htgtMt, bind, Except.bind] - cases apply₁ (UnaryOp.is et) vt <;> simp - | some ie, hMatch => - simp [Option.bind_eq_some_iff] at hMatch - have ⟨mi, hmi, hres⟩ := hMatch - subst hres - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hmt - have ⟨tEos, htEos, htExpr⟩ := hmt - have htarget_iff := - @Cst.AddExpr.toAExpr?_evaluate target tEos req es htEos mt htExpr - have hie_trans : ie.toAExpr? = some mi := hmi - simp [Cst.AddExpr.toAExpr?, Option.bind_eq_some_iff] at hmi - have ⟨iEos, hiEos, hiExpr⟩ := hmi - have hinEntity_iff := - @Cst.AddExpr.toAExpr?_evaluate ie iEos req es hiEos mi hiExpr - exact rIsIn_some_eval_agrees hEt htarget_iff hinEntity_iff hie_trans v -termination_by (sizeOf rel, 0) -decreasing_by - all_goals (apply Prod.Lex.left; decreasing_tactic) - - -/-- Fold-helper analog for `AndExpr`. Mirrors `addExprFoldExtended_foldOps_agrees`, - with `Expr.and` replacing `binaryApp` and `Relation` replacing `MultExpr`. -/ -theorem andExprFoldExtended_foldOps_agrees - (req : Request) (es : Entities) - (xs : List Cst.Relation) - {acc_ast : Expr} {result : Expr} : - Cst.AndExpr.foldExtended acc_ast xs = some result → - ∀ v, evaluate result req es = .ok v ↔ - (do let acc_v ← evaluate acc_ast req es - Cst.AndExpr.foldOps acc_v xs req es) = .ok v := by - intro hfold v - match xs with - | [] => - simp [Cst.AndExpr.foldExtended] at hfold - simp [hfold]; constructor <;> intro h - · simp [h, bind, Except.bind, Cst.AndExpr.foldOps] - · cases hres : evaluate result req es with - | error err => simp [bind, Except.bind, hres] at h - | ok v' => - simp [bind, Except.bind, hres] at h - simp [Cst.AndExpr.foldOps] at h - rw [h] - | rel :: rest => - simp [Cst.AndExpr.foldExtended] at hfold - cases hrel : rel.toAExpr? with - | none => rw [hrel] at hfold; simp at hfold - | some erel => - rw [hrel] at hfold - simp at hfold - have ih' := andExprFoldExtended_foldOps_agrees req es rest hfold v - rw [ih'] - simp [Cst.Relation.toAExpr?, Option.bind_eq_some_iff] at hrel - obtain ⟨reos, hreos, hrm⟩ := hrel - have hrel_iff : ∀ vp, evaluate erel req es = .ok vp ↔ rel.evaluate req es = .ok vp := - Cst.Relation.toAExpr?_evaluate hreos erel hrm - simp [bind, Except.bind] - cases h_acc : evaluate acc_ast req es with - | error err => - simp [evaluate, h_acc, bind, Except.bind, Result.as] - | ok acc_v => - simp - exact expr_and_eval_eq_foldOps_step req es acc_ast erel acc_v rel rest h_acc hrel_iff v -termination_by (sizeOf xs, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - simp only [List.cons.sizeOf_spec] at * - omega) - -theorem Cst.AndExpr.toAExpr?_evaluate - {ae : Cst.AndExpr} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - ae.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - ae.evaluate req es = .ok v := by - intro hae aexp heos v - match hext : ae.extended with - | [] => - simp only [Cst.AndExpr.toExprOrSpecial?, hext] at hae - have hr_iff := @Cst.Relation.toAExpr?_evaluate ae.initial eos req es hae aexp heos v - rw [hr_iff] - simp [Cst.AndExpr.evaluate, hext] - cases h_init : ae.initial.evaluate req es with - | error err => simp [bind, Except.bind] - | ok iv => simp [bind, Except.bind, Cst.AndExpr.foldOps] - | hd :: tl => - simp [Cst.AndExpr.toExprOrSpecial?, hext, Option.bind_eq_some_iff] at hae - obtain ⟨first, hfirst, result, hres, heos_eq⟩ := hae - rw [← heos_eq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [andExprFoldExtended_foldOps_agrees req es _ hres v] - simp [Cst.Relation.toAExpr?, Option.bind_eq_some_iff] at hfirst - obtain ⟨reos, hreos, hfeu⟩ := hfirst - have hr_iff : ∀ vp, evaluate first req es = .ok vp ↔ ae.initial.evaluate req es = .ok vp := - Cst.Relation.toAExpr?_evaluate hreos first hfeu - have hall := andExprFoldExtended_some_all_translate _ hres - have hguard : (ae.extended.all fun r => r.toAExpr?.isSome) = true := by rw [hext]; exact hall - rw [AndExpr.evaluate_eq hguard] - cases h_init : ae.initial.evaluate req es with - | error err => - simp [bind, Except.bind] - cases h_first : evaluate first req es with - | ok vp => - have := (hr_iff vp).mp h_first - rw [this] at h_init; cases h_init - | error _ => simp - | ok iv => - simp [bind, Except.bind, hext] - have h_first : evaluate first req es = .ok iv := (hr_iff iv).mpr h_init - rw [h_first] -termination_by (sizeOf ae, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases ae - simp only [Cst.AndExpr.mk.sizeOf_spec] - try (have h := hext; subst h) - omega) - - -/-- Fold-helper analog for `OrExpr`. Mirrors `andExprFoldExtended_foldOps_agrees`, - with `Expr.or` replacing `Expr.and` and `AndExpr` replacing `Relation`. -/ -theorem orExprFoldExtended_foldOps_agrees - (req : Request) (es : Entities) - (xs : List Cst.AndExpr) - {acc_ast : Expr} {result : Expr} : - Cst.OrExpr.foldExtended acc_ast xs = some result → - ∀ v, evaluate result req es = .ok v ↔ - (do let acc_v ← evaluate acc_ast req es - Cst.OrExpr.foldOps acc_v xs req es) = .ok v := by - intro hfold v - match xs with - | [] => - simp [Cst.OrExpr.foldExtended] at hfold - simp [hfold]; constructor <;> intro h - · simp [h, bind, Except.bind, Cst.OrExpr.foldOps] - · cases hres : evaluate result req es with - | error err => simp [bind, Except.bind, hres] at h - | ok v' => - simp [bind, Except.bind, hres] at h - simp [Cst.OrExpr.foldOps] at h - rw [h] - | ande :: rest => - simp [Cst.OrExpr.foldExtended] at hfold - cases hande : ande.toAExpr? with - | none => rw [hande] at hfold; simp at hfold - | some eande => - rw [hande] at hfold - simp at hfold - have ih' := orExprFoldExtended_foldOps_agrees req es rest hfold v - rw [ih'] - simp [Cst.AndExpr.toAExpr?, Option.bind_eq_some_iff] at hande - obtain ⟨aeos, haeos, ham⟩ := hande - have hande_iff : ∀ vp, evaluate eande req es = .ok vp ↔ ande.evaluate req es = .ok vp := - Cst.AndExpr.toAExpr?_evaluate haeos eande ham - simp [bind, Except.bind] - cases h_acc : evaluate acc_ast req es with - | error err => - simp [evaluate, h_acc, bind, Except.bind, Result.as] - | ok acc_v => - simp - exact expr_or_eval_eq_foldOps_step req es acc_ast eande acc_v ande rest h_acc hande_iff v -termination_by (sizeOf xs, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - simp only [List.cons.sizeOf_spec] at * - omega) - -theorem Cst.OrExpr.toAExpr?_evaluate - {oe : Cst.OrExpr} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - oe.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - oe.evaluate req es = .ok v := by - intro hoe aexp heos v - match hext : oe.extended with - | [] => - simp only [Cst.OrExpr.toExprOrSpecial?, hext] at hoe - have ha_iff := @Cst.AndExpr.toAExpr?_evaluate oe.initial eos req es hoe aexp heos v - rw [ha_iff] - simp [Cst.OrExpr.evaluate, hext] - cases h_init : oe.initial.evaluate req es with - | error err => simp [bind, Except.bind] - | ok iv => simp [bind, Except.bind, Cst.OrExpr.foldOps] - | hd :: tl => - simp [Cst.OrExpr.toExprOrSpecial?, hext, Option.bind_eq_some_iff] at hoe - obtain ⟨first, hfirst, result, hres, heos_eq⟩ := hoe - rw [← heos_eq] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - rw [orExprFoldExtended_foldOps_agrees req es _ hres v] - simp [Cst.AndExpr.toAExpr?, Option.bind_eq_some_iff] at hfirst - obtain ⟨aeos, haeos, hfeu⟩ := hfirst - have ha_iff : ∀ vp, evaluate first req es = .ok vp ↔ oe.initial.evaluate req es = .ok vp := - Cst.AndExpr.toAExpr?_evaluate haeos first hfeu - have hall := orExprFoldExtended_some_all_translate _ hres - have hguard : (oe.extended.all fun r => r.toAExpr?.isSome) = true := by rw [hext]; exact hall - rw [OrExpr.evaluate_eq hguard] - cases h_init : oe.initial.evaluate req es with - | error err => - simp [bind, Except.bind] - cases h_first : evaluate first req es with - | ok vp => - have := (ha_iff vp).mp h_first - rw [this] at h_init; cases h_init - | error _ => simp - | ok iv => - simp [bind, Except.bind, hext] - have h_first : evaluate first req es = .ok iv := (ha_iff iv).mpr h_init - rw [h_first] -termination_by (sizeOf oe, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases oe - simp only [Cst.OrExpr.mk.sizeOf_spec] - try (have h := hext; subst h) - omega) - - -theorem Cst.ExprData.toAExpr?_evaluate - {ed : Cst.ExprData} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - ed.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - ed.evaluate req es = .ok v := by - intro hed aexp heos v - cases ed with - | edOr ore => - simp [Cst.ExprData.toExprOrSpecial?] at hed - simp [Cst.ExprData.evaluate] - exact Cst.OrExpr.toAExpr?_evaluate hed aexp heos v - | edIf i t f => - simp [Cst.ExprData.toExprOrSpecial?, Option.bind_eq_some_iff] at hed - obtain ⟨eg, hg, et, ht, ef, hf, hres⟩ := hed - have hguard : (t.toAExpr?.isSome && f.toAExpr?.isSome) = true := by - simp [ht, hf] - rw [← hres] at heos - simp [ExprOrSpecial.toExpr?] at heos - rw [← heos] - simp [Cst.Expr.toAExpr?, Option.bind_eq_some_iff] at hg ht hf - obtain ⟨gEos, hgEos, hgExpr⟩ := hg - obtain ⟨tEos, htEos, htExpr⟩ := ht - obtain ⟨fEos, hfEos, hfExpr⟩ := hf - have hg_iff : ∀ vp, evaluate eg req es = .ok vp ↔ i.evaluate req es = .ok vp := - Cst.Expr.toAExpr?_evaluate hgEos eg hgExpr - have ht_iff : ∀ vp, evaluate et req es = .ok vp ↔ t.evaluate req es = .ok vp := - Cst.Expr.toAExpr?_evaluate htEos et htExpr - have hf_iff : ∀ vp, evaluate ef req es = .ok vp ↔ f.evaluate req es = .ok vp := - Cst.Expr.toAExpr?_evaluate hfEos ef hfExpr - rw [ExprData.evaluate_edIf_eq hguard] - simp [evaluate, bind, Except.bind, Result.as, Coe.coe] - cases hg_eval : evaluate eg req es with - | error err => - cases hi : i.evaluate req es with - | ok iv => - have := (hg_iff iv).mpr hi - rw [this] at hg_eval; cases hg_eval - | error _ => simp - | ok gv => - have hi_ok : i.evaluate req es = .ok gv := (hg_iff gv).mp hg_eval - rw [hi_ok] - cases gv with - | prim p => - cases p with - | bool b => - simp [Value.asBool] - cases b with - | true => exact ht_iff v - | false => exact hf_iff v - | int _ | string _ | entityUID _ => simp [Value.asBool] - | set _ | record _ | ext _ => simp [Value.asBool] -termination_by (sizeOf ed, 0) -decreasing_by - all_goals (apply Prod.Lex.left; decreasing_tactic) - -theorem Cst.ExprImpl.toAExpr?_evaluate - {ei : Cst.ExprImpl} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - ei.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - ei.evaluate req es = .ok v := by - intro hei aexp heos v - simp only [Cst.ExprImpl.toExprOrSpecial?] at hei - simp [Cst.ExprImpl.evaluate] - exact Cst.ExprData.toAExpr?_evaluate hei aexp heos v -termination_by (sizeOf ei, 0) -decreasing_by - all_goals - (apply Prod.Lex.left - cases ei; simp only [Cst.ExprImpl.mk.sizeOf_spec]; omega) - -theorem Cst.Expr.toAExpr?_evaluate - {e : Cst.Expr} {eos : ExprOrSpecial} - {req : Request} {es : Entities} : - e.toExprOrSpecial? = some eos → - ∀ aexp, eos.toExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ - e.evaluate req es = .ok v := by - intro he aexp heos v - cases e with - | expr ei => - simp only [Cst.Expr.toExprOrSpecial?] at he - simp [Cst.Expr.evaluate] - exact Cst.ExprImpl.toAExpr?_evaluate he aexp heos v -termination_by (sizeOf e, 0) -decreasing_by - all_goals (apply Prod.Lex.left; decreasing_tactic) - -theorem expr_to_expr_agrees - {e : Cst.Expr} {aexp : Expr} {req : Request} {es : Entities} : - e.toAExpr? = some aexp → - ∀ v, evaluate aexp req es = .ok v ↔ e.evaluate req es = .ok v := by - intro h v - simp [Cst.Expr.toAExpr?] at h - cases heos : e.toExprOrSpecial? with - | none => simp [heos] at h - | some eos => - apply Cst.Expr.toAExpr?_evaluate heos aexp - simp [heos] at h; exact h - -end diff --git a/cedar-lean/Cedar/Thm/Translation/PolicyToExpr.lean b/cedar-lean/Cedar/Thm/Translation/PolicyToExpr.lean index 3ace845a2..7a92eeef3 100644 --- a/cedar-lean/Cedar/Thm/Translation/PolicyToExpr.lean +++ b/cedar-lean/Cedar/Thm/Translation/PolicyToExpr.lean @@ -12,7 +12,7 @@ namespace Cedar.Thm open Cedar.Data open Cedar.Spec -/-! ## Proof structure for `policy_to_expr_agrees` +/-! ## Proof structure for `policy_to_expr_sound` Both translation paths are rearrangements of a left-folded AST conjunction over a common leaf list `[principalScope, actionScope, resourceScope, conds…]`. The @@ -41,11 +41,6 @@ theorem evaluate_and_eq (x y : Expr) (req : Request) (es : Entities) : | error e => simp [bind, Except.bind] | ok b => cases b <;> simp [bind, Except.bind] -/-- Re-coercing a bool-wrapped result back through `.as Bool` is the identity. -/ -theorem as_bool_map (r : Result Bool) : - (Result.as Bool do let a ← r; pure (Value.prim (Prim.bool a))) = r := by - cases r <;> simp [Result.as, Coe.coe, Value.asBool, bind, Except.bind, pure, Except.pure] - /-- `.and` is associative over the full evaluation `Result` (incl. error and short-circuit behavior). This is what makes left- vs right-nesting agree. -/ theorem evaluate_and_assoc (a b c : Expr) (req : Request) (es : Entities) : @@ -84,61 +79,6 @@ theorem evaluate_and_true (x : Expr) (req : Request) (es : Entities) : cases b <;> simp [Result.as, Coe.coe, Value.asBool, Functor.map, Except.map, evaluate] -/-- `r.as Bool = .ok b` iff `r = .ok (.prim (.bool b))`. -/ -theorem as_bool_ok (r : Result Value) (b : Bool) : - r.as Bool = .ok b ↔ r = .ok (.prim (.bool b)) := by - cases r with - | error e => simp [Result.as] - | ok v => - cases v with - | prim p => cases p <;> simp [Result.as, Coe.coe, Value.asBool] - | _ => simp [Result.as, Coe.coe, Value.asBool] - -/-- `.and` is a congruence for iff-on-ok agreement. -/ -theorem and_congr_ok {a a' x x' : Expr} {req : Request} {es : Entities} - (ha : ∀ v, evaluate a req es = .ok v ↔ evaluate a' req es = .ok v) - (hx : ∀ v, evaluate x req es = .ok v ↔ evaluate x' req es = .ok v) : - ∀ v, evaluate (a.and x) req es = .ok v ↔ evaluate (a'.and x') req es = .ok v := by - have hab : ∀ b, (evaluate a req es).as Bool = .ok b ↔ (evaluate a' req es).as Bool = .ok b := by - intro b; rw [as_bool_ok, as_bool_ok]; exact ha _ - have hxb : ∀ b, (evaluate x req es).as Bool = .ok b ↔ (evaluate x' req es).as Bool = .ok b := by - intro b; rw [as_bool_ok, as_bool_ok]; exact hx _ - intro v - rw [evaluate_and_eq, evaluate_and_eq] - cases ha1 : (evaluate a req es).as Bool with - | error => - cases ha1' : (evaluate a' req es).as Bool with - | error => simp - | ok b' => have := (hab b').mpr ha1'; rw [ha1] at this; simp at this - | ok b => - have ha1' : (evaluate a' req es).as Bool = .ok b := (hab b).mp ha1 - rw [ha1'] - cases b with - | false => simp - | true => - cases hx1 : (evaluate x req es).as Bool with - | error => - cases hx1' : (evaluate x' req es).as Bool with - | error => simp [bind, Except.bind] - | ok b' => have := (hxb b').mpr hx1'; rw [hx1] at this; simp at this - | ok bx => - have hx1' : (evaluate x' req es).as Bool = .ok bx := (hxb bx).mp hx1 - simp [hx1'] - -/-- Pointwise iff-on-ok leaves ⇒ iff-on-ok conjunction evaluation. -/ -theorem bigAnd_congr (a a' : Expr) (l l' : List Expr) (req : Request) (es : Entities) : - (∀ v, evaluate a req es = .ok v ↔ evaluate a' req es = .ok v) → - List.Forall₂ (fun e e' => ∀ v, evaluate e req es = .ok v ↔ evaluate e' req es = .ok v) l l' → - ∀ v, evaluate (bigAnd a l) req es = .ok v ↔ evaluate (bigAnd a' l') req es = .ok v := by - intro ha h - induction h generalizing a a' with - | nil => simpa [bigAnd] using ha - | cons hr _ ih => - simp only [bigAnd, List.foldl_cons] - exact ih (a.and _) (a'.and _) (and_congr_ok ha hr) - -/- ===== Layer B: path 1 translation (`foldAnd` → `bigAnd`) ===== -/ - /-- `AndExpr.foldExtended` over lifted relations is exactly `bigAnd`. -/ theorem foldExtended_eq_bigAnd (acc : Expr) (l : List Cst.Expr) (aes : List Expr) : l.mapM Cst.Expr.toAExpr? = some aes → @@ -341,33 +281,6 @@ theorem evaluate_policy_toExpr (ap : Policy) (req : Request) (es : Entities) : /- ===== Layer D: per-leaf agreement ===== -/ -/-- Singleton-set membership ≡ bare-entity membership (action-scope `in uid`). -/ -theorem evaluate_mem_singleton (v : Var) (uid : EntityUID) (req : Request) (es : Entities) : - ∀ val, evaluate (.binaryApp .mem (.var v) (.set [.lit (.entityUID uid)])) req es = .ok val ↔ - evaluate (.binaryApp .mem (.var v) (.lit (.entityUID uid))) req es = .ok val := by - have hels : (Set.make [Value.prim (Prim.entityUID uid)]).elts = [Value.prim (Prim.entityUID uid)] := by - simp [Set.make, Set.elts, List.canonicalize_singleton] - have key : ∀ val1 : Value, - apply₂ .mem val1 (.set (Set.make [.prim (.entityUID uid)])) es - = apply₂ .mem val1 (.prim (.entityUID uid)) es := by - intro val1 - cases val1 with - | prim p => - cases p with - | entityUID a => - have huids : (Set.make [uid]).elts = [uid] := by - simp [Set.make, Set.elts, List.canonicalize_singleton] - simp only [apply₂, inₛ, Set.mapOrErr, hels, List.mapM_cons, List.mapM_nil, - Value.asEntityUID, bind, Except.bind, pure, Except.pure, Set.any, huids, List.any, - Bool.or_false] - | _ => simp [apply₂] - | _ => simp [apply₂] - have heq : evaluate (.binaryApp .mem (.var v) (.set [.lit (.entityUID uid)])) req es = - evaluate (.binaryApp .mem (.var v) (.lit (.entityUID uid))) req es := by - simp only [evaluate, List.mapM₁_eq_mapM (fun e => evaluate e req es), List.mapM_cons, - List.mapM_nil, bind, Except.bind, pure, Except.pure, key] - intro val; rw [heq] - /-- Shared core: the principal/resource leaf equals `Scope.toExpr scope v`, given the scope variable translates to `Expr.var v`. -/ theorem toPRScope_leaf {vd : Cst.VariableDef} {scope : Scope} {leaf : Expr} {v : Var} @@ -438,138 +351,6 @@ theorem toPRScope_leaf {vd : Cst.VariableDef} {scope : Scope} {leaf : Expr} {v : | some (.rGreaterEq, e), _, hscope => simp [Cst.VariableDef.toPRScope?] at hscope | some (.rNotEq, e), _, hscope => simp [Cst.VariableDef.toPRScope?] at hscope -/-- Principal-scope leaf agrees between the two paths. -/ -theorem principal_leaf_agrees {vp : Cst.VariableDef} {ps : PrincipalScope} {leaf : Expr} - (req : Request) (es : Entities) : - vp.toPrincipalScope? = some ps → - vp.toExpr.toAExpr? = some leaf → - ∀ val, evaluate leaf req es = .ok val ↔ evaluate ps.toExpr req es = .ok val := by - intro hps hleaf val - simp only [Cst.VariableDef.toPrincipalScope?] at hps - split at hps <;> [skip; simp at hps] - rename_i hvar - simp [Option.bind_eq_some_iff] at hps - obtain ⟨scope, hscope, hps⟩ := hps - subst hps - have hv : (vp.var.varToAddExpr).toExprOrSpecial? = some (ExprOrSpecial.var .principal) := by - rw [hvar]; simp [Cst.Ident.varToAddExpr, Cst.Primary.toMember, Cst.Member.toUnary, - Cst.Unary.toMultExpr, Cst.MultExpr.toAddExpr, Cst.AddExpr.toExprOrSpecial?, - Cst.MultExpr.toExprOrSpecial?, Cst.Unary.toExprOrSpecial?, Cst.Member.toExprOrSpecial?, - Cst.Primary.toExprOrSpecial?, Cst.Name.toVar?, memberAuxA, memberAux] - rw [toPRScope_leaf hv hscope hleaf]; exact Iff.rfl - -/-- Resource-scope leaf agrees between the two paths. -/ -theorem resource_leaf_agrees {vr : Cst.VariableDef} {rs : ResourceScope} {leaf : Expr} - (req : Request) (es : Entities) : - vr.toResourceScope? = some rs → - vr.toExpr.toAExpr? = some leaf → - ∀ val, evaluate leaf req es = .ok val ↔ evaluate rs.toExpr req es = .ok val := by - intro hrs hleaf val - simp only [Cst.VariableDef.toResourceScope?] at hrs - split at hrs <;> [skip; simp at hrs] - rename_i hvar - simp [Option.bind_eq_some_iff] at hrs - obtain ⟨scope, hscope, hrs⟩ := hrs - subst hrs - have hv : (vr.var.varToAddExpr).toExprOrSpecial? = some (ExprOrSpecial.var .resource) := by - rw [hvar]; simp [Cst.Ident.varToAddExpr, Cst.Primary.toMember, Cst.Member.toUnary, - Cst.Unary.toMultExpr, Cst.MultExpr.toAddExpr, Cst.AddExpr.toExprOrSpecial?, - Cst.MultExpr.toExprOrSpecial?, Cst.Unary.toExprOrSpecial?, Cst.Member.toExprOrSpecial?, - Cst.Primary.toExprOrSpecial?, Cst.Name.toVar?, memberAuxA, memberAux] - rw [toPRScope_leaf hv hscope hleaf]; exact Iff.rfl - -/-- Action-scope leaf agrees between the two paths (uses `evaluate_mem_singleton` - for the single-entity `in` case). -/ -theorem action_leaf_agrees {va : Cst.VariableDef} {as : ActionScope} {leaf : Expr} - (req : Request) (es : Entities) : - va.toActionScope? = some as → - va.toExpr.toAExpr? = some leaf → - ∀ val, evaluate leaf req es = .ok val ↔ evaluate as.toExpr req es = .ok val := by - intro has hleaf val - have collapse : ∀ r : Cst.Relation, - ({initial := r, extended := []} : Cst.AndExpr).toOrExpr.toExpr.toAExpr? = r.toAExpr? := by - intro r - simp [Cst.AndExpr.toOrExpr, Cst.OrExpr.toExpr, Cst.Expr.toAExpr?, Cst.Expr.toExprOrSpecial?, - Cst.ExprImpl.toExprOrSpecial?, Cst.ExprData.toExprOrSpecial?, Cst.OrExpr.toExprOrSpecial?, - Cst.AndExpr.toExprOrSpecial?, Cst.Relation.toAExpr?] - obtain ⟨var, et, ineq⟩ := va - simp only [Cst.VariableDef.toExpr, Cst.VariableDef.toAndExpr] at hleaf - cases var - case idAction => - have hv : (Cst.Ident.idAction.varToAddExpr).toExprOrSpecial? = some (ExprOrSpecial.var .action) := by - simp [Cst.Ident.varToAddExpr, Cst.Primary.toMember, Cst.Member.toUnary, Cst.Unary.toMultExpr, - Cst.MultExpr.toAddExpr, Cst.AddExpr.toExprOrSpecial?, Cst.MultExpr.toExprOrSpecial?, - Cst.Unary.toExprOrSpecial?, Cst.Member.toExprOrSpecial?, Cst.Primary.toExprOrSpecial?, - Cst.Name.toVar?, memberAuxA, memberAux] - have hv2 : (Cst.Ident.idAction.varToAddExpr).toAExpr? = some (Expr.var .action) := by - simp [Cst.AddExpr.toAExpr?, hv, ExprOrSpecial.toExpr?] - cases et - case some t => - simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - case none => - cases ineq with - | none => - simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, - ActionScope.containsOnlyActionTypes?] at has - subst has - rw [collapse] at hleaf - simp [Cst.Relation.tt, Cst.Primary.toMember, Cst.Member.toUnary, Cst.Unary.toMultExpr, - Cst.MultExpr.toAddExpr, Cst.AddExpr.toRelation, Cst.Relation.toAExpr?, - Cst.Relation.toExprOrSpecial?, Cst.AddExpr.toExprOrSpecial?, Cst.MultExpr.toExprOrSpecial?, - Cst.Unary.toExprOrSpecial?, Cst.Member.toExprOrSpecial?, Cst.Primary.toExprOrSpecial?, - Cst.Literal.toExprOrSpecial?, memberAuxA, memberAux, ExprOrSpecial.toExpr?] at hleaf - rw [← hleaf]; rfl - | some opE => - obtain ⟨op, e⟩ := opE - cases op with - | rEq => - cases huid : e.toEntityUID? with - | none => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, huid] at has - | some uid => - simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, huid, - ] at has - obtain ⟨hcheck, hsc⟩ := has - subst hsc - rw [collapse] at hleaf - simp [Cst.Relation.toAExpr?, Cst.Relation.toExprOrSpecial?, hv, constructExprRel, - toAddExpr_toAExpr, toEntityUID_toAExpr huid, ExprOrSpecial.toExpr?, - ] at hleaf - rw [← hleaf]; rfl - | rIn => - cases hr : e.toMultipleEntityUID? with - | none => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, - Cst.Expr.toEntityUIDs?, hr] at has - | some r => - have hmem := expr_mem_toAExpr hr - have hleaf' : leaf = Expr.binaryApp .mem (.var .action) (memToExpr r) := by - rw [collapse] at hleaf - simp [Cst.Relation.toAExpr?, Cst.Relation.toExprOrSpecial?, hv, constructExprRel, - toAddExpr_toAExpr, hmem, ExprOrSpecial.toExpr?] at hleaf - rw [← hleaf] - cases r with - | inl uid => - simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, - Cst.Expr.toEntityUIDs?, hr] at has - obtain ⟨hcheck, hsc⟩ := has - subst hsc - subst hleaf' - simp only [memToExpr, ActionScope.toExpr, List.map_cons, List.map_nil] - exact (evaluate_mem_singleton _ uid req es val).symm - | inr uids => - simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?, - Cst.Expr.toEntityUIDs?, hr] at has - obtain ⟨hcheck, hsc⟩ := has - subst hsc - subst hleaf' - simp only [memToExpr, ActionScope.toExpr] - | rLess => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - | rLessEq => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - | rGreater => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - | rGreaterEq => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - | rNotEq => simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - all_goals simp [Cst.VariableDef.toActionScope?, Cst.VariableDef.toActionScopeAux?] at has - - /-- Per-condition agreement: a condition's `foldAnd` leaf equals its AST `Condition.toExpr`. -/ theorem cond_leaf_eq {c : Cst.Cond} {cond : Condition} {leaf : Expr} : @@ -607,67 +388,6 @@ theorem cond_leaves_eq (conds : List Cst.Cond) (condLeaves : List Expr) (apConds have hrest := ih lrest condrest hlrest hcondrest subst hcl; subst hap; subst hper; subst hrest; rfl -/-- Reflexivity of the iff-on-ok `Forall₂` relation. -/ -theorem forall₂_iff_refl (l : List Expr) (req : Request) (es : Entities) : - List.Forall₂ (fun e e' => ∀ v, evaluate e req es = .ok v ↔ evaluate e' req es = .ok v) l l := by - induction l with - | nil => exact List.Forall₂.nil - | cons x xs ih => exact List.Forall₂.cons (fun _ => Iff.rfl) ih - -/-- The two translation paths from a CST policy to an AST expression - (`cp → CST Expr → AST Expr` and `cp → AST Policy → AST Expr`) are - *semantically* equivalent: on every request/entities, the two resulting AST - expressions evaluate to the same value (agreement on successful `.ok` - results). -/ -theorem policy_to_expr_agrees (cp : Cst.Policy) (ap : Policy) - (ce : Cst.Expr) (ae : Expr) (req : Request) (es : Entities) : - cp.toPolicy? = some ap → - cp.toExpr = ce → - ce.toAExpr? = some ae → - ∀ val, evaluate ae req es = .ok val ↔ evaluate ap.toExpr req es = .ok val := by - intro hap hce hae val - obtain ⟨⟨eff, vars, conds⟩⟩ := cp - -- Path 1: `ce = foldAnd (vars.map toExpr ++ conds.map Cond.toExpr)`. - rw [← hce] at hae - simp only [Cst.Policy.toExpr, Cst.PolicyImpl.toExpr] at hae - -- Invert `toPolicy?` (treating the sub-translations as opaque). - simp only [Cst.Policy.toPolicy?, Cst.PolicyImpl.toPolicy?, bind, Option.bind_eq_some_iff, - Option.some.injEq] at hap - obtain ⟨eff', heff, ⟨ps, as, rs⟩, hsc, apConds, hconds, hapeq⟩ := hap - subst hapeq - -- Invert `extractScope?`: exactly three scope variables. - match vars, hsc, hae with - | [vp, va, vr], hscope, hae => - simp only [extractScope?, bind, Option.bind_eq_some_iff] at hscope - obtain ⟨ps', hps, as', has, rs', hrs, rfl, rfl, rfl⟩ := hscope - -- Path 1: `ae = bigAnd Lp [La, Lr, condLeaves…]`. - obtain ⟨leaves, hmapM, haeForm⟩ := foldAnd_inv _ ae hae - rw [List.map_cons, List.map_cons, List.map_cons, List.map_nil, List.cons_append, - List.cons_append, List.cons_append, List.nil_append, List.mapM_cons] at hmapM - simp only [bind, Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at hmapM - obtain ⟨Lp, hLp, rest1, hrest1, e1⟩ := hmapM - rw [List.mapM_cons] at hrest1; simp only [bind, Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at hrest1 - obtain ⟨La, hLa, rest2, hrest2, e2⟩ := hrest1 - rw [List.mapM_cons] at hrest2; simp only [bind, Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at hrest2 - obtain ⟨Lr, hLr, condLeaves, hcond, e3⟩ := hrest2 - subst e1; subst e2; subst e3 - -- condition leaves equal the AST condition exprs. - have hcondeq : condLeaves = apConds.map Condition.toExpr := - cond_leaves_eq conds condLeaves apConds hcond (by simpa [toConditions?] using hconds) - subst haeForm - -- Path 2: normalize `ap.toExpr` to `bigAnd`. - rw [evaluate_policy_toExpr] - -- Apply the conjunction congruence. - apply bigAnd_congr - · exact principal_leaf_agrees req es hps hLp - · refine List.Forall₂.cons (action_leaf_agrees req es has hLa) ?_ - refine List.Forall₂.cons (resource_leaf_agrees req es hrs hLr) ?_ - rw [hcondeq]; exact forall₂_iff_refl _ req es - | [], hscope, _ => simp [extractScope?] at hscope - | [_], hscope, _ => simp [extractScope?] at hscope - | [_, _], hscope, _ => simp [extractScope?] at hscope - | _ :: _ :: _ :: _ :: _, hscope, _ => simp [extractScope?] at hscope - /- ===== Full-`Except`-equality analogs (for `policy_to_expr_sound`) ===== -/ /-- Full-equality congruence for `.and`: `evaluate (a.and x)` is determined @@ -696,8 +416,8 @@ theorem forall₂_eval_refl (l : List Expr) (req : Request) (es : Entities) : | nil => exact List.Forall₂.nil | cons _ _ ih => exact List.Forall₂.cons rfl ih -/-- Full-equality version of `evaluate_mem_singleton`: membership against a - singleton set equals membership against the bare literal. -/ +/-- Membership against a singleton set equals membership against the bare + literal (action-scope `in uid`), as a full evaluation equality. -/ theorem evaluate_mem_singleton_eq (v : Var) (uid : EntityUID) (req : Request) (es : Entities) : evaluate (.binaryApp .mem (.var v) (.set [.lit (.entityUID uid)])) req es = evaluate (.binaryApp .mem (.var v) (.lit (.entityUID uid))) req es := by