Skip to content

Commit

Permalink
add Lean protobuf library (#478)
Browse files Browse the repository at this point in the history
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
  • Loading branch information
cdisselkoen authored Nov 20, 2024
1 parent b511731 commit 420b4cc
Show file tree
Hide file tree
Showing 15 changed files with 1,418 additions and 0 deletions.
27 changes: 27 additions & 0 deletions cedar-lean/Protobuf.lean
Original file line number Diff line number Diff line change
@@ -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
163 changes: 163 additions & 0 deletions cedar-lean/Protobuf/BParsec.lean
Original file line number Diff line number Diff line change
@@ -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
57 changes: 57 additions & 0 deletions cedar-lean/Protobuf/ByteArray.lean
Original file line number Diff line number Diff line change
@@ -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
45 changes: 45 additions & 0 deletions cedar-lean/Protobuf/Enum.lean
Original file line number Diff line number Diff line change
@@ -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
72 changes: 72 additions & 0 deletions cedar-lean/Protobuf/Field.lean
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 420b4cc

Please sign in to comment.