Stabilise SMT the One True Way™

formosa-crypto · Dec 8, 2023 · ab5542f · ab5542f
1 parent d9e3bbc
commit ab5542f
Showing 1 changed file with 22 additions and 1 deletion.
diff --git a/sha3/proof/smart_counter/Handle.eca b/sha3/proof/smart_counter/Handle.eca
@@ -2148,8 +2148,29 @@ proof.
     conseq(:_==> Redo.prefixes{1}.[take (i{1}+1) p{1}] = Some (sa{1}, sc{1})
               /\ (take (i{1} + 1) p{1} \in Redo.prefixes{1})
               /\ (G1.bcol{2} \/ G1.bext{2}));1:smt(prefix_ge0).
-    if{1};sp;2:if{1};(if{2};2:if{2});sp;auto;5:swap{2}4-3;auto;
+    if {1}; last first.
+    + sp; if {1}; if {2}; last first.
+      + if {2}; sp; auto=> />.
+        + smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+        smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+      + auto=> />.
+        smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+      + if {2}; last first.
+        + auto=> />.
+        smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+      + swap {2} 4 -3; auto=> />.
+        smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+      auto=> />.
       smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+    if {2}.
+    + auto=> />.
+      smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+    if {2}.
+    + auto=> />.
+      smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+    auto=> />.
+    smt(get_setE mem_set DBlock.dunifin_ll DCapacity.dunifin_ll).
+
   rcondf{1}1;1:auto=>/#.
   sp;wp.
   if{1};2:rcondt{2}1;first last;3:rcondf{2}1;..3:auto.