[cedar-lean] actually run protobuf tests (#483)

Signed-off-by: Craig Disselkoen <[email protected]>

cedar-lean/Protobuf/Map.lean

@@ -28,8 +28,15 @@ def Map (KeyT ValueT : Type) [Field KeyT] [Field ValueT] := Array (KeyT × Value
 
 namespace Map
 
-instance {α β : Type} [Field α] [Field β] : Inhabited (Map α β) where
-     default := #[]
+instance [Field α] [Field β] [Repr α] [Repr β] : Repr (Map α β) where
+  reprPrec m n := let a : Array (α × β) := m ; reprPrec a n
+
+instance [Field α] [Field β] : Inhabited (Map α β) where
+  default := #[]
+
+instance [Field α] [Field β] [DecidableEq α] [DecidableEq β] : DecidableEq (Map α β) := by
+  unfold DecidableEq Map
+  exact decEq
 
 @[inline]
 def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BParsec (Map KeyT ValueT) := do

cedar-lean/Protobuf/Structures.lean

@@ -100,4 +100,12 @@ def skip (wt : WireType) : BParsec Unit := do
 
 end WireType
 
+namespace Field
+
+def guardedParse (t : Proto.Tag) [Field α] : BParsec α := do
+  @guardWireType α _ t.wireType
+  Field.parse
+
+end Field
+
 end Proto

cedar-lean/Protobuf/Varint.lean

@@ -112,7 +112,7 @@ instance : Field UInt32 := {
 }
 
 def Int32 := Int
-deriving instance Inhabited, DecidableEq for Int32
+deriving instance Repr, Inhabited, DecidableEq for Int32
 instance : OfNat Int32 n := ⟨Int.ofNat n⟩
 instance : Neg Int32 := { neg := Int.neg }
 
@@ -133,7 +133,7 @@ instance : Field Int32 := {
 }
 
 def Int64 := Int
-deriving instance Inhabited, DecidableEq for Int64
+deriving instance Repr, Inhabited, DecidableEq for Int64
 instance : OfNat Int64 n := ⟨Int.ofNat n⟩
 instance : Neg Int64 := { neg := Int.neg }
 

cedar-lean/UnitTest.lean

@@ -17,4 +17,5 @@
 import UnitTest.Decimal
 import UnitTest.IPAddr
 import UnitTest.Main
+import UnitTest.Proto
 import UnitTest.Run

cedar-lean/UnitTest/Main.lean

@@ -16,14 +16,16 @@
 
 import UnitTest.Decimal
 import UnitTest.IPAddr
+import UnitTest.Proto
 import UnitTest.Wildcard
 
 open UnitTest
 
 def tests :=
   Decimal.tests ++
   IPAddr.tests ++
-  Wildcard.tests
+  Wildcard.tests ++
+  Proto.tests
 
 def main : IO UInt32 := do
   TestSuite.runAll tests

cedar-lean/UnitTest/Proto.lean

@@ -15,82 +15,71 @@
 -/
 
 import Protobuf.Structures
-import Protobuf.HardCodeTest
 import Protobuf.String
 import Protobuf.Map
 import Protobuf.Field
+import Protobuf.Message
 import Protobuf.Enum
 import Protobuf.Varint
 import Protobuf.Packed
+import UnitTest.Run
 
 /-! Test Cases for Protobuffer functions -/
 
 open Proto
 
--- Show DecidableEquality of Except for unit tests
+-- Show DecidableEq 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)
+  cases a <;> cases b <;> simp only [reduceCtorEq, ok.injEq, error.injEq]
+  case ok.error | error.ok => exact instDecidableFalse
+  case error.error c d => exact decEq c d
+  case ok.ok c d => exact decEq c d
 end Except
 
+namespace Proto
 
-#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
+/-!
+Struct with array of UInt32 for testing purposes
+-/
+private structure HardCodeStruct where
+  f6 : Array UInt32 -- Field 6
+deriving Inhabited, Repr, DecidableEq
+
+namespace HardCodeStruct
+
+def merge_6 (result : HardCodeStruct) (x : Array UInt32) : HardCodeStruct :=
+  {
+    f6 := Field.merge (α := Packed UInt32) result.f6 x
+  }
+
+def merge (x : HardCodeStruct) (y : HardCodeStruct) : HardCodeStruct :=
+  {
+    f6 := Field.merge (α := Packed UInt32) x.f6 y.f6
+  }
+
+def parseField (t : Tag) : BParsec (MergeFn HardCodeStruct) := do
+  match t.fieldNum with
+    | 6 =>
+      let x : Packed UInt32 ← Field.guardedParse t
+      pure (merge_6 · x)
+    | _ =>
+      t.wireType.skip
+      pure id
+
+instance : Message HardCodeStruct := {
+  parseField := parseField
+  merge := merge
+}
+
+end HardCodeStruct
+
+private inductive A where
+  | Monday
+  | Tuesday
+deriving Repr, Inhabited, DecidableEq
 
 namespace A
 def get? (n: Int) : Except String A :=
@@ -103,4 +92,78 @@ instance : ProtoEnum A where
   fromInt := get?
 end A
 
-#guard (@Field.interpret? A) (ByteArray.mk #[02]) = Except.ok A.Tuesday
+
+def tests := [
+  UnitTest.suite "General protobuf deserialization tests" ([
+    UnitTest.test "false" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := Bool) (ByteArray.mk #[0]))
+      (.ok false)
+    ⟩,
+    UnitTest.test "true" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := Bool) (ByteArray.mk #[1]))
+      (.ok true)
+    ⟩,
+    UnitTest.test "UInt64" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := UInt64) (ByteArray.mk #[150, 01]))
+      (.ok 150)
+    ⟩,
+    UnitTest.test "Int64" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := Int64) (ByteArray.mk #[254, 255, 255, 255, 255, 255, 255, 255, 255, 1]))
+      (.ok (-2))
+    ⟩,
+    UnitTest.test "Packed Int64" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := Packed Int64) (ByteArray.mk #[06, 03, 142, 02, 158, 167, 05]))
+      (.ok #[3, 270, 86942])
+    ⟩,
+    UnitTest.test "String" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := String) (ByteArray.mk #[07, 116, 101, 115, 116, 105, 110, 103]))
+      (.ok "testing")
+    ⟩,
+    UnitTest.test "Tag 1" ⟨λ () => UnitTest.checkEq
+      (Tag.interpret? (ByteArray.mk #[08]))
+      (.ok (Tag.mk 1 WireType.VARINT))
+    ⟩,
+    UnitTest.test "Tag 2" ⟨λ () => UnitTest.checkEq
+      (Tag.interpret? (ByteArray.mk #[18]))
+      (.ok (Tag.mk 2 WireType.LEN))
+    ⟩,
+    UnitTest.test "Tag 6" ⟨λ () => UnitTest.checkEq
+      (Tag.interpret? (ByteArray.mk #[50]))
+      (.ok (Tag.mk 6 WireType.LEN))
+    ⟩,
+    UnitTest.test "HardCodeStruct" ⟨λ () => UnitTest.checkEq
+      (Message.interpret? (α := HardCodeStruct) (ByteArray.mk #[50, 06, 03, 142, 02, 158, 167, 05]))
+      (.ok (HardCodeStruct.mk #[3, 270, 86942]))
+    ⟩,
+    UnitTest.test "Enum" ⟨λ () => UnitTest.checkEq
+      (Field.interpret? (α := A) (ByteArray.mk #[02]))
+      (.ok A.Tuesday)
+    ⟩,
+    UnitTest.test "map" ⟨λ () => UnitTest.checkEq
+      (
+        let 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]
+        let interpret_map := 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
+        )
+        interpret_map data
+      )
+      (.ok #[("Darcie", 4), ("Shawn", 2)])
+    ⟩,
+  ] : List (UnitTest.TestCase IO))
+]