Fix Deed proof again

pirapira · Dec 29, 2016 · 43a7a5d · 43a7a5d
1 parent d1e0a28
commit 43a7a5d
Show file tree

Hide file tree

Showing 3 changed files with 1,242 additions and 509 deletions.
diff --git a/ContractSem.thy b/ContractSem.thy
@@ -21,6 +21,20 @@ imports Main "~~/src/HOL/Word/Word" "./Instructions" "./KEC" "./lem/Evm"
 
 begin
 
+
+(* Generated by Lem in EvmAuxiliary.thy *)
+(* termination cut_natural_map by lexicographic_order
+*)
+(*
+termination store_byte_list_memory by lexicographic_order *)
+
+termination log256floor by lexicographic_order
+
+termination word_exp by lexicographic_order
+
+
+
+
 declare vctx_advance_pc_def [simp]
 declare vctx_next_instruction_def [simp]
 declare call_def [simp]

diff --git a/README.md b/README.md
@@ -57,7 +57,7 @@ $ ./runVmTest.native
 
 ## Makefile goals
 
-* (currently not working; now fixing) `make deed` produces a verified PDF document for the Deed contract in `output/document.pdf`.
+* `make deed` produces a verified PDF document for the Deed contract in `output/document.pdf`.
 * `make doc` produces `output/document.pdf` as well as `lem/*.pdf`.
 * `make lem-thy` compiles the Lem sources into Isabelle/HOL
 * `make lem-pdf` compiles some of the Lem sources into PDF through LaTeX