From 0a4899d33914fc1c05cbaaca947b9e8513c6aaa4 Mon Sep 17 00:00:00 2001
From: Sanjit Bhat <sanjit.bhat@gmail.com>
Date: Tue, 19 Nov 2024 11:01:53 -0500
Subject: [PATCH] update pav code

---
 external/Goose/github_com/mit_pdos/pav/kt.v | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

diff --git a/external/Goose/github_com/mit_pdos/pav/kt.v b/external/Goose/github_com/mit_pdos/pav/kt.v
index 644753b95..c695f2cd6 100644
--- a/external/Goose/github_com/mit_pdos/pav/kt.v
+++ b/external/Goose/github_com/mit_pdos/pav/kt.v
@@ -211,10 +211,11 @@ Definition checkDig: val :=
     (if: "err0"
     then "stdErr"
     else
-      let: ("seenDig", "ok0") := MapGet "seenDigs" (struct.loadF SigDig "Epoch" "dig") in
-      (if: "ok0"
-      then
-        (if: (~ (std.BytesEqual (struct.loadF SigDig "Dig" "seenDig") (struct.loadF SigDig "Dig" "dig")))
+      (if: ((struct.loadF SigDig "Epoch" "dig") + #1) = #0
+      then "stdErr"
+      else
+        let: ("seenDig", "ok0") := MapGet "seenDigs" (struct.loadF SigDig "Epoch" "dig") in
+        (if: "ok0" && (~ (std.BytesEqual (struct.loadF SigDig "Dig" "seenDig") (struct.loadF SigDig "Dig" "dig")))
         then
           let: "evid" := struct.new Evid [
             "sigDig0" ::= "dig";
@@ -224,13 +225,6 @@ Definition checkDig: val :=
             "Evid" ::= "evid";
             "Err" ::= #true
           ]
-        else
-          struct.new ClientErr [
-            "Err" ::= #false
-          ])
-      else
-        (if: ((struct.loadF SigDig "Epoch" "dig") + #1) = #0
-        then "stdErr"
         else
           struct.new ClientErr [
             "Err" ::= #false