From 14a6ba380f4732310e2d4fa61b346e3c9aa12968 Mon Sep 17 00:00:00 2001
From: Lukas Zobernig <zlukas@google.com>
Date: Tue, 10 Mar 2026 13:30:01 +0000
Subject: [PATCH] Add signed byte and word conversion support.

---
 src/coqutil/Byte.v            | 11 +++++++++++
 src/coqutil/Word/Properties.v | 26 ++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/src/coqutil/Byte.v b/src/coqutil/Byte.v
index 3d99312c..0cda5d70 100644
--- a/src/coqutil/Byte.v
+++ b/src/coqutil/Byte.v
@@ -1,5 +1,6 @@
 Require Coq.Init.Byte Coq.Strings.Byte.
 Require Import Coq.ZArith.ZArith.
+From coqutil Require Import Z.PushPullMod.
 
 Local Open Scope Z_scope.
 
@@ -12,6 +13,10 @@ Module byte.
 
   Definition wrap(z: Z): Z := z mod 2 ^ 8.
 
+  Definition swrap(z : Z): Z := (z + 2^7) mod 2^8 - 2^7.
+
+  Definition signed(b: byte): Z := swrap (byte.unsigned b).
+
   Lemma wrap_range z:
     0 <= byte.wrap z < 2 ^ 8.
   Proof. apply Z.mod_pos_bound. reflexivity. Qed.
@@ -122,4 +127,10 @@ Module byte.
   (* FIXME isn't this defined somewhere already? *)
   Definition and (b1 b2: byte) := byte.of_Z (Z.land (byte.unsigned b1) (byte.unsigned b2)).
   Definition xor a b := byte.of_Z (Z.lxor (byte.unsigned a) (byte.unsigned b)).
+
+  Lemma swrap_wrap b : byte.swrap (byte.wrap b) = byte.swrap b.
+  Proof.
+    cbv [byte.wrap byte.swrap].
+    Z.mod_equality.
+  Qed.
 End byte.
diff --git a/src/coqutil/Word/Properties.v b/src/coqutil/Word/Properties.v
index 3234fb95..810ca4c1 100644
--- a/src/coqutil/Word/Properties.v
+++ b/src/coqutil/Word/Properties.v
@@ -1,4 +1,5 @@
 From Coq Require Import ZArith.
+Require Import Coq.ZArith.Znumtheory.
 Require Import Coq.ZArith.Zpow_facts.
 Require Import coqutil.Z.div_mod_to_equations.
 Require Import coqutil.Z.Lia Btauto.
@@ -6,6 +7,7 @@ Require Import coqutil.Z.PushPullMod.
 Require Coq.setoid_ring.Ring_theory.
 Require Import coqutil.Z.bitblast.
 Require Import coqutil.Word.Interface. Import word.
+Require Import coqutil.Byte.
 
 Local Open Scope Z_scope.
 
@@ -767,6 +769,30 @@ Module word.
 
     Lemma mul_comm: forall x y : word, word.mul x y = word.mul y x.
     Proof. intros. ring. Qed.
+
+    Lemma byte_wrap_word_wrap: forall w,
+      8 <= width ->
+      byte.wrap (word.wrap w) = byte.wrap w.
+    Proof.
+      intros.
+      cbv [byte.wrap word.wrap].
+      rewrite <-Zmod_div_mod.
+      { reflexivity. }
+      { blia. }
+      { blia. }
+      exists (2^(width - 8)).
+      rewrite <-Z.pow_add_r by blia.
+      rewrite Z.sub_add.
+      reflexivity.
+    Qed.
+
+    Lemma byte_swrap_word_wrap: forall w,
+      8 <= width ->
+      byte.swrap (word.wrap w) = byte.swrap w.
+    Proof.
+      intros.
+      rewrite <-byte.swrap_wrap, (byte_wrap_word_wrap _ H), byte.swrap_wrap; reflexivity.
+    Qed.
   End WordConvenienceKitchenSink.
 End word.