update pav code

mit-pdos · Nov 19, 2024 · 0a4899d · 0a4899d
1 parent 10d5f2a
commit 0a4899d
Showing 1 changed file with 5 additions and 11 deletions.
diff --git 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