fix packed fields not packed & default values being serialized

Author: Qiu233

Protobuf/Notation/Basic.lean

@@ -51,7 +51,7 @@ meta def mkFreshUserName (n : Name) : CommandElabM Name := do
 structure Options where
   raw : Array (Ident × Term)
   entries : Std.HashMap Name (Array Term)
-deriving Inhabited
+deriving Inhabited, Repr
 
 -- TODO: maybe force this?
 private def Options.recognized : Array Name :=
@@ -85,7 +85,7 @@ private def Options.first? (options : Options) (x : Name) : Option Term :=
 private def Options.is_true? (options : Options) (x : Name) : Option Bool :=
   if let some y := options.first? x then
     y matches `(true)
-  else false
+  else none
 
 syntax options_entry := ident " = " term
 

Protobuf/Notation/Message.lean

@@ -367,10 +367,10 @@ def computeMData.map [Monad m] [MonadQuotation m] [MonadError m] [MonadEnv m] [M
   }
 
 def computeMData.ordinary.computeShape [Monad m] [MonadQuotation m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m] [MonadRef m] [AddMessageContext m] [MonadResolveName m]
-    (mod? : Modifier) (is_scalar : Bool) (lean_type_inner : Ident) : m (TSyntax `term × LeanShape) := do
+    (mod? : Modifier) (internal_type? : Option InternalType) (enum_type? : Option Name) (lean_type_inner : Ident) : m (TSyntax `term × LeanShape) := do
   match mod? with
     | .default | .required =>
-      if is_scalar then
+      if internal_type?.isSome || enum_type?.isSome then
         pure (← `($lean_type_inner), LeanShape.strict)
       else
         pure (← `(Option $lean_type_inner), LeanShape.option)
@@ -424,7 +424,7 @@ def computeMData.ordinary [Monad m] [MonadQuotation m] [MonadError m] [MonadEnv
   let (is_scalar, internal_type?, enum_type?, oneof_type?) ← getProtoTypeMData mutEnums mutOneofs messages proto_type
   if oneof_type?.isSome && !(mod? matches .default) then
     throwErrorAt name "oneof field cannot have cardinality modifier: {oneof_type?.get!}"
-  let (lean_type, lean_shape) ← computeMData.ordinary.computeShape mod? is_scalar lean_type_inner
+  let (lean_type, lean_shape) ← computeMData.ordinary.computeShape mod? internal_type? enum_type? lean_type_inner
   let builder? ← internal_type?.mapM InternalType.builder
   let builder? := if oneof_type?.isNone then some (builder?.getD (mkIdentFrom proto_type (proto_type.getId.str "builder"))) else none
   let toMessage? := if is_scalar then none else some (mkIdentFrom proto_type (proto_type.getId.str "toMessage"))
@@ -551,7 +551,7 @@ end
 private def construct_toMessage (name : Ident) (push_name : String → Ident) (fields : Array ProtoFieldMData) : CommandElabM (Ident × Command) := do
   let msg ← mkIdent <$> mkFreshUserName `msg
   let val ← mkIdent <$> mkFreshUserName `val
-  let toMessageBody ← fields.mapM fun {mod, field_proj, field_num, options, is_scalar, builder?, oneof_type?, toMessage?, test_unset, map_info?, ..} => do
+  let toMessageBody ← fields.mapM fun {mod, field_proj, field_num, options, is_scalar, internal_type?, builder?, enum_type?, oneof_type?, toMessage?, test_unset, map_info?, ..} => do
     if let some map_info := map_info? then
       let entries ← mkIdent <$> mkFreshUserName `entries
       let submsg ← mkIdent <$> mkFreshUserName `submsg
@@ -586,7 +586,7 @@ private def construct_toMessage (name : Ident) (push_name : String → Ident) (f
       let builder := builder?.get!
       match mod with
       | .default =>
-        if is_scalar then
+        if internal_type?.isSome || enum_type?.isSome then
           `(Parser.Term.doSeqItem| let $msg ← do
             if $test_unset ($field_proj $val) then
               pure $msg
@@ -595,7 +595,7 @@ private def construct_toMessage (name : Ident) (push_name : String → Ident) (f
         else
           `(Parser.Term.doSeqItem| let $msg ← $field_num:num <~? (Option.mapM $builder ($field_proj $val)) # $msg)
       | .required =>
-        if is_scalar then
+        if internal_type?.isSome || enum_type?.isSome then
           `(Parser.Term.doSeqItem| let $msg ← do
             if $test_unset ($field_proj $val) then
               pure $msg
@@ -612,10 +612,20 @@ private def construct_toMessage (name : Ident) (push_name : String → Ident) (f
       | .optional =>
         `(Parser.Term.doSeqItem| let $msg ← $field_num:num <~? (Option.mapM $builder ($field_proj $val)) # $msg)
       | .repeated =>
-        if options.packed?.getD is_scalar then
-          `(Parser.Term.doSeqItem| let $msg ← $field_num:num <~p (Array.mapM $builder ($field_proj $val)) # $msg)
+        if options.packed?.isEqSome true then
+          `(Parser.Term.doSeqItem|
+            let $msg ← do
+              if $test_unset ($field_proj $val) then
+                pure $msg
+              else
+                $field_num:num <~p (Array.mapM $builder ($field_proj $val)) # $msg)
         else
-          `(Parser.Term.doSeqItem| let $msg ← $field_num:num <~f (Array.mapM $builder ($field_proj $val)) # $msg)
+          `(Parser.Term.doSeqItem|
+            let $msg ← do
+              if $test_unset ($field_proj $val) then
+                pure $msg
+              else
+                $field_num:num <~f (Array.mapM $builder ($field_proj $val)) # $msg)
   let toMessageId := push_name "toMessage"
   let toMessage ← `(partial def $toMessageId:ident : $name → Except Protobuf.Encoding.ProtoError Protobuf.Encoding.Message := fun $val => do
     let $msg:ident := Protobuf.Encoding.Message.emptyWithCapacity $(quote fields.size)
@@ -637,7 +647,7 @@ private def construct_builder (name : Ident) (push_name : String → Ident) (toM
 private def construct_fromMessage (name : Ident) (push_name : String → Ident) (fields : Array ProtoFieldMData) : CommandElabM (Ident × Command) := do
   let msg ← mkIdent <$> mkFreshUserName `msg
   let ns := fields.map ProtoFieldMData.field_num
-  let decoder ← fields.mapM (β := (Ident × TSyntax ``Parser.Term.doSeqItem)) fun {mod, field_name, field_proj, field_num, options, is_scalar, oneof_type?, decoder??, decoder_rep?, decoder_rep_packed?, fromMessage??, map_info?, ..} => do
+  let decoder ← fields.mapM (β := (Ident × TSyntax ``Parser.Term.doSeqItem)) fun {mod, field_name, field_proj, field_num, options, is_scalar, internal_type?, enum_type?, oneof_type?, decoder??, decoder_rep?, decoder_rep_packed?, fromMessage??, map_info?, ..} => do
     let var ← mkIdent <$> mkFreshUserName (field_name.getId)
     if let some map_info := map_info? then
       let key_decoder? := map_info.key_decoder?
@@ -668,12 +678,12 @@ private def construct_fromMessage (name : Ident) (push_name : String → Ident)
       let decoder? := decoder??.get!
       let stx ← match mod with
         | .default =>
-          if is_scalar then
+          if internal_type?.isSome || enum_type?.isSome then
             `(Parser.Term.doSeqItem| let $var ← ($decoder? $msg $field_num:num <&> (fun x => Option.getD x Inhabited.default)))
           else
             `(Parser.Term.doSeqItem| let $var ← ($decoder? $msg $field_num:num))
         | .required =>
-          if is_scalar then
+          if internal_type?.isSome || enum_type?.isSome then
             `(Parser.Term.doSeqItem| let $var ← ($decoder? $msg $field_num:num >>= (fun x => Option.getDM x
               (throw (Protobuf.Encoding.ProtoError.missingRequiredField s!"required field `{$(quote field_proj.getId.toString)}` is missing when decoding the message")))))
           else
@@ -686,7 +696,7 @@ private def construct_fromMessage (name : Ident) (push_name : String → Ident)
         | .optional =>
           `(Parser.Term.doSeqItem| let $var ← ($decoder? $msg $field_num:num))
         | .repeated =>
-          if options.packed?.getD is_scalar then
+          if options.packed?.isEqSome true then
             assert! decoder_rep_packed?.isSome
             let decoder_rep_packed := decoder_rep_packed?.get!
             `(Parser.Term.doSeqItem| let $var ← ($decoder_rep_packed $msg $field_num:num))
@@ -730,7 +740,7 @@ private def construct_decoder_rep (name : Ident) (push_name : String → Ident)
 private def construct_merge (name : Ident) (push_name : String → Ident) (fields : Array ProtoFieldMData) : CommandElabM (Ident × Command) := do
   let a ← mkIdent <$> mkFreshUserName `a
   let b ← mkIdent <$> mkFreshUserName `b
-  let mergeBody ← fields.mapM (β := (Ident × TSyntax ``Parser.Term.doSeqItem)) fun {mod, proto_type, field_name, field_proj := field_proj, is_scalar, oneof_type?, map_info?, ..} => do
+  let mergeBody ← fields.mapM (β := (Ident × TSyntax ``Parser.Term.doSeqItem)) fun {mod, proto_type, field_name, field_proj, internal_type?, enum_type?, oneof_type?, map_info?, ..} => do
     let var ← mkIdent <$> mkFreshUserName (field_name.getId)
     let va ← `($field_proj $a)
     let vb ← `($field_proj $b)
@@ -744,18 +754,16 @@ private def construct_merge (name : Ident) (push_name : String → Ident) (field
     else
       let stx ← match mod with
         | .default | .required =>
-          if is_scalar then
+          if internal_type?.isSome || enum_type?.isSome then
             `(Parser.Term.doSeqItem| let $var := $vb)
-          else if (proto_type matches `(string) | `(bytes)) then
-            `(Parser.Term.doSeqItem| let $var := $vb <|> $va) -- optional, last first
           else
             `(Parser.Term.doSeqItem| let $var := match $va:term, $vb:term with
               | Option.some x, Option.some y => Option.some ($merger x y)
               | Option.some x, _ => Option.some x
               | _, Option.some y => Option.some y
               | _, _ => Option.none)
         | .optional =>
-          if is_scalar || (proto_type matches `(string) | `(bytes)) then
+          if internal_type?.isSome || enum_type?.isSome then
             `(Parser.Term.doSeqItem| let $var := $vb <|> $va)
           else
             `(Parser.Term.doSeqItem| let $var := match $va:term, $vb:term with

Protobuf/Versions/Proto3.lean

@@ -206,10 +206,15 @@ private def field_modifier? (field : FieldDescriptorProto) : M (Option (TSyntax
     else
       return none
 
+set_option hygiene false in
 private def field_options? (field : FieldDescriptorProto) : M (Option (TSyntax ``options)) := do
   let mut entries := #[]
   if let some packed := field.options&.packed then
     entries := entries.push (← `(options_entry| packed = $(quote packed)))
+  else
+    if let some type := field.type then
+      unless type matches .TYPE_STRING | .TYPE_GROUP | .TYPE_MESSAGE | .TYPE_BYTES do
+        entries := entries.push (← `(options_entry| packed = true)) -- NOTE: proto3 defaults to packed
   if !! field.options&.deprecated then
     entries := entries.push (← `(options_entry| deprecated = true))
   if entries.isEmpty then

Test/Proto3.lean

@@ -0,0 +1,161 @@
+module
+
+import Protobuf.Encoding
+meta import Protobuf.Notation
+meta import Protobuf.Elab
+
+open Protobuf Encoding
+open scoped Protobuf.Notation
+
+set_option protobuf.trace.notation true
+
+#load_proto_file "Test/Proto3.proto"
+
+def ofExcept {α} (e : Except ProtoError α) : IO α := do
+  match e with
+  | .ok v => pure v
+  | .error err => throw (IO.userError err.toString)
+
+def assert (cond : Bool) (msg : String) : IO Unit := do
+  if cond then pure () else throw (IO.userError msg)
+
+def assertEq [BEq α] (a b : α) (msg : String) : IO Unit := do
+  assert (a == b) msg
+
+def testDefaults : IO Unit := do
+  let val : _root_.test.proto3.All := default
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  assert msg.records.isEmpty "proto3 defaults should not serialize"
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage Message.empty)
+  assertEq decoded.int32_field (0 : Int32) "default int32_field mismatch"
+  assertEq decoded.string_field "" "default string_field mismatch"
+  assertEq decoded.bool_field false "default bool_field mismatch"
+  assertEq decoded.bytes_field ByteArray.empty "default bytes_field mismatch"
+  assertEq decoded.float_field (0 : Float32) "default float_field mismatch"
+  assertEq decoded.double_field (0 : Float) "default double_field mismatch"
+  assertEq decoded.uint32_field (0 : UInt32) "default uint32_field mismatch"
+  assertEq decoded.uint64_field (0 : UInt64) "default uint64_field mismatch"
+  assertEq decoded.sint32_field (0 : Int32) "default sint32_field mismatch"
+  assertEq decoded.sint64_field (0 : Int64) "default sint64_field mismatch"
+  assertEq decoded.fixed32_field (0 : UInt32) "default fixed32_field mismatch"
+  assertEq decoded.fixed64_field (0 : UInt64) "default fixed64_field mismatch"
+  assertEq decoded.sfixed32_field (0 : Int32) "default sfixed32_field mismatch"
+  assertEq decoded.sfixed64_field (0 : Int64) "default sfixed64_field mismatch"
+  assertEq decoded.color _root_.test.proto3.Color.COLOR_UNSPECIFIED "default enum mismatch"
+  assert decoded.sub.isNone "default sub mismatch"
+  assertEq decoded.opt_int32 none "default opt_int32 mismatch"
+  assertEq decoded.rep_int32 #[] "default rep_int32 mismatch"
+  assertEq decoded.rep_int32_unpacked #[] "default rep_int32_unpacked mismatch"
+  assertEq decoded.rep_color #[] "default rep_color mismatch"
+  assert (decoded.map_str_int32.size == 0) "default map mismatch"
+  assert decoded.choice.isNone "default choice mismatch"
+  assert decoded.rep_sub.isEmpty "default rep_sub mismatch"
+
+def testOptionalPresence : IO Unit := do
+  let base : _root_.test.proto3.All := default
+  let val : _root_.test.proto3.All := { base with opt_int32 := some 0 }
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  assert ((Message.getRecordsOf msg 17).size == 1) "optional field should serialize when set"
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  assertEq decoded.opt_int32 (some (0 : Int32)) "optional presence mismatch"
+
+def testSubPresence : IO Unit := do
+  let sub : _root_.test.proto3.Sub := { id := 0 }
+  let base : _root_.test.proto3.All := default
+  let val : _root_.test.proto3.All := { base with sub := some sub }
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  assert ((Message.getRecordsOf msg 16).size == 1) "message field should serialize when present"
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  match decoded.sub with
+  | some v => assertEq v.id (0 : Int32) "message field presence mismatch"
+  | none => throw (IO.userError "message field presence mismatch")
+
+def testOneof : IO Unit := do
+  let choice : _root_.test.proto3.All.choice_Type := _root_.test.proto3.All.choice_Type.oneof_int32 7
+  let base : _root_.test.proto3.All := default
+  let val : _root_.test.proto3.All := { base with choice := some choice }
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  assert ((Message.getRecordsOf msg 22).size == 1) "oneof field did not serialize"
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  match decoded.choice with
+  | some (.oneof_int32 v) => assertEq v (7 : Int32) "oneof int32 value mismatch"
+  | _ => throw (IO.userError "oneof decode mismatch")
+
+def testPackedAndUnpacked : IO Unit := do
+  let base : _root_.test.proto3.All := default
+  let val : _root_.test.proto3.All := {
+    base with
+    rep_int32 := #[(1 : Int32), 2],
+    rep_int32_unpacked := #[(3 : Int32), 4]
+  }
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  let repPacked := Message.getRecordsOf msg 18
+  assert (repPacked.size == 1) "packed repeated field should be a single record"
+  match repPacked[0]!.value with
+  | .LEN _ => pure ()
+  | _ => throw (IO.userError "packed repeated field should use LEN wire type")
+  let repUnpacked := Message.getRecordsOf msg 19
+  assert (repUnpacked.size == 2) "unpacked repeated field should be multiple records"
+  for r in repUnpacked do
+    match r.value with
+    | .VARINT _ => pure ()
+    | _ => throw (IO.userError "unpacked repeated field should use VARINT wire type")
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  assertEq decoded.rep_int32 #[(1 : Int32), 2] "packed repeated decode mismatch"
+  assertEq decoded.rep_int32_unpacked #[(3 : Int32), 4] "unpacked repeated decode mismatch"
+
+def testPackedAcceptsUnpacked : IO Unit := do
+  let msg := Message.set Message.empty 18 (.VARINT 1)
+  let msg := Message.set msg 18 (.VARINT 2)
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  assertEq decoded.rep_int32 #[(1 : Int32), 2] "packed field should accept unpacked encoding"
+
+def testMapRoundtrip : IO Unit := do
+  let map := Std.HashMap.ofList [("a", (1 : Int32)), ("b", (2 : Int32))]
+  let base : _root_.test.proto3.All := default
+  let val : _root_.test.proto3.All := { base with map_str_int32 := map }
+  let msg ← ofExcept (_root_.test.proto3.All.toMessage val)
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  assertEq (decoded.map_str_int32.get? "a") (some (1 : Int32)) "map value mismatch for key a"
+  assertEq (decoded.map_str_int32.get? "b") (some (2 : Int32)) "map value mismatch for key b"
+
+def testUnknownEnum : IO Unit := do
+  let msg := Message.set Message.empty 15 (.VARINT 9)
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  match decoded.color with
+  | _root_.test.proto3.Color.«Unknown.Value» raw =>
+      assertEq raw (9 : Int32) "unknown enum raw value mismatch"
+  | _ => throw (IO.userError "unknown enum value should be preserved")
+
+def testUnknownFields : IO Unit := do
+  let msg := Message.set Message.empty 99 (.VARINT 123)
+  let decoded ← ofExcept (_root_.test.proto3.All.fromMessage msg)
+  match decoded.«Unknown.Fields».get? 99 with
+  | some vals => assert (vals.size == 1) "unknown field should be preserved"
+  | none => throw (IO.userError "unknown field missing")
+  let roundtrip ← ofExcept (_root_.test.proto3.All.toMessage decoded)
+  assert ((Message.getRecordsOf roundtrip 99).size == 1) "unknown field should round-trip"
+
+def runTest (name : String) (t : IO Unit) (errs : IO.Ref (Array String)) : IO Unit := do
+  try
+    t
+  catch e =>
+    errs.modify (·.push s!"{name}: {e.toString}")
+
+def testProto3 : IO Unit := do
+  let errs ← IO.mkRef #[]
+  runTest "testDefaults" testDefaults errs
+  runTest "testOptionalPresence" testOptionalPresence errs
+  runTest "testSubPresence" testSubPresence errs
+  runTest "testOneof" testOneof errs
+  runTest "testPackedAndUnpacked" testPackedAndUnpacked errs
+  runTest "testPackedAcceptsUnpacked" testPackedAcceptsUnpacked errs
+  runTest "testMapRoundtrip" testMapRoundtrip errs
+  runTest "testUnknownEnum" testUnknownEnum errs
+  runTest "testUnknownFields" testUnknownFields errs
+  let failures ← errs.get
+  unless failures.isEmpty do
+    let msg := String.intercalate "\n" failures.toList
+    throw (IO.userError msg)
+
+#eval! testProto3

Test/Proto3.proto

@@ -0,0 +1,43 @@
+syntax = "proto3";
+
+package test.proto3;
+
+message Sub {
+  int32 id = 1;
+}
+
+enum Color {
+  COLOR_UNSPECIFIED = 0;
+  RED = 1;
+  GREEN = 2;
+}
+
+message All {
+  int32 int32_field = 1;
+  string string_field = 2;
+  bool bool_field = 3;
+  bytes bytes_field = 4;
+  float float_field = 5;
+  double double_field = 6;
+  uint32 uint32_field = 7;
+  uint64 uint64_field = 8;
+  sint32 sint32_field = 9;
+  sint64 sint64_field = 10;
+  fixed32 fixed32_field = 11;
+  fixed64 fixed64_field = 12;
+  sfixed32 sfixed32_field = 13;
+  sfixed64 sfixed64_field = 14;
+  Color color = 15;
+  Sub sub = 16;
+  optional int32 opt_int32 = 17;
+  repeated int32 rep_int32 = 18;
+  repeated int32 rep_int32_unpacked = 19 [packed = false];
+  repeated Color rep_color = 20;
+  map<string, int32> map_str_int32 = 21;
+  oneof choice {
+    int32 oneof_int32 = 22;
+    string oneof_string = 23;
+    Sub oneof_sub = 24;
+  }
+  repeated Sub rep_sub = 25;
+}