Change in libgfxinit[master]: dp aux: Add TODO and pre-condition for I2C writes

[Nico Huber (Code Review)]

Attention is currently required from: Angel Pons.
Hello Angel Pons,

I'd like you to do a code review. Please visit

https://review.coreboot.org/c/libgfxinit/+/52824

to review the following change.

Change subject: dp aux: Add TODO and pre-condition for I2C writes
......................................................................

dp aux: Add TODO and pre-condition for I2C writes

Change-Id: If7566fc7b701c8a36d9e8a0af5beb7a84a558ee3
Signed-off-by: Nico Huber 
---
M common/hw-gfx-dp_aux_ch.adb
1 file changed, 11 insertions(+), 0 deletions(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/24/52824/1

diff --git a/common/hw-gfx-dp_aux_ch.adb b/common/hw-gfx-dp_aux_ch.adb
index b8eb510..854a2bc 100644
--- a/common/hw-gfx-dp_aux_ch.adb
+++ b/common/hw-gfx-dp_aux_ch.adb
@@ -178,6 +178,15 @@
       Length            : in     DP_Defs.Aux_Payload_Length;
       Data              : in     DP_Defs.Aux_Payload;
       Success           :    out Boolean)
+   with
+      -- TODO: The justification below turns out to be wrong. There is
+      --       another way to signal a deferred final ACK:
+      --       When multiple bytes are written and not all of them are
+      --       ack'ed yet, we should receive AUX-ACK/I2C-ACK with the
+      --       number of already written bytes as response. So far our
+      --       API only allows single-byte writes, so we can limit the
+      --       `Length` here.
+      Pre => Length <= 1
    is
       Request : DP_Defs.Aux_Request;

@@ -276,6 +285,8 @@
       Length   : in     DP_Defs.Aux_Payload_Length;
       Data     : in     DP_Defs.Aux_Payload;
       Success  :    out Boolean)
+   with
+      Pre => Length <= 1   -- see I2C_Out_Packet()
    is
       Ignored_Success : Boolean;
    begin