From 420b4ccaabead7d3a977c4b08393f345c8be6794 Mon Sep 17 00:00:00 2001 From: Craig Disselkoen Date: Wed, 20 Nov 2024 10:29:52 -0800 Subject: [PATCH] add Lean protobuf library (#478) Signed-off-by: Craig Disselkoen --- cedar-lean/Protobuf.lean | 27 ++++ cedar-lean/Protobuf/BParsec.lean | 163 +++++++++++++++++++ cedar-lean/Protobuf/ByteArray.lean | 57 +++++++ cedar-lean/Protobuf/Enum.lean | 45 ++++++ cedar-lean/Protobuf/Field.lean | 72 +++++++++ cedar-lean/Protobuf/Map.lean | 103 ++++++++++++ cedar-lean/Protobuf/Message.lean | 99 ++++++++++++ cedar-lean/Protobuf/Packed.lean | 97 ++++++++++++ cedar-lean/Protobuf/Proofs.lean | 238 ++++++++++++++++++++++++++++ cedar-lean/Protobuf/String.lean | 103 ++++++++++++ cedar-lean/Protobuf/Structures.lean | 103 ++++++++++++ cedar-lean/Protobuf/Varint.lean | 170 ++++++++++++++++++++ cedar-lean/Protobuf/WireType.lean | 32 ++++ cedar-lean/UnitTest/Proto.lean | 106 +++++++++++++ cedar-lean/lakefile.lean | 3 + 15 files changed, 1418 insertions(+) create mode 100644 cedar-lean/Protobuf.lean create mode 100644 cedar-lean/Protobuf/BParsec.lean create mode 100644 cedar-lean/Protobuf/ByteArray.lean create mode 100644 cedar-lean/Protobuf/Enum.lean create mode 100644 cedar-lean/Protobuf/Field.lean create mode 100644 cedar-lean/Protobuf/Map.lean create mode 100644 cedar-lean/Protobuf/Message.lean create mode 100644 cedar-lean/Protobuf/Packed.lean create mode 100644 cedar-lean/Protobuf/Proofs.lean create mode 100644 cedar-lean/Protobuf/String.lean create mode 100644 cedar-lean/Protobuf/Structures.lean create mode 100644 cedar-lean/Protobuf/Varint.lean create mode 100644 cedar-lean/Protobuf/WireType.lean create mode 100644 cedar-lean/UnitTest/Proto.lean diff --git a/cedar-lean/Protobuf.lean b/cedar-lean/Protobuf.lean new file mode 100644 index 000000000..3ffc0966d --- /dev/null +++ b/cedar-lean/Protobuf.lean @@ -0,0 +1,27 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.ByteArray +import Protobuf.Enum +import Protobuf.Map +import Protobuf.Message +import Protobuf.Packed +import Protobuf.Proofs +import Protobuf.String +import Protobuf.Structures +import Protobuf.Varint +import Protobuf.WireType diff --git a/cedar-lean/Protobuf/BParsec.lean b/cedar-lean/Protobuf/BParsec.lean new file mode 100644 index 000000000..30e09bab5 --- /dev/null +++ b/cedar-lean/Protobuf/BParsec.lean @@ -0,0 +1,163 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.ByteArray + +/-! +Monadic Parser Combinator for ByteArrays +-/ + +namespace BParsec +inductive ParseResult (α : Type) where + | success (pos : ByteArray.ByteIterator) (res : α) + | error (pos : ByteArray.ByteIterator) (err : String) + deriving Repr +end BParsec + +def BParsec (α : Type) : Type := ByteArray.ByteIterator → BParsec.ParseResult α + +namespace BParsec + +instance (α : Type) : Inhabited (BParsec α) := ⟨λ it => .error it ""⟩ + +@[inline] +def map {α β : Type} (g : α → β) (f : BParsec α) : BParsec β := λ it => + match f it with + | .success it a => .success it (g a) + | .error it msg => .error it msg + +@[inline] +def mapConst {α β : Type} (x : α) (f : BParsec β) : BParsec α := λ it => + match f it with + | .success it _ => .success it x + | .error it msg => .error it msg + +instance : Functor BParsec := { map, mapConst } + +@[inline] +def pure (a : α) : BParsec α := λ it => .success it a + +@[inline] +def bind {α β : Type} (f : BParsec α) (g : α → BParsec β) : BParsec β := λ it => + match f it with + | .success it a => g a it + | .error it msg => .error it msg + +instance : Monad BParsec := { pure := BParsec.pure, bind } + +@[inline] +def fail (msg : String) : BParsec α := fun it => .error it msg + +@[inline] +def tryCatch (body : BParsec α) (handler : String → BParsec α) : BParsec α := fun it => + match body it with + | .success it result => .success it result + | .error it err => (handler err) it + +@[inline] +def orElse (p : BParsec α) (q : Unit → BParsec α) : BParsec α := fun it => + match p it with + | .success it result => .success it result + | .error it _ => q () it + +/-- Attempt a parser combinator on a byte array, if it fails, reset +the position-/ +@[inline] +def attempt (p : BParsec α) : BParsec α := λ it => + match p it with + | .success rem res => .success rem res + | .error _ err => .error it err + +instance : Alternative BParsec := { failure := fail default, orElse } + +instance : MonadExceptOf String BParsec := { + throw := fail, tryCatch := tryCatch +} + +/- Execute parser combinators on a byte array, +returns an Except to capture both successes and failures -/ +@[inline] +def run (p : BParsec α) (ba : ByteArray) : Except String α := + match p ba.byte_iter with + | .success _ res => .ok res + | .error it err => .error s!"offset {it.pos}: {err}" + +/- Execute parser combinators on a byte array, panics on error -/ +@[inline] +def run! [Inhabited α] (p : BParsec α) (ba : ByteArray) : α := + match p ba.byte_iter with + | .success _ res => res + | .error _ _ => panic!("Unexpected error") + +-- Iterator wrappers + +@[inline] +def hasNext : BParsec Bool := + fun it => .success it it.hasNext + +@[inline] +def next : BParsec Unit := + fun it => .success (it.next) () + +@[inline] +def forward (n : Nat) : BParsec Unit := + fun it => .success (it.forward n) () + +@[inline] +def size : BParsec Nat := + fun it => .success it it.size + +@[inline] +def remaining : BParsec Nat := + fun it => .success it it.remaining + +@[inline] +def empty : BParsec Bool := + fun it => .success it it.empty + +@[inline] +def pos : BParsec Nat := + fun it => .success it it.pos + +@[specialize] def foldlHelper {α β : Type} (f : BParsec α) (g : β → α → β) (remaining : Nat) (result : β) : BParsec β := do + if remaining = 0 then + pure result + else + + let startPos ← pos + let element ← f + let endPos ← pos + + let elementSize := endPos - startPos + if elementSize = 0 then + throw "f did not progress ByteArray" + else + + let newResult := g result element + foldlHelper f g (remaining - elementSize) newResult + +@[inline] +def foldl {α β : Type} (f : BParsec α) (g : β → α → β) (remaining : Nat) (init : β) : BParsec β := + foldlHelper f g remaining init + +@[inline] +def eof : BParsec Unit := fun it => + if it.pos ≥ it.data.size then + .success it () + else + .error it "Expected end of file" + +end BParsec diff --git a/cedar-lean/Protobuf/ByteArray.lean b/cedar-lean/Protobuf/ByteArray.lean new file mode 100644 index 000000000..2abc483bb --- /dev/null +++ b/cedar-lean/Protobuf/ByteArray.lean @@ -0,0 +1,57 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +/-! +Iterators for ByteArrays +-/ + +namespace ByteArray + +deriving instance Repr, DecidableEq, Inhabited for ByteArray + +-- note that ByteArray.Iterator and ByteArray.iter are provided by Lean, +-- but the interfaces are more limited than those we provide in this file. + +structure ByteIterator where + data : ByteArray + /-- The current position.--/ + pos : Nat + deriving DecidableEq, Repr, Inhabited + +/-- Creates an iterator at the beginning of a ByteArray. -/ +@[inline] +def byte_iter (b : ByteArray) : ByteIterator := ⟨b, 0⟩ + +@[inline] +def ByteIterator.next (i : ByteIterator) : ByteIterator := ⟨i.data, i.pos + 1⟩ + +@[inline] +def ByteIterator.forward (i : ByteIterator) (n : Nat) : ByteIterator := ⟨i.data, i.pos + n⟩ + +@[inline] +def ByteIterator.size (i : ByteIterator) : Nat := i.data.size + +@[inline] +def ByteIterator.remaining (i : ByteIterator) : Nat := i.size - i.pos + +/-- True if there are more bytes passed the current position. -/ +@[inline] +def ByteIterator.hasNext (i : ByteIterator) : Bool := i.remaining != 0 + +@[inline] +def ByteIterator.empty (i : ByteIterator) : Bool := ¬i.hasNext + +end ByteArray diff --git a/cedar-lean/Protobuf/Enum.lean b/cedar-lean/Protobuf/Enum.lean new file mode 100644 index 000000000..a5f345310 --- /dev/null +++ b/cedar-lean/Protobuf/Enum.lean @@ -0,0 +1,45 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Field +import Protobuf.Varint + +/-! +Protobuf enums and their parsers +-/ + +namespace Proto + +class ProtoEnum (α : Type) where + fromInt : Int → Except String α +export ProtoEnum (fromInt) + +@[inline] +def parseEnum (α : Type) [ProtoEnum α] : BParsec α := do + let wdata : Int ← parse_int32 + let result : Except String α := fromInt wdata + match result with + | Except.ok r => pure r + | Except.error e => throw e + +instance [ProtoEnum α] : Field α := { + parse := (parseEnum α) + checkWireType := fun w => WireType.VARINT = w + merge := Field.Merge.override +} + +end Proto diff --git a/cedar-lean/Protobuf/Field.lean b/cedar-lean/Protobuf/Field.lean new file mode 100644 index 000000000..e6f70ca97 --- /dev/null +++ b/cedar-lean/Protobuf/Field.lean @@ -0,0 +1,72 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.WireType + +/-! +Protobuf fields and their parsers +-/ + +namespace Proto + +class Field (α : Type) where + parse : BParsec α + checkWireType : WireType → Bool + merge : α → α → α + +namespace Field + + +namespace Merge + +/-- Models override semantics, replaces the former value with the latter -/ +@[inline] +def override (_ : α) (x : α) : α := x + +/-- Concatenation semantics, combines two arrays -/ +@[inline] +def concatenate (x1 : Array α) (x2 : Array α) : Array α := + x1.append x2 + +end Merge + +@[inline] +def interpret! {α : Type} [Field α] [Inhabited α] (b : ByteArray) : α := + BParsec.run! Field.parse b + +@[inline] +def interpret? {α : Type} [Field α] [Inhabited α] (b : ByteArray) : Except String α := + BParsec.run Field.parse b + +@[inline] +def guardWireType {α : Type} [Field α] (wt : WireType) : BParsec Unit := do + let wtMatches := (@Field.checkWireType α) wt + if not wtMatches then + throw s!"WireType mismatch" + +@[inline] +def fromInterField {α β : Type} [Inhabited α] [Field α] (convert : α → β) (merge : β → β → β) : Field β := { + parse := do + let intMessage : α ← Field.parse + pure (convert intMessage) + checkWireType := Field.checkWireType α + merge := merge +} + +end Field + +end Proto diff --git a/cedar-lean/Protobuf/Map.lean b/cedar-lean/Protobuf/Map.lean new file mode 100644 index 000000000..1df83c059 --- /dev/null +++ b/cedar-lean/Protobuf/Map.lean @@ -0,0 +1,103 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Field +import Protobuf.Structures + +/-! +Parsers for Map Fields +-/ + +namespace Proto + +def Map (KeyT ValueT : Type) [Field KeyT] [Field ValueT] := Array (KeyT × ValueT) + +namespace Map + +instance {α β : Type} [Field α] [Field β] : Inhabited (Map α β) where + default := #[] + +@[inline] +def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BParsec (Map KeyT ValueT) := do + let len_size ← Len.parseSize + let startPos ← BParsec.pos + + let tag1 ← Tag.parse + let result ← match tag1.fieldNum with + | 1 => + let wt1Matches := (@Field.checkWireType KeyT) tag1.wireType + if not wt1Matches then + throw s!"WireType mismatch" + else + let key : KeyT ← Field.parse + + -- Since the fields are optional, check to see if we're done parsing now + let curPos ← BParsec.pos + if curPos - startPos == len_size then + pure #[(Prod.mk key (default : ValueT))] + else + + let tag2 ← Tag.parse + let wt2Matches := (@Field.checkWireType ValueT) tag2.wireType + if not wt2Matches then + throw s!"WireType mismatch" + else + if tag2.fieldNum != 2 then + throw s!"Expected Field Number 2 within map, not {tag2.fieldNum}" + else + let value : ValueT ← Field.parse + pure #[(Prod.mk key value)] + | 2 => + let wt1Matches := (@Field.checkWireType ValueT) tag1.wireType + if not wt1Matches then + throw s!"WireType mismatch" + else + let value : ValueT ← Field.parse + + -- Since the fields are optional, check to see if we're done parsing now + let curPos ← BParsec.pos + if curPos - startPos == len_size then + pure #[(Prod.mk (default : KeyT) value)] + else + + let tag2 ← Tag.parse + let wt2Matches := (@Field.checkWireType KeyT) tag2.wireType + if not wt2Matches then + throw s!"WireType mismatch" + else + if tag2.fieldNum != 1 then + throw s!"Expected Field Number 1 within map, not {tag2.fieldNum}" + else + let key : KeyT ← Field.parse + pure #[(Prod.mk key value)] + + | _ => throw "Unexpected Field Number within Map Element" + + let endPos ← BParsec.pos + + if endPos - startPos != len_size then + throw s!"[Map parse] LEN size invariant not maintained: expected {len_size}, parsed {endPos - startPos}" + + pure result + +instance {α β : Type} [Inhabited α] [Inhabited β] [Field α] [Field β] : Field (Map α β) := { + parse := parse + checkWireType := fun (w : WireType) => WireType.LEN = w + merge := Field.Merge.concatenate +} +end Map +end Proto diff --git a/cedar-lean/Protobuf/Message.lean b/cedar-lean/Protobuf/Message.lean new file mode 100644 index 000000000..9ef947776 --- /dev/null +++ b/cedar-lean/Protobuf/Message.lean @@ -0,0 +1,99 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Structures +import Protobuf.Packed +import Protobuf.WireType + +/-! +Protobuf Message class +-/ + +namespace Proto + +def MergeFn (α : Type) : Type := (α → α) + +class Message (α : Type) [Inhabited α] where + parseField : Tag → BParsec (MergeFn α) + merge : α → α → α + +export Message (parseField) +namespace Message + +private def parseMessageHelper [Inhabited α] [Message α] (remaining : Nat) (result : α) : BParsec α := do + if remaining = 0 then + pure result + else + + let empty ← BParsec.empty + if empty then + throw "Expected more bytes" + else + + let startPos ← BParsec.pos + + let tag ← Tag.parse + + let f : MergeFn α ← parseField tag + + let endPos ← BParsec.pos + + let newResult := f result + let elementSize := (endPos - startPos) + if elementSize = 0 then + throw "[parseMessageHelper] f did not progress ByteArray" + else + + (parseMessageHelper (remaining - elementSize) newResult) + + + +@[inline] +def parse [Inhabited α] [Message α] : BParsec α := do + let remaining ← BParsec.remaining + let message : α ← parseMessageHelper remaining default + BParsec.eof + pure message + +@[inline] +def parseWithLen [Inhabited α] [Message α] : BParsec α := do + let len_size ← Len.parseSize + let message : α ← parseMessageHelper len_size default + pure message + +@[inline] +def parseWithSize [Inhabited α] [Message α] (size : Nat) : BParsec α := do + let message : α ← parseMessageHelper size default + pure message + +@[inline] +def interpret? [Inhabited α] [Message α] (b : ByteArray) : Except String α := + BParsec.run parse b + +@[inline] +def interpret! [Inhabited α] [Message α] (b : ByteArray) : α := + BParsec.run! parse b + +instance [Inhabited α] [Message α] : Field α := { + parse := parseWithLen + checkWireType := fun (w : WireType) => WireType.LEN = w + merge := merge +} + +end Message + +end Proto diff --git a/cedar-lean/Protobuf/Packed.lean b/cedar-lean/Protobuf/Packed.lean new file mode 100644 index 000000000..fde08ab8d --- /dev/null +++ b/cedar-lean/Protobuf/Packed.lean @@ -0,0 +1,97 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Field +import Protobuf.Structures +import Protobuf.WireType + +/-! +Parsers for Repeated Fields +-/ + +namespace Proto + +/-- Repeated fields are assumed to come one record at a time -/ +def Repeated (α : Type) [Field α] : Type := Array α + +namespace Repeated + +instance [Field α] : Inhabited (Repeated α) where + default := #[] + +instance [DecidableEq α] [Field α] : DecidableEq (Repeated α) := by + unfold DecidableEq + unfold Repeated + intro a b + apply inferInstance + +instance [Repr α] [Field α] : Repr (Repeated α) := by + unfold Repeated + apply inferInstance + +/-- Parses one value from a record -/ +@[inline] +def parse (α : Type) [Field α] : BParsec (Array α) := do + let element ← Field.parse + pure #[element] + +instance [Field α] : Field (Repeated α) := { + parse := (parse α) + checkWireType := Field.checkWireType α + merge := Field.Merge.concatenate +} + +end Repeated + +/-- An array of elements that are contained sequentially within + a single LEN wire type -/ +def Packed (α : Type) [Field α] : Type := Array α + +namespace Packed + +instance [Field α] : Inhabited (Packed α) where + default := #[] + +instance [DecidableEq α] [Field α] : DecidableEq (Packed α) := by + unfold DecidableEq + unfold Packed + intro a b + apply inferInstance + +instance [Repr α] [Field α] : Repr (Packed α) := by + unfold Packed + apply inferInstance + +@[inline] +def parse (α : Type) [Field α] : BParsec (Array α) := do + let len_size ← Len.parseSize + BParsec.foldl + Field.parse + (fun arr => fun element => arr.push element) + len_size + #[] + +instance [Field α] : Field (Packed α) := { + parse := (parse α) + checkWireType := fun (w : WireType) => WireType.LEN = w + merge := Field.Merge.concatenate +} + +end Packed + + +end Proto diff --git a/cedar-lean/Protobuf/Proofs.lean b/cedar-lean/Protobuf/Proofs.lean new file mode 100644 index 000000000..0545f837b --- /dev/null +++ b/cedar-lean/Protobuf/Proofs.lean @@ -0,0 +1,238 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.ByteArray +import Protobuf.BParsec +import Protobuf.String + +/-! +Theorems about protobuf parsing and its helper functions +-/ + +namespace ByteArray.ByteIterator + +@[simp] theorem next_pos_eq (i : ByteIterator) : i.next.pos = i.pos + 1 := rfl +@[simp] theorem next_data_eq (i : ByteIterator) : i.next.data = i.data := rfl +@[simp] theorem next_size_eq (i : ByteIterator) : i.next.size = i.size := rfl +attribute [simp] remaining + +theorem next_le_remaining (i : ByteIterator) : i.next.remaining ≤ i.remaining := by + simp only [remaining, next_size_eq, next_pos_eq] + omega + +@[simp] theorem hasNext_iff (i : ByteIterator) : i.hasNext ↔ i.remaining != 0 := by + simp only [hasNext, remaining, bne_iff_ne, ne_eq] + +@[simp] theorem not_hasNext_iff (i : ByteIterator) : ¬i.hasNext ↔ i.remaining = 0 := by + simp only [hasNext, remaining, bne_iff_ne, ne_eq, Decidable.not_not] + +@[simp] theorem empty_iff (i : ByteIterator) : i.empty ↔ ¬i.hasNext := by + simp only [empty, hasNext_iff, remaining, bne_iff_ne, ne_eq, Decidable.not_not, decide_eq_true_eq] + +@[simp] theorem not_empty_iff (i : ByteIterator) : ¬i.empty ↔ i.hasNext := by + simp only [empty_iff, hasNext_iff, remaining, bne_iff_ne, ne_eq, Decidable.not_not] + +end ByteArray.ByteIterator + +namespace BParsec + +instance [DecidableEq α] : DecidableEq (ParseResult α) := by + unfold DecidableEq + intro a b + cases a <;> cases b <;> simp only [reduceCtorEq, ParseResult.success.injEq, ParseResult.error.injEq] + case error.success | success.error => exact isFalse (by simp only [not_false_eq_true]) + case error.error c d e f | success.success c d e f => + match (decEq c e), (decEq d f) with + | isTrue h1, isTrue h2 => subst e f ; exact isTrue (by simp only [and_self]) + | _, isFalse h2 => exact isFalse (by intro h; simp [h] at h2) + | isFalse h1, _ => exact isFalse (by intro h; simp [h] at h1) + +attribute [simp] map +attribute [simp] mapConst + +theorem ext (x y : BParsec α) (H : ∀ it, x it = y it) : x = y := funext H + +@[simp] theorem id_map (x : BParsec α) : id <$> x = x := by + apply ext + intro it + simp only [Functor.map, map, id_eq] + split <;> simp only [*] + +theorem map_const : (@mapConst α β) = ((@map β α) ∘ (@Function.const α β)) := rfl + +theorem comp_map (g : α → β) (h : β → γ) (x : BParsec α) : (h ∘ g) <$> x = h <$> g <$> x := by + apply ext + intro it + simp only [Functor.map, map, Function.comp_apply] + split <;> simp only [*] + +instance : LawfulFunctor BParsec := { + map_const := map_const, + id_map := id_map, + comp_map := comp_map +} + +attribute [simp] pure +attribute [simp] bind + +instance : LawfulMonad BParsec := { + map_const, id_map, + seqLeft_eq := by + intro α β f1 f2 + apply ext + intro it + simp only [Monad.toApplicative, instMonad, instFunctor, Functor.map, bind, pure, map] + split <;> simp only [Function.const_apply] + + seqRight_eq := by + intro α β x y + apply ext + intro it + simp only [SeqRight.seqRight, bind, Seq.seq, Functor.map, map, Function.const] + split <;> simp only [id_eq] + split <;> simp only [*] + + pure_seq := by + intro α β g x + apply ext + intro it + simp only [Seq.seq, bind, Pure.pure, pure, Monad.toApplicative, instMonad] + + bind_pure_comp := by + intro α β f x + simp only [Bind.bind, Pure.pure, Functor.map] + rfl + + bind_map := by + intro α β f x + simp only [Bind.bind, Functor.map, Seq.seq] + + pure_bind := by + intro α β x f + simp only [Bind.bind, Pure.pure] + rfl + + bind_assoc := by + intro α β γ x f g + simp only [Bind.bind] + apply ext + intro it + simp only [bind] + cases x it <;> simp only +} + +attribute [simp] hasNext +attribute [simp] next +attribute [simp] forward +attribute [simp] size +attribute [simp] remaining +attribute [simp] empty +attribute [simp] pos + +theorem foldl_iterator_progress {f : BParsec α} {g : β → α → β} {remaining : Nat} {init : β} {result : β} (H1 : remaining > 0) (H : (foldl f g remaining init) it1 = .success it2 result) : it2.pos > it1.pos := by + unfold foldl at H + revert (H1 : remaining > 0) + induction remaining using Nat.strongRecOn generalizing f g init result it1 it2 + next ni IH => + intro (H1 : ni > 0) + unfold foldlHelper at H + have H2 : ¬(ni = 0) := by omega + rw [if_neg H2] at H + simp only [Bind.bind, bind, pos] at H + cases H3 : f it1 <;> simp only [H3, reduceCtorEq] at H + case success itn resultn => + by_cases H4 : (itn.pos - it1.pos = 0) + case pos => simp only [H4, reduceIte] at H ; contradiction + case neg => + simp only [H4, reduceIte] at H + let ni2 := ni - (itn.pos - it1.pos) + have Hni2 : ni2 = ni - (itn.pos - it1.pos) := rfl + rw [← Hni2] at H + by_cases H6 : (itn.pos - it1.pos ≥ ni) + case neg => + specialize @IH ni2 (by omega) itn it2 f g (g init resultn) result H (by omega) + omega + case pos => + have Hn : ni2 = 0 := by omega + simp only [Hn] at H + unfold foldlHelper at H + rw [if_pos (by decide)] at H + simp only [pure, ParseResult.success.injEq] at H + replace ⟨H, _⟩ := H + subst it2 + omega + +end BParsec + +namespace Proto + +instance : DecidableEq (BParsec.ParseResult (Char × Nat)) := by apply inferInstance + +theorem utf8DecodeChar.sizeGt0 (it1 it2 : ByteArray.ByteIterator) (pos : Nat) (c : Char) (H : utf8DecodeChar pos it1 = .success it2 ⟨c, n⟩) : n > 0 := by + unfold utf8DecodeChar at H + simp only [beq_iff_eq, bne_iff_ne, ne_eq, gt_iff_lt, ite_not, Bool.and_eq_true, not_and, + and_imp] at H + split at H + · simp only [BParsec.ParseResult.success.injEq, Prod.mk.injEq, true_and] at H + omega + · split at H + · split at H + · split at H + · simp only [reduceCtorEq] at H + · split at H + · simp only [BParsec.ParseResult.success.injEq, Prod.mk.injEq, true_and] at H + omega + · simp only [reduceCtorEq] at H + · simp only [reduceCtorEq] at H + · split at H + · split at H + · simp only [reduceCtorEq] at H + · split at H + · simp only [reduceCtorEq] at H + · split at H + · simp only [BParsec.ParseResult.success.injEq, Prod.mk.injEq, true_and] at H + omega + · simp only [reduceCtorEq] at H + · split at H + · split at H + · simp only [reduceCtorEq] at H + · split at H + · simp only [BParsec.ParseResult.success.injEq, Prod.mk.injEq, true_and] at H + omega + · simp only [reduceCtorEq] at H + · simp only [reduceCtorEq] at H + +private def parseStringHelper_unoptimized (remaining : Nat) (r : String) : BParsec String := do + if remaining = 0 then pure r else + let empty ← BParsec.empty + if empty then throw s!"Expected more packed uints, Size Remaining: {remaining}" else + let pos ← BParsec.pos + fun it => + let result := utf8DecodeChar pos it + match result with + | .success it2 ⟨c, elementSize⟩ => + -- NOTE: I don't know how to get H_Redunant other than + -- doing this. Which is bad for runtime O(n) of ByteArray + if H_Redundant : result = .success it2 ⟨c, elementSize⟩ then + have _ : elementSize > 0 := utf8DecodeChar.sizeGt0 it it2 pos c H_Redundant + (do + BParsec.forward (elementSize) + parseStringHelper_unoptimized (remaining - elementSize) (r.push c)) it + else + .error it2 "Impossible case" + | .error it msg => .error it msg + +end Proto diff --git a/cedar-lean/Protobuf/String.lean b/cedar-lean/Protobuf/String.lean new file mode 100644 index 000000000..07817e676 --- /dev/null +++ b/cedar-lean/Protobuf/String.lean @@ -0,0 +1,103 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Field +import Protobuf.Structures +import Protobuf.WireType + +/-! +Decode UTF-8 encoded strings with ByteArray Parser Combinators +-/ + +namespace Proto + +-- NOTE: Will panic if there's not enough bytes to determine the next character +-- NOTE: Does not progress iterator +-- Returns the size of the character as well +@[inline] +def utf8DecodeChar (i : Nat) : BParsec (Char × Nat) := fun it => + let c := it.data[i]! + if c &&& 0x80 == 0 then + have char := ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩ + .success it ⟨char, 1⟩ + else if c &&& 0xe0 == 0xc0 then + let c1 := it.data[i+1]! + if c1 &&& 0xc0 != 0x80 then .error it "Not a valid UTF8 Char" else + let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32 + if 0x80 > r then .error it "Not a valid UTF8 Char" else + if h : r < 0xd800 then + have char := ⟨r, .inl h⟩ + .success it ⟨char, 2⟩ + else .error it s!"Not valid UTF8 Char: {c} {c1}" + else if c &&& 0xf0 == 0xe0 then + let c1 := it.data[i+1]! + let c2 := it.data[i+2]! + if ¬(c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80) then + .error it "Not a valid UTF8 Char" + else + let r := + ((c &&& 0x0f).toUInt32 <<< 12) ||| + ((c1 &&& 0x3f).toUInt32 <<< 6) ||| + (c2 &&& 0x3f).toUInt32 + if (0x800 > r) then .error it "Not a valid UTF8 Char" else + if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then + have char := ⟨r, h⟩ + .success it ⟨char, 3⟩ + else .error it s!"Not valid UTF8 Char: {c} {c1} {c2}" + else if c &&& 0xf8 == 0xf0 then + let c1 := it.data[i+1]! + let c2 := it.data[i+2]! + let c3 := it.data[i+3]! + if ¬(c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80 && c3 &&& 0xc0 == 0x80) then + .error it "Not a valid UTF8 Char" + else + let r := + ((c &&& 0x07).toUInt32 <<< 18) ||| + ((c1 &&& 0x3f).toUInt32 <<< 12) ||| + ((c2 &&& 0x3f).toUInt32 <<< 6) ||| + (c3 &&& 0x3f).toUInt32 + if h : 0x10000 ≤ r ∧ r < 0x110000 then + have char := ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩ + .success it ⟨ char, 4 ⟩ + else .error it s!"Not valid UTF8 Char: {c} {c1} {c2} {c3}" + else + .error it s!"Not valid UTF8 Char: {c}" + + +-- Progresses ByteArray.Iterator +-- Assumes UTF8 encoding +private partial def parseStringHelper (remaining : Nat) (r : String) : BParsec String := do + if remaining = 0 then pure r else + let empty ← BParsec.empty + if empty then throw s!"Expected more packed uints, Size Remaining: {remaining}" else + let pos ← BParsec.pos + let ⟨c, elementSize⟩ ← utf8DecodeChar pos + BParsec.forward (elementSize) + parseStringHelper (remaining - elementSize) (r.push c) + +@[inline] +def parse_string : BParsec String := do + let len_size ← Len.parseSize + parseStringHelper len_size "" + +instance : Field String := { + parse := parse_string + checkWireType := fun (w : WireType) => WireType.LEN = w + merge := Field.Merge.override +} + +end Proto diff --git a/cedar-lean/Protobuf/Structures.lean b/cedar-lean/Protobuf/Structures.lean new file mode 100644 index 000000000..9456c96a7 --- /dev/null +++ b/cedar-lean/Protobuf/Structures.lean @@ -0,0 +1,103 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Lean.Data.HashMap +import Protobuf.BParsec +import Protobuf.Varint +import Protobuf.WireType + +/-! +Various Protobuf Structures, likely will reorganize later +-/ + +namespace Proto + +structure MessageSchema where + schema : Std.HashMap Nat PType + +structure Tag where + fieldNum : Nat + wireType : WireType +deriving Repr, DecidableEq, Inhabited + +structure Len where + size : Nat +deriving Repr + +namespace VarInt + @[inline] + def skip : BParsec Unit := do + let size ← find_varint_size + BParsec.forward size +end VarInt + +namespace Len + @[inline] + def parseSize : BParsec Nat := do + let isize ← parse_int32 + match isize with + | Int.negSucc _ => throw "Expected positive size in len payload" + | Int.ofNat size => + pure size + + /-- Skips the LEN and its payload-/ + @[inline] + def skip : BParsec Unit := do + let size ← Len.parseSize + BParsec.forward size + +end Len + +namespace Tag +@[inline] +def parse : BParsec Tag := do + let element ← parse_uint32 + have wt_uint := element &&& 7 + let wire_type ← if wt_uint = 0 then pure WireType.VARINT + else if wt_uint = 1 then pure WireType.I64 + else if wt_uint = 2 then pure WireType.LEN + else if wt_uint = 3 then pure WireType.SGROUP + else if wt_uint = 4 then pure WireType.EGROUP + else if wt_uint = 5 then pure WireType.I32 + else throw "Unexcepted Wire Type" + have field_num := element >>> 3 + pure (Tag.mk field_num.toNat wire_type) + +@[inline] +def interpret? (b : ByteArray) : Except String Tag := + BParsec.run Tag.parse b + +@[inline] +def interpret! (b : ByteArray) : Tag := + BParsec.run! Tag.parse b + +end Tag + +namespace WireType + +@[inline] +def skip (wt : WireType) : BParsec Unit := do + match wt with + | .VARINT => VarInt.skip + | .I64 => BParsec.forward 8 + | .LEN => Len.skip + | .SGROUP => pure () + | .EGROUP => pure () + | .I32 => BParsec.forward 4 + +end WireType + +end Proto diff --git a/cedar-lean/Protobuf/Varint.lean b/cedar-lean/Protobuf/Varint.lean new file mode 100644 index 000000000..2a8787478 --- /dev/null +++ b/cedar-lean/Protobuf/Varint.lean @@ -0,0 +1,170 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.BParsec +import Protobuf.Field +import Protobuf.WireType + +/-! +Variable-width integers and parsers for their relevant +Protobuf Types +-/ + +namespace Proto + +@[inline] def msb_set8(i : UInt8) : Bool := i &&& (128 : UInt8) != 0 +@[inline] def clear_msb8(i : UInt8) : UInt8 := i &&& (127 : UInt8) + +@[inline] def msb_set32(i : UInt32) : Bool := i &&& (2147483648 : UInt32) != 0 +@[inline] def clear_msb32(i : UInt32) : UInt32 := i &&& (2147483648 : UInt32) + +@[inline] def msb_set64(i : UInt64) : Bool := i &&& (9223372036854775808 : UInt64) != 0 +@[inline] def clear_msb64(i : UInt64) : UInt64 := i &&& (9223372036854775808 : UInt64) + + +-- Does not progress iterator +-- Has panic! indexing, should work towards adding needed proof +private def find_end_of_varint_helper (n : Nat) : BParsec Nat := do + let empty ← BParsec.empty + have H0 := empty + if empty then throw "Expected more bytes" + + -- Due to the PTypes allowed, we can't have a varint with more than 10 bytes + if H : n ≥ 10 then throw "Too many bytes in this varint" else + + let msbSet ← fun it => BParsec.ParseResult.success it (msb_set8 it.data[it.pos + n]!) + if ¬msbSet then + let pos ← BParsec.pos + pure (pos + n + 1) -- Include current byte as part of varint + else + + find_end_of_varint_helper (n + 1) +termination_by 10 - n + +@[inline] +def find_end_of_varint : BParsec Nat := find_end_of_varint_helper 0 + + +/- Find the start and end indices of the next varint -/ +-- NOTE: Does not progress iterator +@[inline] +def find_varint_size : BParsec Nat := do + let start_idx ← BParsec.pos + let end_idx ← find_end_of_varint + pure (end_idx - start_idx) + + +-- Note: Panic indexing used but may be able to remove with some work +private def parse_uint64_helper (remaining : Nat) (p : Nat) (r : UInt64) : BParsec UInt64 := do + if remaining = 0 then pure r else + let empty ← BParsec.empty + if empty then throw "Expected more bytes" else + let byte ← fun it => BParsec.ParseResult.success it it.data[it.pos]! + BParsec.next -- Progress iterator + have byte2 := clear_msb8 byte + have byte3 := byte2.toUInt64 <<< (7 * p.toUInt64) + parse_uint64_helper (remaining - 1) (p + 1) (r ||| byte3) + + +@[inline] +def parse_uint64 : BParsec UInt64 := do + let remaining ← find_varint_size + parse_uint64_helper remaining 0 0 + + +instance : Field UInt64 := { + parse := parse_uint64 + checkWireType := fun (w : WireType) => WireType.VARINT = w + merge := Field.Merge.override +} + +private def parse_uint32_helper (remaining : Nat) (p : Nat) (r : UInt32) : BParsec UInt32 := do + if remaining = 0 then pure r else + let empty ← BParsec.empty -- NOTE: Might be able to remove if we add a hypotheses in the definition + if empty then throw "Expected more bytes" else + let byte ← fun it => .success it it.data[it.pos]! + BParsec.next -- Progress iterator + have byte2 := clear_msb8 byte + have byte3 := byte2.toUInt32 <<< (7 * p.toUInt32) + parse_uint32_helper (remaining - 1) (p + 1) (r ||| byte3) + + +@[inline] +def parse_uint32 : BParsec UInt32 := do + let remaining ← find_varint_size + parse_uint32_helper remaining 0 0 + +instance : Field UInt32 := { + parse := parse_uint32 + checkWireType := fun w => WireType.VARINT = w + merge := Field.Merge.override +} + +def Int32 := Int +deriving instance Inhabited, DecidableEq for Int32 +instance : OfNat Int32 n := ⟨Int.ofNat n⟩ +instance : Neg Int32 := { neg := Int.neg } + + +@[inline] +def parse_int32 : BParsec Int32 := do + let r ← parse_uint32 + if msb_set32 r then + pure (Int.neg (~~~(r - (1 : UInt32))).toNat) + else + pure (Int.ofNat r.toNat) + + +instance : Field Int32 := { + parse := parse_int32 + checkWireType := fun w => WireType.VARINT = w + merge := Field.Merge.override +} + +def Int64 := Int +deriving instance Inhabited, DecidableEq for Int64 +instance : OfNat Int64 n := ⟨Int.ofNat n⟩ +instance : Neg Int64 := { neg := Int.neg } + + +@[inline] +def parse_int64 : BParsec Int64 := do + let r ← parse_uint64 + if msb_set64 r then + pure (Int.neg (~~~(r - (1 : UInt64))).toNat) + else + pure (Int.ofNat r.toNat) + +instance : Field Int64 := { + parse := parse_int64 + checkWireType := fun w => WireType.VARINT = w + merge := Field.Merge.override +} + +@[inline] +def parse_bool : BParsec Bool := do + let result ← parse_int32 + if result = 1 then pure true else + if result = 0 then pure false else + throw "Expected 00 or 01" + +instance : Field Bool := { + parse := Proto.parse_bool + checkWireType := fun w => WireType.VARINT = w + merge := Field.Merge.override +} + +end Proto diff --git a/cedar-lean/Protobuf/WireType.lean b/cedar-lean/Protobuf/WireType.lean new file mode 100644 index 000000000..f4cc9531f --- /dev/null +++ b/cedar-lean/Protobuf/WireType.lean @@ -0,0 +1,32 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +namespace Proto + +/-! +Protobuf Wire Types +-/ + +inductive WireType where + | VARINT : WireType + | I64 : WireType + | LEN : WireType + | SGROUP : WireType + | EGROUP : WireType + | I32 : WireType +deriving Inhabited, Repr, DecidableEq + +end Proto diff --git a/cedar-lean/UnitTest/Proto.lean b/cedar-lean/UnitTest/Proto.lean new file mode 100644 index 000000000..26003af41 --- /dev/null +++ b/cedar-lean/UnitTest/Proto.lean @@ -0,0 +1,106 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Protobuf.Structures +import Protobuf.HardCodeTest +import Protobuf.String +import Protobuf.Map +import Protobuf.Field +import Protobuf.Enum +import Protobuf.Varint +import Protobuf.Packed + +/-! Test Cases for Protobuffer functions -/ + +open Proto + +-- Show DecidableEquality of Except for unit tests +namespace Except +instance [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by + unfold DecidableEq + intro a b + cases a <;> cases b <;> + -- Get rid of obvious cases where .ok != .err + try { apply isFalse ; intro h ; injection h } + case error.error c d => + match decEq c d with + | isTrue h => apply isTrue (by rw [h]) + | isFalse _ => apply isFalse (by intro h; injection h; contradiction) + case ok.ok c d => + match decEq c d with + | isTrue h => apply isTrue (by rw [h]) + | isFalse _ => apply isFalse (by intro h; injection h; contradiction) +end Except + + +#guard (@Field.interpret? Bool) (ByteArray.mk #[0]) = Except.ok false +#guard (@Field.interpret? Bool) (ByteArray.mk #[1]) = Except.ok true +#guard (@Field.interpret? UInt64) (ByteArray.mk #[150, 01]) = Except.ok 150 +#guard (@Field.interpret? Int64) (ByteArray.mk #[254, 255, 255, 255, 255, 255, 255, 255, 255, 1]) = Except.ok (-2) +#guard (@Field.interpret? (Packed Int64)) (ByteArray.mk #[06, 03, 142, 02, 158, 167, 05]) = Except.ok #[3, 270, 86942] +#guard (@Field.interpret? String) (ByteArray.mk #[07, 116, 101, 115, 116, 105, 110, 103]) = Except.ok "testing" +#guard Tag.interpret? (ByteArray.mk #[08]) = Except.ok (Tag.mk 1 WireType.VARINT) +#guard Tag.interpret? (ByteArray.mk #[18]) = Except.ok (Tag.mk 2 WireType.LEN) +#guard Tag.interpret? (ByteArray.mk #[50]) = Except.ok (Tag.mk 6 WireType.LEN) + +#guard (@Message.interpret? HardCodeStruct) (ByteArray.mk #[50, 06, 03, 142, 02, 158, 167, 05]) = + Except.ok (HardCodeStruct.mk #[3, 270, 86942]) + +def map_test : Except String (Array (String × UInt32)) := + have data := ByteArray.mk #[10, 10, 10, 06, 68, 97, 114, 99, 105, 101, 16, 04, 10, 09, 10, 05, + 83, 104, 97, 119, 110, 16, 02, 10, 09, 10, 05, 67, 97, 114, 108, 121, + 16, 04, 08, 07, 10, 03, 82, 111, 121, 16, 01] + BParsec.run (do + let mut result: Array (String × UInt32) := #[] + + let tag1 ← Tag.parse + if tag1.fieldNum != 1 then + throw "Unexpected field number" + + let element: Map String UInt32 ← Field.parse + result := (@Field.merge (Map String UInt32)) result element + + let tag2 ← Tag.parse + if tag2.fieldNum != 1 then + throw "Unexpected field number" + + let element2: Map String UInt32 ← Field.parse + result := (@Field.merge (Map String UInt32)) result element2 + + pure result + ) data + +#guard map_test = Except.ok #[("Darcie", 4), ("Shawn", 2)] + +-- Enum Test + +inductive A where + | Monday + | Tuesday + deriving Repr, Inhabited, DecidableEq + +namespace A +def get? (n: Int) : Except String A := + match n with + | 1 => .ok A.Monday + | 2 => .ok A.Tuesday + | n => .error s!"Field {n} does not exist in enum" + +instance : ProtoEnum A where + fromInt := get? +end A + +#guard (@Field.interpret? A) (ByteArray.mk #[02]) = Except.ok A.Tuesday diff --git a/cedar-lean/lakefile.lean b/cedar-lean/lakefile.lean index 452851658..3758c5659 100644 --- a/cedar-lean/lakefile.lean +++ b/cedar-lean/lakefile.lean @@ -34,6 +34,9 @@ lean_lib DiffTest where lean_lib UnitTest where defaultFacets := #[LeanLib.staticFacet] +lean_lib Protobuf where + defaultFacets := #[LeanLib.staticFacet] + lean_exe CedarUnitTests where root := `UnitTest.Main