From 5f4b8ed8128b37fd300f47de29c1325cf943898f Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Tue, 15 Oct 2019 09:38:55 -0700
Subject: [PATCH] Fix test_tutorial5 (#565)

Fixes #511.
---
 doc/tutorial/code/DES.cry  |  9 +++------
 doc/tutorial/code/des3.saw | 36 ++++++++++++++++++++++++------------
 2 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/doc/tutorial/code/DES.cry b/doc/tutorial/code/DES.cry
index f477e69d27..7b2de1f2c0 100644
--- a/doc/tutorial/code/DES.cry
+++ b/doc/tutorial/code/DES.cry
@@ -7,12 +7,9 @@ module DES where
 
 import Cipher
 
-// DES API
-DES : Cipher 64 64
-DES = 
-    { encrypt key pt = des pt (expandKey key)
-    , decrypt key ct = des ct (reverse (expandKey key))
-    }
+encrypt key pt = des pt (expandKey key)
+
+decrypt key ct = des ct (reverse (expandKey key))
 
 // Encryption 
 
diff --git a/doc/tutorial/code/des3.saw b/doc/tutorial/code/des3.saw
index 7a1b6d411b..2cdca85518 100644
--- a/doc/tutorial/code/des3.saw
+++ b/doc/tutorial/code/des3.saw
@@ -1,26 +1,38 @@
-m <- cryptol_load "DES.cry";
-let enc = {{ m::DES.encrypt }};
-let dec = {{ m::DES.decrypt }};
+import "DES.cry";
 
 print "proving dec_enc...";
-let {{ prop1 key msg = dec key (enc key msg) == msg }};
-dec_enc <- prove_print do { unfolding ["enc", "dec"]; abc; } {{prop1}};
+let prop1 = {{ \key msg -> decrypt key (encrypt key msg) == msg }};
+dec_enc <- prove_print abc {{prop1}};
+
+print dec_enc;
 
 print "proving enc_dec...";
-let {{ prop2 key msg = enc key (dec key msg) == msg }};
-enc_dec <- prove_print do { unfolding ["enc", "dec"]; abc; } {{prop2}};
+let prop2 = {{ \key msg -> encrypt key (decrypt key msg) == msg }};
+enc_dec <- prove_print abc {{prop2}};
 
 print enc_dec;
 
-let ss = addsimp dec_enc (addsimp enc_dec empty_ss);
+let ss = addsimp dec_enc (addsimp enc_dec basic_ss);
 
-let {{ enc3 k1 k2 k3 msg = enc k3 (dec k2 (enc k1 msg)) }};
-let {{ dec3 k1 k2 k3 msg = dec k1 (enc k2 (dec k3 msg)) }};
+let {{ enc3 k1 k2 k3 msg = encrypt k3 (decrypt k2 (encrypt k1 msg)) }};
+let {{ dec3 k1 k2 k3 msg = decrypt k1 (encrypt k2 (decrypt k3 msg)) }};
 
 print "proving dec3_enc3...";
 let {{ prop3 k1 k2 k3 msg = dec3 k1 k2 k3 (enc3 k1 k2 k3 msg) == msg }};
-prove_print do { simplify ss; print_goal; abc; } {{prop3}};
+prove_print do {
+    unfolding ["prop3"];
+    unfolding ["dec3", "enc3"];
+    simplify ss;
+    print_goal;
+    abc;
+} {{prop3}};
 
 print "proving enc3_dec3...";
 let {{ prop4 k1 k2 k3 msg = enc3 k1 k2 k3 (dec3 k1 k2 k3 msg) == msg }};
-prove_print do { simplify ss; print_goal; abc; } {{prop4}};
+prove_print do {
+    unfolding ["prop4"];
+    unfolding ["dec3", "enc3"];
+    simplify ss;
+    print_goal;
+    abc;
+} {{prop4}};