Merge branch 'master' into dispatcher_ex_mbegel

Conflicts:
	EvmFacts.thy

.gitignore

@@ -1,6 +1,14 @@
 *~
 *#
 *.bak
+*.out2
+julia/julia.ml
+julia/parsr.ml
+julia/parsr.mli
+julia/*.native
+julia/*.thy
+julia/_build
+julia/lem
 lem/*.vo
 lem/*.d
 lem/*.glob

.travis.yml

@@ -1,12 +1,11 @@
 dist: trusty
 cache:
   directories:
-  - $HOME/.isabelle
   - $HOME/.opam
 sudo: required
 before_install:
 - sudo apt-get -qq update
-- sudo apt-get -qq install libgmp3-dev
+- sudo apt-get -qq install libgmp3-dev texlive-latex-recommended
 # - git clone https://github.com/polyml/polyml.git
 # - cd polyml
 # - git checkout v5.6
@@ -22,7 +21,7 @@ before_install:
 - opam init -y --comp=4.04.1
 - eval `opam config env`
 - opam update
-- opam install -y ocamlbuild ocamlfind batteries yojson bignum easy-format bisect_ppx zarith depext sha
+- opam install -y ocamlbuild ocamlfind batteries yojson bignum easy-format bisect_ppx zarith depext sha menhir
 - git clone https://github.com/mrsmkl/ECC-OCaml.git ECC-OCaml
 - cd ECC-OCaml/src
 - make depend
@@ -34,9 +33,9 @@ before_install:
 - make || echo "failure expected"
 - cd ..
 - export PATH=./lemdir:$PATH
-- wget https://isabelle.in.tum.de/dist/Isabelle2016-1_app.tar.gz
-- tar xf Isabelle2016-1_app.tar.gz
-- export PATH=./Isabelle2016-1/bin:$PATH
+- wget https://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz
+- tar xf Isabelle2017_app.tar.gz
+- export PATH=./Isabelle2017/bin:$PATH
 # - git clone git://github.com/HOL-Theorem-Prover/HOL.git
 # - cd HOL
 # - echo 'val polymllibdir = "/usr/local/lib"' > tools-poly/poly-includes.ML
@@ -48,11 +47,17 @@ script:
 - make lem-thy
 - make lem-hol
 - make lem-coq
+- make lem-julia
+- cd julia
+- make test
+- cd -
 # - cd lem
 # - ../HOL/bin/Holmake evmTheory.uo
 # - cd -
 - cd tester
 - sh compile.sh
 - ./runVmTest.native 89
 - cd -
-- make light-isabelle
+- isabelle version
+- make simplewallet
+

ContractSem.thy

@@ -16,7 +16,7 @@
 
 theory ContractSem
 
-imports Main "~~/src/HOL/Word/Word" "./lem/Evm"
+imports Main "HOL-Word.Word" "./lem/Evm"
 (* If ./lem/Evm is missing, try executing `make lem-thy` *)
 
 begin

EvmFacts.thy

@@ -26,7 +26,6 @@ lemmas gas_simps = Gverylow_def Glow_def Gmid_def Gbase_def Gzero_def Glogtopic_
     Cgascap_def Cextra_def Gnewaccount_def Cxfer_def Cnew_def
     Gcall_def Gcallvalue_def Csstore_def Csuicide_def
 
-
 lemma log256floor_ge_0:
   "0 \<le> log256floor s"
   apply (induct s rule: log256floor.induct)

GlobalTriple.thy

@@ -13,16 +13,16 @@ datatype global_element =
 
 type_synonym global_pred = "global_element set \<Rightarrow> bool"
 
-definition state_as_set :: "(address \<Rightarrow> account) \<Rightarrow> global_element set" where
-"state_as_set st = {AccountStorage a p e | a p e. e = account_storage0 (st a) p}"
+definition state_as_set :: "(address \<Rightarrow> block_account) \<Rightarrow> global_element set" where
+"state_as_set st = {AccountStorage a p e | a p e. e = block_account_storage (st a) p}"
 
-definition backup_as_set :: "(address \<Rightarrow> account) \<Rightarrow> global_element set" where
-"backup_as_set st = {BackupStorage a p e | a p e. e = account_storage0 (st a) p}"
+definition backup_as_set :: "(address \<Rightarrow> block_account) \<Rightarrow> global_element set" where
+"backup_as_set st = {BackupStorage a p e | a p e. e = block_account_storage (st a) p}"
 
-definition sstorage_as_set :: "nat \<Rightarrow> (address \<Rightarrow> account) \<Rightarrow> global_element set" where
-"sstorage_as_set n st = {SavedStorage n a p e | a p e. e = account_storage0 (st a) p}"
+definition sstorage_as_set :: "nat \<Rightarrow> (address \<Rightarrow> block_account) \<Rightarrow> global_element set" where
+"sstorage_as_set n st = {SavedStorage n a p e | a p e. e = block_account_storage (st a) p}"
 
-definition saved_as_set :: "nat \<Rightarrow> (address\<Rightarrow>account) \<Rightarrow> constant_ctx \<Rightarrow>
+definition saved_as_set :: "nat \<Rightarrow> (address\<Rightarrow>block_account) \<Rightarrow> constant_ctx \<Rightarrow>
   variable_ctx \<Rightarrow> stack_hint \<Rightarrow> global_element set" where
 "saved_as_set n st c v hint =
     sstorage_as_set n st \<union> SavedState n ` contexts_as_set v c"
@@ -40,9 +40,9 @@ fun global_as_set :: "global_state \<Rightarrow> global_element set" where
     backup_as_set (g_orig g) \<union>
     saved_stack_as_set (g_stack g)"
 
-fun iter :: "nat \<Rightarrow> global_state \<Rightarrow> global_state" where
-"iter 0 x = x"
-| "iter (Suc n) x = next0 (iter n x)"
+fun iter :: "network \<Rightarrow> nat \<Rightarrow> global_state \<Rightarrow> global_state" where
+"iter net 0 x = x"
+| "iter net (Suc n) x = step net (iter net n x)"
 
 fun good_context :: "global_state \<Rightarrow> bool" where
 "good_context (Continue g) = no_assertion (g_cctx g)"

Hoare/Hoare.thy

@@ -5,7 +5,6 @@ imports Main
  "../sep_algebra/EvmSep"
  "../sep_algebra/Sep_Tactics"
  "~~/src/HOL/Eisbach/Eisbach"
- "../attic/Apply_Trace_Cmd"
 begin
 
 lemma not_at_least_one :

Hoare/HoareTripleForInstructions.thy

@@ -1307,22 +1307,21 @@ lemma sep_action_sep :
 
 lemma iota0_non_empty_aux:
   "\<forall> b x len lst a.
-    len \<le> l \<longrightarrow>
+    len \<le> l \<longrightarrow>                     
     iota0 b len (lst @ [a]) = a # iota0 b len lst"
-apply(induction l)
- apply(simp add: iota0.simps)
-apply(auto simp add: iota0.simps)
-apply(case_tac "len = Suc l")
- apply clarsimp
- apply(simp add: iota0.simps)
- apply(drule_tac x = "b + 1" in spec)
- apply(drule_tac x = l in spec)
- apply simp
- apply(drule_tac x = "b # lst" in spec)
- apply(drule_tac x = "a" in spec)
- apply simp
-apply simp
-done
+  apply(induction l)
+    apply(simp add: iota0.simps)
+  apply(simp add: iota0.simps)
+  apply(rule allI)
+  apply(rule allI)
+  apply(case_tac "len = Suc l"; auto)
+  apply(drule_tac x = "b + 1" in spec)
+  apply(drule_tac x = l in spec)
+  apply simp
+  apply(drule_tac x = "b # lst" in spec)
+  apply(drule_tac x = "a" in spec)
+  by(simp add: iota0.simps)  
+
 
 lemma iota0_non_empty_aux':
   "\<forall> b x len lst a l.
@@ -1386,13 +1385,9 @@ apply(simp add:cut_memory_aux.simps)
 
 apply(simp add:cut_memory_aux.simps)
 apply(cases "unat (n + 1)")
-apply(simp)
+  apply(simp)
 apply(subst (asm) my_unat_suc)
-apply(simp add:cut_memory_aux.simps)
-apply(auto)
-apply(subst cut_memory_aux)
-apply(auto)
-done
+by(auto simp add:cut_memory_aux.simps)
 
 lemma cut_memory_tail:
   "cut_memory b (n + 1) m = a # lst \<Longrightarrow> cut_memory (b + 1) n m = lst"

Hoare/HoareTripleForInstructions2.thy

@@ -120,10 +120,9 @@ lemma iszero_gas_triple :
                        gas_pred (g - Gverylow) **
                        continuing
                       )"
-  apply (clarsimp simp add: triple_def)
+  apply (auto simp add: triple_def)
   apply(rule_tac x = 1 in exI)
-  apply clarsimp
-  apply(clarsimp simp add: program_sem.simps)
+  apply(simp add: program_sem.simps)
   apply(case_tac presult;  (solves \<open>(hoare_sep sep: evm_sep simp:   stateelm_means_simps dest: stateelm_dest)\<close>)?)
   apply clarsimp
   apply(hoare_sep sep: evm_sep 
@@ -132,8 +131,8 @@ lemma iszero_gas_triple :
                    dest: advance_pc_inc_but_stack
                   split:if_split_asm)
   apply (drule advance_pc_inc_but_stack)
-  apply (simp add: image_def)
-  apply (simp  add: triv_if_eq advance_pc_stack_oblivious)
+    apply (simp add: image_def)
+  apply (simp add: triv_if_eq advance_pc_stack_oblivious)
   apply(erule_tac P=rest in back_subst)
   apply simp
   apply(rename_tac presult t)           

Hoare/HoareTripleForLogGasCall.thy

@@ -86,7 +86,7 @@ apply(rule Set.equalityI)
  apply(simp add: gasprice_advance_pc)
 apply auto
 apply(rename_tac elm; case_tac elm; simp)
-apply(case_tac "length (vctx_logs x1) \<le> fst x5"; auto)
+apply auto
 done
 
 lemma imp_to_disjD: "P \<longrightarrow> Q \<Longrightarrow> \<not>P \<or> Q"