From 0694f3d18ac0cf729f8a9aaf37e4d0ec2529568e Mon Sep 17 00:00:00 2001
From: PLR <51248199+plredmond@users.noreply.github.com>
Date: Thu, 21 Jul 2022 15:53:41 -0700
Subject: [PATCH 1/4] implement support for structs in munge

---
 crux-mir-comp/src/Mir/Cryptol.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs
index e083c18c66..125511f213 100644
--- a/crux-mir-comp/src/Mir/Cryptol.hs
+++ b/crux-mir-comp/src/Mir/Cryptol.hs
@@ -326,7 +326,11 @@ munge sym shp rv = do
                     W4.justPartExpr sym <$> go shp rv
                 return $ MirVector_PartialVector pv'
             MirVector_Array _ -> error $ "munge: MirVector_Array NYI"
-        -- TODO: StructShape
+        go (StructShape _ _ flds) (AnyValue tr rvs)
+            | StructRepr cr <- tr
+            , Just Refl <- testEquality (fmapFC fieldShapeType flds) cr =
+                AnyValue tr <$> goFields flds rvs
+            | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tr
         go (TransparentShape _ shp) rv = go shp rv
         -- TODO: RefShape
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"

From 07d1f942a8b77b3ecc7a332888ab5b5587903037 Mon Sep 17 00:00:00 2001
From: PLR <51248199+plredmond@users.noreply.github.com>
Date: Fri, 22 Jul 2022 14:45:54 -0700
Subject: [PATCH 2/4] test for munge-ing a struct

---
 .../test/symb_eval/comp/munge_struct.rs       | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 crux-mir-comp/test/symb_eval/comp/munge_struct.rs

diff --git a/crux-mir-comp/test/symb_eval/comp/munge_struct.rs b/crux-mir-comp/test/symb_eval/comp/munge_struct.rs
new file mode 100644
index 0000000000..25cdd7c669
--- /dev/null
+++ b/crux-mir-comp/test/symb_eval/comp/munge_struct.rs
@@ -0,0 +1,20 @@
+extern crate crucible;
+use crucible::*;
+use crucible::cryptol::munge;
+
+#[derive(Clone)]
+struct Point{
+    x: u32,
+    y: u32,
+}
+
+fn reflect(p: Point) -> Point {
+    Point{x: p.y, y: p.x}
+}
+
+#[crux_test]
+fn munge_struct_equiv_test() {
+    let (x, y) = <(u32, u32)>::symbolic("p");
+    let p2 = reflect(munge(Point{x, y}));
+    crucible_assert!(p2.x == y);
+}

From 2f37a8f3098bca6227e761e331150db75b4473b4 Mon Sep 17 00:00:00 2001
From: PLR <51248199+plredmond@users.noreply.github.com>
Date: Fri, 22 Jul 2022 14:54:19 -0700
Subject: [PATCH 3/4] adjust binders to match naming convention

---
 crux-mir-comp/src/Mir/Cryptol.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs
index 125511f213..1db880a784 100644
--- a/crux-mir-comp/src/Mir/Cryptol.hs
+++ b/crux-mir-comp/src/Mir/Cryptol.hs
@@ -326,11 +326,11 @@ munge sym shp rv = do
                     W4.justPartExpr sym <$> go shp rv
                 return $ MirVector_PartialVector pv'
             MirVector_Array _ -> error $ "munge: MirVector_Array NYI"
-        go (StructShape _ _ flds) (AnyValue tr rvs)
-            | StructRepr cr <- tr
-            , Just Refl <- testEquality (fmapFC fieldShapeType flds) cr =
-                AnyValue tr <$> goFields flds rvs
-            | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tr
+        go (StructShape _ _ flds) (AnyValue tpr rvs)
+            | StructRepr ctx <- tpr
+            , Just Refl <- testEquality (fmapFC fieldShapeType flds) ctx =
+                AnyValue tpr <$> goFields flds rvs
+            | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
         -- TODO: RefShape
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"

From 3206c46f4d4cca84efc2d31b06dcc48f078172bd Mon Sep 17 00:00:00 2001
From: PLR <51248199+plredmond@users.noreply.github.com>
Date: Fri, 22 Jul 2022 15:03:39 -0700
Subject: [PATCH 4/4] add golden file for munge test

---
 crux-mir-comp/test/symb_eval/comp/munge_struct.good | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 crux-mir-comp/test/symb_eval/comp/munge_struct.good

diff --git a/crux-mir-comp/test/symb_eval/comp/munge_struct.good b/crux-mir-comp/test/symb_eval/comp/munge_struct.good
new file mode 100644
index 0000000000..6ee4dd3406
--- /dev/null
+++ b/crux-mir-comp/test/symb_eval/comp/munge_struct.good
@@ -0,0 +1,3 @@
+test munge_struct/3a1fbbbh::munge_struct_equiv_test[0]: ok
+
+[Crux] Overall status: Valid.