diff options
Diffstat (limited to 'rego-proofs')
| -rw-r--r-- | rego-proofs/.gitignore | 3 | ||||
| -rw-r--r-- | rego-proofs/Rego/Rego.lean | 614 | ||||
| -rw-r--r-- | rego-proofs/Rego/lake-manifest.json | 55 | ||||
| -rw-r--r-- | rego-proofs/Rego/lakefile.lean | 14 | ||||
| -rw-r--r-- | rego-proofs/Rego/lean-toolchain | 1 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 6 |
6 files changed, 631 insertions, 62 deletions
diff --git a/rego-proofs/.gitignore b/rego-proofs/.gitignore new file mode 100644 index 0000000..73368ec --- /dev/null +++ b/rego-proofs/.gitignore @@ -0,0 +1,3 @@ +.lake/ +_build/ +*.olean diff --git a/rego-proofs/Rego/Rego.lean b/rego-proofs/Rego/Rego.lean index ce52b89..717a62c 100644 --- a/rego-proofs/Rego/Rego.lean +++ b/rego-proofs/Rego/Rego.lean @@ -1,5 +1,8 @@ +import Aesop import Lean.Data.AssocList import Lean.Data.Json +import Mathlib.Init.Logic +import Mathlib.Tactic.LibrarySearch namespace Rego @@ -7,64 +10,603 @@ inductive Any where -- Scalar types | null | bool (b : Bool) - | num (n : Lean.JsonNumber) + | num (n : Nat) | str (s : String) -- Composite types | array (xs : Array Any) | set (elts : List Any) -- FIXME: `List` obviously isn't correct here. - | object (field : Lean.AssocList String Any) + | object (field : Lean.AssocList Any Any) deriving Inhabited namespace Any -def expectBool (x : Any) : Option Bool := - if let Any.bool b := x then some b else none - -def expectNumber (x : Any) : Option Lean.JsonNumber := - if let Any.num n := x then some n else none - -def expectArray (x : Any) : Option (Array Any) := - if let Any.array y := x then some y else none - -def expectObject (x : Any) : Option (Lean.AssocList String Any) := - if let Any.object y := x then some y else none - -end Any - --- TODO: Complete implementation def eqv : Any → Any → Bool | Any.null, Any.null => True | Any.bool b₁, Any.bool b₂ => b₁ = b₂ + | Any.str s₁, Any.str s₂ => s₁ = s₂ + -- TODO: array, set, object | _, _ => False instance : BEq Any where beq := eqv -abbrev Set := List -abbrev Number := Lean.JsonNumber -abbrev Object := Lean.AssocList String Any +def deref (target : Any) (field : Any) : Any := + match target with + | array xs => + (match field with + | num x => xs.getD x Any.null + | _ => Any.null) + | set xs => + (match field with + | num x => xs.getD x Any.null + | _ => Any.null) + | object fields => + (match field with + | str s => Option.getD (fields.find? (str s)) Any.null + -- TODO: Coe to str + | _ => Any.null + ) + | _ => Any.null -namespace Number -def toNat' (n : Number) : Option Nat := - if n.exponent = 0 && n.mantissa ≥ 0 then - some (Int.toNat n.mantissa) - else none +end Any -end Number +def scalar_specified_by (x : Any) (ind : Any → Prop) : Prop := ind x -namespace Object +def set_specified_by (x : Any) (ind : Any → Prop) : Prop := + match x with + | Any.set xs => ∀ (k : Rego.Any), k ∈ xs ↔ ind k + | _ => False -def ref (obj : Object) (attr : String) : Option Any := - Lean.AssocList.find? attr obj +def object_specified_by (x : Any) (ind : Any → Prop) : Prop := + match x with + | Any.object xs => ∀ (k v : Rego.Any), (xs.find? k = some v) ↔ ind k + | _ => False -end Object +end Rego -def obj_eqv (x y : Object) : Bool := - (List.map Prod.snd (Lean.AssocList.toList x)) - == (List.map Prod.snd (Lean.AssocList.toList y)) +def eq (a b : Rego.Any) := if a == b then Rego.Any.bool true else Rego.Any.bool false +def equal (a b : Rego.Any) := if a == b then Rego.Any.bool true else Rego.Any.bool false -instance : BEq Object where - beq := obj_eqv +inductive XmlType + | string : XmlType + | boolean : XmlType + | integer : XmlType + | double : XmlType + | time : XmlType + | date : XmlType + | dateTime : XmlType + | anyURI : XmlType + | hexBinary : XmlType + | base64Binary : XmlType + | dayTimeDuration : XmlType + | yearMonthDuration : XmlType + | x500Name : XmlType + | rfc822Name : XmlType + | ipAddress : XmlType + | dnsName : XmlType +deriving BEq, Repr -end Rego +instance : LawfulBEq XmlType where + eq_of_beq {a b} h := by cases a <;> cases b <;> first | rfl | contradiction + rfl {a} := by cases a <;> decide + +structure AttributeDesignator where + category : String + identifier : String + type : XmlType + issuer : Option String + must_be_present : Bool +deriving BEq, Repr + +def Primitive : Type := XmlType × String +deriving BEq, Repr + +def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner) + +structure Bag where + contents: List Primitive +deriving Repr + +def Bag.beq (b₁ b₂ : Bag) : Bool := + b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x) + +instance : BEq Bag where + beq := Bag.beq + +inductive Value where + | primitive (p : Primitive) : Value + | bag (b : Bag) : Value +deriving BEq, Repr + +structure Attribute where + category : String + identifier : String + issuer : Option String + value : Primitive +deriving Repr + +inductive StatusCode + | ok : StatusCode + | missing_attribute : StatusCode + | syntax_error : StatusCode + | processing_error : StatusCode +deriving BEq, Repr + +namespace AttributeDesignator + def eval (designator : AttributeDesignator) (context : List Attribute) : Sum Value (List StatusCode) := + match designator with + | AttributeDesignator.mk category identifier type issuer must_be_present => + let found := + -- A named attribute SHALL match an attribute if the values of + -- their respective Category, AttributeId, DataType and Issuer + -- attributes match. The attribute designator’s Category MUST + -- match, by identifier equality, the Category of the + -- <Attributes> element in which the attribute is present. The + -- attribute designator’s AttributeId MUST match, by identifier + -- equality, the AttributeId of the attribute. The attribute + -- designator’s DataType MUST match, by identifier equality, the + -- DataType of the same attribute. + -- + -- If the Issuer attribute is present in the attribute + -- designator, then it MUST match, using the + -- “urn:oasis:names:tc:xacml:1.0:function:string-equal” + -- function, the Issuer of the same attribute. If the Issuer is + -- not present in the attribute designator, then the matching of + -- the attribute to the named attribute SHALL be governed by + -- AttributeId and DataType attributes alone. + context.filter (fun (attr : Attribute) => + attr.category == category + ∧ attr.identifier == identifier + ∧ attr.value.fst == type + ∧ (attr.issuer == Option.none ∨ attr.issuer == issuer)) + let found := found.map (fun x => x.value) + if must_be_present then + match found with + | [] => Sum.inr $ [StatusCode.missing_attribute] + | _ => Sum.inl $ Value.bag (Bag.mk found) + else Sum.inl $ Value.bag (Bag.mk found) +end AttributeDesignator + +def attribute_matches (designator : AttributeDesignator) (attr : Attribute) : Prop := + match designator with + | AttributeDesignator.mk category identifier type issuer _ => + attr.category == category + ∧ attr.identifier == identifier + ∧ attr.value.fst == type + ∧ (attr.issuer == Option.none ∨ attr.issuer == issuer) + +def string_of_xmltype : XmlType → String + | XmlType.string => "string" + | XmlType.boolean => "boolean" + | XmlType.integer => "integer" + | XmlType.double => "double" + | XmlType.time => "time" + | XmlType.date => "date" + | XmlType.dateTime => "dateTime" + | XmlType.anyURI => "anyURI" + | XmlType.hexBinary => "hexBinary" + | XmlType.base64Binary => "base64Binary" + | XmlType.dayTimeDuration => "dayTimeDuration" + | XmlType.yearMonthDuration => "yearMonthDuration" + | XmlType.x500Name => "x500Name" + | XmlType.rfc822Name => "rfc822Name" + | XmlType.ipAddress => "ipAddress" + | XmlType.dnsName => "dnsName" + +@[simp] def toAssocList : List (α × β) → Lean.AssocList α β + | [] => Lean.AssocList.nil + | (a,b) :: es => Lean.AssocList.cons a b (toAssocList es) + +def rego_of_primitive : Primitive → Rego.Any + | (type, value) => + Rego.Any.object + (toAssocList + [(Rego.Any.str "kind" , Rego.Any.str "primitive"), + (Rego.Any.str "type" , Rego.Any.str (string_of_xmltype type)), + (Rego.Any.str "value" , Rego.Any.str value)]) + +def rego_of_attribute_designator : AttributeDesignator → Rego.Any + | AttributeDesignator.mk category identifier type (some issuer) must_be_present => + Rego.Any.object + (toAssocList + [(Rego.Any.str "category" , Rego.Any.str category), + (Rego.Any.str "identifier" , Rego.Any.str identifier), + (Rego.Any.str "type" , Rego.Any.str (string_of_xmltype type)), + (Rego.Any.str "issuer" , Rego.Any.str issuer), + (Rego.Any.str "must_be_present" , Rego.Any.bool must_be_present)]) + | AttributeDesignator.mk category identifier type (none) must_be_present => + Rego.Any.object + (toAssocList + [(Rego.Any.str "category" , Rego.Any.str category), + (Rego.Any.str "identifier" , Rego.Any.str identifier), + (Rego.Any.str "type" , Rego.Any.str (string_of_xmltype type)), + (Rego.Any.str "must_be_present" , Rego.Any.bool must_be_present)]) + +def rego_of_attribute : Attribute → Rego.Any + | Attribute.mk category identifier (some issuer) value => + Rego.Any.object + (toAssocList + [(Rego.Any.str "category" , Rego.Any.str category), + (Rego.Any.str "identifier" , Rego.Any.str identifier), + (Rego.Any.str "issuer" , Rego.Any.str issuer), + (Rego.Any.str "value" , (rego_of_primitive value))]) + | Attribute.mk category identifier _ value => + Rego.Any.object + (toAssocList + [(Rego.Any.str "category" , Rego.Any.str category), + (Rego.Any.str "identifier" , Rego.Any.str identifier), + (Rego.Any.str "value" , (rego_of_primitive value))]) + +inductive designator_matches (varg__1 varg__2 vy__0 : Rego.Any) : Prop where + | rule0 : (And (Ne (eq vy__0 (Rego.Any.bool True)) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "issuer")) (Rego.Any.null )) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref (Rego.Any.deref varg__2 (Rego.Any.str "value")) (Rego.Any.str "type")) (Rego.Any.deref varg__1 (Rego.Any.str "type"))) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "identifier")) (Rego.Any.deref varg__1 (Rego.Any.str "identifier"))) (Rego.Any.bool False)) + (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "category")) (Rego.Any.deref varg__1 (Rego.Any.str "category"))) (Rego.Any.bool False)))))) + → designator_matches varg__1 varg__2 vy__0 + | rule1 : (And (Ne (eq vy__0 (Rego.Any.bool True)) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "issuer")) (Rego.Any.deref varg__1 (Rego.Any.str "issuer"))) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref (Rego.Any.deref varg__2 (Rego.Any.str "value")) (Rego.Any.str "type")) (Rego.Any.deref varg__1 (Rego.Any.str "type"))) (Rego.Any.bool False)) + (And (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "identifier")) (Rego.Any.deref varg__1 (Rego.Any.str "identifier"))) (Rego.Any.bool False)) + (Ne (equal (Rego.Any.deref varg__2 (Rego.Any.str "category")) (Rego.Any.deref varg__1 (Rego.Any.str "category"))) (Rego.Any.bool False)))))) + → designator_matches varg__1 varg__2 vy__0 + +theorem category_inv' : + ∀ (attr : Attribute), + Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "category") = Rego.Any.str attr.category := by + unfold Rego.Any.deref + unfold rego_of_attribute + aesop + +@[simp] +theorem rego_str_eq : (Rego.Any.str s₁ == Rego.Any.str s₂) = (s₁ == s₂) := by + simp [BEq.beq, Rego.Any.instBEqAny, Rego.Any.eqv] + +@[simp] theorem const_str_neq₀ : ("category" == "identifier") = false := by rfl +@[simp] theorem const_str_neq₁ : ("category" == "value") = false := by rfl +@[simp] theorem const_str_neq₂ : ("identifier" == "value") = false := by rfl +@[simp] theorem const_str_neq₃ : ("issuer" == "value") = false := by rfl +@[simp] theorem const_str_neq₄ : ("category" == "type") = false := by rfl +@[simp] theorem const_str_neq₅ : ("identifier" == "type") = false := by rfl +@[simp] theorem const_str_neq₆ : ("kind" == "type") = false := by rfl +@[simp] theorem const_str_neq₇ : ("category" == "issuer") = false := by rfl +@[simp] theorem const_str_neq₈ : ("identifier" == "issuer") = false := by rfl +@[simp] theorem const_str_neq₉ : ("value" == "issuer") = false := by rfl +@[simp] theorem const_str_neq₁₀ : ("type" == "issuer") = false := by rfl +@[simp] theorem const_str_neq₁₁ : ("must_be_present" == "issuer") = false := by rfl + +@[simp] +theorem bool_comparison (cmp : Bool) : + ¬ (if cmp = true then Rego.Any.bool true else Rego.Any.bool false) = Rego.Any.bool false + ↔ cmp := by aesop + +@[simp] +theorem bool_comparison' (s₁ s₂ : String) : + ¬ (if s₁ = s₂ then Rego.Any.bool true else Rego.Any.bool false) = Rego.Any.bool false + ↔ s₁ = s₂ := by aesop + +theorem category_inv : + ∀ (attr : Attribute), + Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "category") = Rego.Any.str attr.category := by + intro attr + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem designator_category_inv : + ∀ (attr : AttributeDesignator), + Rego.Any.deref (rego_of_attribute_designator attr) (Rego.Any.str "category") = Rego.Any.str attr.category := by + intro attr + simp [Rego.Any.deref, rego_of_attribute_designator] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem identifier_inv : + ∀ (attr : Attribute), + Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "identifier") = Rego.Any.str attr.identifier := by + intro attr + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem designator_identifier_inv : + ∀ (attr : AttributeDesignator), + Rego.Any.deref (rego_of_attribute_designator attr) (Rego.Any.str "identifier") = Rego.Any.str attr.identifier := by + intro attr + simp [Rego.Any.deref, rego_of_attribute_designator] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem value_inv : + ∀ (attr : Attribute), + Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "value") = rego_of_primitive attr.value := by + intro attr + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem designator_type_inv : + ∀ (attr : AttributeDesignator), + Rego.Any.deref (rego_of_attribute_designator attr) (Rego.Any.str "type") = + Rego.Any.str (string_of_xmltype attr.type) := by + intro attr + simp [Rego.Any.deref, rego_of_attribute_designator] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem value_type_inv : + ∀ (attr : Attribute), + Rego.Any.deref (rego_of_primitive attr.value) (Rego.Any.str "type") = + Rego.Any.str (string_of_xmltype attr.value.fst) := by + intro attr + simp [Rego.Any.deref, rego_of_attribute_designator, rego_of_primitive] + match attr with + | { value := (type, inner), issuer := some _, .. } => + simp [Lean.AssocList.find?, Option.getD] + | { value := (type, inner), issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem issuer_none : + ∀ (attr : Attribute), + ((Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "issuer") == Rego.Any.null) = true) -> + attr.issuer = none := by + intro attr + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + simp [Lean.AssocList.find?, Option.getD] + intro h + contradiction + | { identifier := identifier, issuer := none, .. } => + simp [Lean.AssocList.find?, Option.getD] + +theorem str_str_eq : + ∀ (s₁ s₂ : String), + (Rego.Any.str s₁ == Rego.Any.str s₂) = true → s₁ = s₂ := by + intros s₁ s₂ h + have hint : (Rego.Any.str s₁ == Rego.Any.str s₂) = (s₁ == s₂) := by rfl + simp [hint] at h + exact h + +theorem attr_type_inv : + ∀ (attr : Attribute), + Rego.Any.deref (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "value")) (Rego.Any.str "type") + = Rego.Any.str (string_of_xmltype attr.value.fst) := by + intro attr + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, value, .. } => + simp [Lean.AssocList.find?, Option.getD] + unfold rego_of_primitive + match value with + | (fst, snd) => simp [Lean.AssocList.find?] + | { issuer := none, value, .. } => + simp [Lean.AssocList.find?, Option.getD] + unfold rego_of_primitive + match value with + | (fst, snd) => simp [Lean.AssocList.find?] + +theorem issuer_inv_eq : + ∀ (attr : Attribute) (desg : AttributeDesignator), + (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "issuer") == + Rego.Any.deref (rego_of_attribute_designator desg) (Rego.Any.str "issuer")) = true + → attr.issuer = desg.issuer := by + intros attr desg + simp [Rego.Any.deref, rego_of_attribute, rego_of_attribute_designator] + match attr with + | { issuer := some issuer, .. } => + match desg with + | { issuer := some issuer', .. } => + simp [Option.getD, Lean.AssocList.find?] + | { issuer := none, .. } => + intro h + contradiction + | { issuer := none, .. } => + match desg with + | { issuer := some issuer', .. } => + intro h + contradiction + | { issuer := none, .. } => + simp [Option.getD, Lean.AssocList.find?] + +theorem issuer_inv_eq' : + ∀ (attr : Attribute) (desg : AttributeDesignator), + attr.issuer = desg.issuer → + (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "issuer") == + Rego.Any.deref (rego_of_attribute_designator desg) (Rego.Any.str "issuer")) = true := by + intros attr desg + simp [Rego.Any.deref, rego_of_attribute, rego_of_attribute_designator] + match attr with + | { issuer := some issuer, .. } => + match desg with + | { issuer := some issuer', .. } => + simp [Option.getD, Lean.AssocList.find?] + | { issuer := none, .. } => + intro h + contradiction + | { issuer := none, .. } => + match desg with + | { issuer := some issuer', .. } => + intro h + contradiction + | { issuer := none, .. } => + simp [Option.getD, Lean.AssocList.find?] + +theorem string_of_xmltype_inj : + ∀ (t₁ t₂ : XmlType), + (string_of_xmltype t₁) = (string_of_xmltype t₂) → t₁ = t₂ := by + intros t₁ t₂ + cases t₁ <;> { cases t₂ <;> simp [string_of_xmltype] } + +theorem string_of_xmltype_functional : + ∀ (t₁ t₂ : XmlType), + t₁ = t₂ → (string_of_xmltype t₁) = (string_of_xmltype t₂) := by + intros t₁ t₂ + cases t₁ <;> { cases t₂ <;> simp [string_of_xmltype] } + +theorem inv_issuer (issuer : String) : + attr.issuer = some issuer → + (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "issuer") == + Rego.Any.str issuer) = true := by + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + simp [Option.getD, Lean.AssocList.find?] + | { issuer := none, .. } => + intro h + contradiction + +theorem inv_issuer_none : + attr.issuer = none → + (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "issuer") == + Rego.Any.null) = true := by + intro h + simp [Rego.Any.deref, rego_of_attribute] + match attr with + | { issuer := some issuer, .. } => + contradiction + | { issuer := none, .. } => + simp [Option.getD, Lean.AssocList.find?] + +-- theorem inv_value_type : +-- attr.value.fst = designator.type → +-- (Rego.Any.deref (Rego.Any.deref (rego_of_attribute attr) (Rego.Any.str "value")) (Rego.Any.str "type") == +-- Rego.Any.deref (rego_of_attribute_designator designator) (Rego.Any.str "type")) = +-- true := by +-- intro h +-- simp [Rego.Any.deref, rego_of_attribute] +-- match attr with +-- | { issuer := some issuer, .. } => +-- simp [Option.getD, Lean.AssocList.find?] +-- sorry +-- | { issuer := none, .. } => +-- simp [Option.getD, Lean.AssocList.find?] +-- sorry + +theorem designator_matches_correct : + ∀ (designator : AttributeDesignator) (attr : Attribute), + designator_matches + (rego_of_attribute_designator designator) + (rego_of_attribute attr) + (Rego.Any.bool true) + ↔ + attribute_matches designator attr := by + intros designator attr + rw [iff_iff_implies_and_implies] + apply And.intro + { intro h + cases h with + | rule0 h => + let h₂ := h.right.left + let h₃ := h.right.right.left + let h₄ := h.right.right.right.left + let h₅ := h.right.right.right.right + + unfold attribute_matches + simp [eq, equal, Rego.Any.deref] + + apply And.intro + { simp [category_inv, designator_category_inv, equal] at h₅ + exact h₅ } + { apply And.intro + { simp [identifier_inv, designator_identifier_inv, equal] at h₄ + exact h₄ } + { apply And.intro + { simp [equal, value_inv, designator_type_inv, value_type_inv] at h₃ + apply string_of_xmltype_inj + exact h₃ } + { apply Or.inl + apply issuer_none + simp [equal] at h₂ + exact h₂ }}} + | rule1 h => + let h₂ := h.right.left + let h₃ := h.right.right.left + let h₄ := h.right.right.right.left + let h₅ := h.right.right.right.right + + unfold attribute_matches + simp [eq, equal, Rego.Any.deref] + + apply And.intro + { simp [category_inv, designator_category_inv, equal] at h₅ + exact h₅ } + { apply And.intro + { simp [identifier_inv, designator_identifier_inv, equal] at h₄ + exact h₄ } + { apply And.intro + { simp [equal, value_inv, designator_type_inv, value_type_inv] at h₃ + apply string_of_xmltype_inj + exact h₃ } + { apply Or.inr + simp [equal] at h₂ + apply issuer_inv_eq + exact h₂ }}}} + { unfold attribute_matches + simp + intros hcat hident htyp hissuer + cases hissuer with + | inl hissuer => + apply designator_matches.rule0 + apply And.intro + { simp [eq] } + { apply And.intro + { simp [equal] + apply inv_issuer_none + assumption } + { apply And.intro + { simp [equal, designator_type_inv, attr_type_inv] + apply string_of_xmltype_functional + assumption } + { apply And.intro + { simp [equal, identifier_inv, designator_identifier_inv] + assumption } + { simp [equal, category_inv, designator_category_inv] + assumption }}}} + | inr hissuer => + apply designator_matches.rule1 + apply And.intro + { simp [eq] } + { apply And.intro + { simp [equal] + apply issuer_inv_eq' + assumption } + { apply And.intro + { simp [equal, designator_type_inv, attr_type_inv] + apply string_of_xmltype_functional + assumption } + { apply And.intro + { simp [equal, identifier_inv, designator_identifier_inv] + assumption } + { simp [equal, category_inv, designator_category_inv] + assumption }}}} } + + +-- def rego_error := (∀ (vargs__40 : Rego.Any), ∃! (vvalue__41 : Rego.Any), (eq (designator_matches vargs__40) vvalue__41)) + +-- #eval Rego.Any.deref (rego_of_attribute (Attribute.mk "a" "b" "c" (XmlType.boolean, "true"))) (Rego.Any.str "issuer") + +inductive q (vx__0 : Rego.Any) where + | rule0 : ∃ (vinternal__15 vsites__16 vsite__17 : Rego.Any), + (And (Ne (eq vx__0 (Rego.Any.deref vsite__17 (Rego.Any.str "name"))) (Rego.Any.bool False)) + (Ne (vsites__16.contains vsite__17) (Rego.Any.bool False))) → q vx__0 +def rego_error := (False) diff --git a/rego-proofs/Rego/lake-manifest.json b/rego-proofs/Rego/lake-manifest.json index 9b0ab31..639b42c 100644 --- a/rego-proofs/Rego/lake-manifest.json +++ b/rego-proofs/Rego/lake-manifest.json @@ -1,27 +1,52 @@ -{"version": 4, +{"version": 6, "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/aesop", "subDir?": null, - "rev": "f85368f49bea5a60679f40625f31177479d7f732", + "rev": "0654e7a1ba1542c3a24f936e52a40b3fee6c13c0", + "opts": {}, + "name": "aesop", + "inputRev?": "v4.2.0", + "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover-community/mathlib4", + "subDir?": null, + "rev": "753159252c585df6b6aa7c48d2b8828d58388b79", + "opts": {}, "name": "mathlib", - "inputRev?": null}}, + "inputRev?": "v4.2.0", + "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "409a644492aaff846b6b2963e221c7f1ceaf30cc", + "opts": {}, + "name": "std", + "inputRev?": "v4.2.0", + "inherited": true}}, {"git": - {"url": "https://github.com/gebner/quote4", + {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, - "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", + "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", + "opts": {}, "name": "Qq", - "inputRev?": "master"}}, + "inputRev?": "master", + "inherited": true}}, {"git": - {"url": "https://github.com/JLimperg/aesop", + {"url": "https://github.com/leanprover/lean4-cli", "subDir?": null, - "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", - "name": "aesop", - "inputRev?": "master"}}, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "opts": {}, + "name": "Cli", + "inputRev?": "nightly", + "inherited": true}}, {"git": - {"url": "https://github.com/leanprover/std4", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "subDir?": null, - "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", - "name": "std", - "inputRev?": "main"}}]} + "rev": "f1a5c7808b001305ba07d8626f45ee054282f589", + "opts": {}, + "name": "proofwidgets", + "inputRev?": "v0.0.21", + "inherited": true}}], + "name": "rego"} diff --git a/rego-proofs/Rego/lakefile.lean b/rego-proofs/Rego/lakefile.lean index acc69c1..9163884 100644 --- a/rego-proofs/Rego/lakefile.lean +++ b/rego-proofs/Rego/lakefile.lean @@ -1,14 +1,10 @@ import Lake open Lake DSL -package «rego» { - -- add any package configuration options here -} - -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" +package rego @[default_target] -lean_lib «Rego» { - -- add any library configuration options here -} +lean_lib Rego + +require aesop from git "https://github.com/leanprover-community/aesop"@"v4.2.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4"@"v4.2.0" diff --git a/rego-proofs/Rego/lean-toolchain b/rego-proofs/Rego/lean-toolchain new file mode 100644 index 0000000..2f868c6 --- /dev/null +++ b/rego-proofs/Rego/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.2.0 diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 03f37d0..3b0384a 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -10,7 +10,6 @@ type definition_kind = Complete | FunctionRule [@@deriving eq, show] - let fold_or props = match List.reduce props ~f:(fun x y -> Application (Identifier "Or", [y; x])) with | Some x -> x @@ -21,6 +20,9 @@ let fold_and props = | Some x -> x | None -> Bool false +let fold_deref terms = + List.reduce_exn terms ~f:(fun x y -> Application (Identifier "Rego.Any.deref", [x; y])) + let kind_and_args_of_rule = function | { head = ((_, []), Assignment (_, term)); _ } -> `ScalarRule term @@ -259,7 +261,7 @@ let rec compile_term env : term -> lean_expression = let terms' = List.map ~f:(compile_term env) terms in if List.is_empty terms' then target' - else Application (Identifier "Rego.Any.deref", [target'] @ terms') + else [target'] @ terms' |> fold_deref | Array xs -> let xs' = List.map ~f:(compile_term env) xs in Application (Identifier "Rego.Any.array", xs') |