Is there a codegen bug in positional?

TestModels/Positional/Model/positional.smithy

@@ -11,7 +11,7 @@ use aws.polymorph#reference
 service SimplePositional {
   version: "2021-11-01",
   resources: [],
-  operations: [ GetResource, GetResourcePositional ],
+  operations: [ GetResource, GetResourcePositional, GetIntegerInputPosition, GetIntegerOutputPosition ],
   errors: [ SimplePositionalException ],
 }
 
@@ -73,3 +73,33 @@ structure GetResourcePositionalOutput {
   @required
   output: SimpleResourceReference
 }
+
+operation GetIntegerInputPosition {
+  input: GetIntegerInputPositionInput
+  output: GetIntegerInputPositionOutput,
+}
+
+@positional
+structure GetIntegerInputPositionInput {
+  @required
+  value: Integer
+}
+
+structure GetIntegerInputPositionOutput {
+  value: Integer
+}
+
+operation GetIntegerOutputPosition {
+  input: GetIntegerOutputPositionInput
+  output: GetIntegerOutputPositionOutput,
+}
+
+structure GetIntegerOutputPositionInput {
+  value: Integer
+}
+
+@positional
+structure GetIntegerOutputPositionOutput {
+  @required
+  value: Integer
+}

TestModels/Positional/src/SimplePositionalImpl.dfy

@@ -13,14 +13,12 @@ module SimplePositionalImpl refines AbstractSimplePositionalOperations {
   {true}
   function ModifiesInternalConfig(config: InternalConfig): set<object>
   {{}}
+
   predicate GetResourceEnsuresPublicly(input: GetResourceInput , output: Result<GetResourceOutput, Error>)
   {true}
 
-
-
   method GetResource ( config: InternalConfig , input: GetResourceInput )
     returns (output: Result<GetResourceOutput, Error>)
-
   {
     var resource := new SimpleResource.SimpleResource(
       input.name
@@ -31,20 +29,36 @@ module SimplePositionalImpl refines AbstractSimplePositionalOperations {
     return Success(result);
   }
 
-
   predicate GetResourcePositionalEnsuresPublicly(input: string , output: Result<ISimpleResource, Error>)
   {true}
 
-
-
   // @positional allows use to accept the input parameters directly without the input structure
   method GetResourcePositional ( config: InternalConfig , input: string )
     returns (output: Result<ISimpleResource, Error>)
-
   {
     var resource := new SimpleResource.SimpleResource(input);
 
     // @positional allows use to return the result without the output structure
     return Success(resource);
   }
-}
+
+  predicate GetIntegerInputPositionEnsuresPublicly(input: int32 , output: Result<GetIntegerInputPositionOutput, Error>)
+  {true}
+
+  method GetIntegerInputPosition ( config: InternalConfig , input: int32 )
+    returns (output: Result<GetIntegerInputPositionOutput, Error>)
+  {
+    var res := GetIntegerInputPositionOutput(value := Some(input));
+    return Success(res);
+  }
+
+  predicate GetIntegerOutputPositionEnsuresPublicly(input: GetIntegerOutputPositionInput , output: Result<int32, Error>)
+  {true}
+
+  method GetIntegerOutputPosition ( config: InternalConfig , input: GetIntegerOutputPositionInput )
+    returns (output: Result<int32, Error>)
+  {
+    expect input.value.Some?;
+    return Success(input.value.UnwrapOr(-1));
+  }
+}

TestModels/Positional/test/SimplePositionalImplTest.dfy

@@ -14,6 +14,8 @@ module {:options "--function-syntax:4"} SimplePositionalImplTest {
     {
         TestGetResource(client);
         TestGetResourcePositional(client);
+        GetIntegerInputPosition(client);
+        GetIntegerOutputPosition(client);
     }
 
     method TestGetResource(client: Types.ISimplePositionalClient)
@@ -41,6 +43,28 @@ module {:options "--function-syntax:4"} SimplePositionalImplTest {
         expect getNameOutput.name == "TestPositional";
     }
 
+    method GetIntegerInputPosition(client: Types.ISimplePositionalClient) 
+        requires client.ValidState()
+        modifies client.Modifies
+        ensures client.ValidState()
+    {
+        var input := 5;
+        var ret :- expect client.GetIntegerInputPosition(input);
+        expect ret.value.UnwrapOr(0) == input;
+    }
+
+    method GetIntegerOutputPosition(client: Types.ISimplePositionalClient) 
+        requires client.ValidState()
+        modifies client.Modifies
+        ensures client.ValidState()
+    {
+        var inputInteger:= 5;
+        var input := Types.GetIntegerOutputPositionInput(value:= Some(inputInteger));
+        var ret :- expect client.GetIntegerOutputPosition(input);
+        expect ret == inputInteger;
+    }
+
+
     method {:test} TestDefaultConfig() {
         var client :- expect SimplePositional.SimplePositional();
         TestClient(client);