From 4cd9eceb6b06416c24e1d7412e41d306cd7e7ff4 Mon Sep 17 00:00:00 2001 From: Craig Disselkoen Date: Thu, 21 Nov 2024 12:33:55 -0800 Subject: [PATCH] [cedar-lean] actually run protobuf tests (#483) Signed-off-by: Craig Disselkoen --- cedar-lean/Protobuf/Map.lean | 11 +- cedar-lean/Protobuf/Structures.lean | 8 ++ cedar-lean/Protobuf/Varint.lean | 4 +- cedar-lean/UnitTest.lean | 1 + cedar-lean/UnitTest/Main.lean | 4 +- cedar-lean/UnitTest/Proto.lean | 181 +++++++++++++++++++--------- 6 files changed, 145 insertions(+), 64 deletions(-) diff --git a/cedar-lean/Protobuf/Map.lean b/cedar-lean/Protobuf/Map.lean index a5f9405a5..99b32a45e 100644 --- a/cedar-lean/Protobuf/Map.lean +++ b/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 diff --git a/cedar-lean/Protobuf/Structures.lean b/cedar-lean/Protobuf/Structures.lean index 9456c96a7..e50a3a754 100644 --- a/cedar-lean/Protobuf/Structures.lean +++ b/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 diff --git a/cedar-lean/Protobuf/Varint.lean b/cedar-lean/Protobuf/Varint.lean index 6b3c549ba..f0b64fe4e 100644 --- a/cedar-lean/Protobuf/Varint.lean +++ b/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 } diff --git a/cedar-lean/UnitTest.lean b/cedar-lean/UnitTest.lean index 511cb1368..456bb4aba 100644 --- a/cedar-lean/UnitTest.lean +++ b/cedar-lean/UnitTest.lean @@ -17,4 +17,5 @@ import UnitTest.Decimal import UnitTest.IPAddr import UnitTest.Main +import UnitTest.Proto import UnitTest.Run diff --git a/cedar-lean/UnitTest/Main.lean b/cedar-lean/UnitTest/Main.lean index 60d7ea139..44432cbd0 100644 --- a/cedar-lean/UnitTest/Main.lean +++ b/cedar-lean/UnitTest/Main.lean @@ -16,6 +16,7 @@ import UnitTest.Decimal import UnitTest.IPAddr +import UnitTest.Proto import UnitTest.Wildcard open UnitTest @@ -23,7 +24,8 @@ open UnitTest def tests := Decimal.tests ++ IPAddr.tests ++ - Wildcard.tests + Wildcard.tests ++ + Proto.tests def main : IO UInt32 := do TestSuite.runAll tests diff --git a/cedar-lean/UnitTest/Proto.lean b/cedar-lean/UnitTest/Proto.lean index 26003af41..256a0978b 100644 --- a/cedar-lean/UnitTest/Proto.lean +++ b/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)) +]