theory week09B_demo
imports "autocorres-0.98/AutoCorres" "GCD"
begin

text {*
  To run this demo you must have the AutoCorres tool.
  This demo was tested with AutoCorres 0.98 and Isabelle2013-2

  You can download AutoCorres from 
  \url{http://ssrg.nicta.com.au/projects/TS/autocorres/}

  The following instructions assume you downloaded autocorres-0.98.tar.gz

  1. Unpack the .tar.gz file, which will create the directory autocorres-0.98
  
     tar -xzf autocorres-0.98.tar.gz

  2. To test that it builds with your Isabelle version, build the AutoCorres logic

     isabelle build -v -d autocorres-0.98 AutoCorres

  3. Load this demo theory using the AutoCorres logic

     isabelle jedit -d autocorres-0.98 -l AutoCorres week09B_demo.thy

  To parse the C file you need to have 'cpp' installed. On Linux you
  will probably already have gcc. On Mac OS, you may need to download
  the Command Line Tools. You can do this via Xcode if you have it installed.
  Or you can download standalone packages:
  \url{https://developer.apple.com/downloads/index.action?=Command%20Line%20Tools}

  Make sure the demo C file simple.c is in the same directory as this .thy file
*}

text {*
  Parse in the C file; give each function a deeply embedded semantics in
  the SIMPL language.
*}
install_C_file "simple.c"

text {*
  Use AutoCorres to give each function a (monadic) shallow embedding that
  is designed to be more easily reasoned about.

  (The ts_force_nondet option below forces AutoCorres not to type strengthen
   the gcd function. Try removing it to see type strengthening in action.
   You might also like to experiment with forcing other levels of type
   strengthening for max by adding ts_force monad=max  where monad is
   one of pure, gets, option, nondet.)
*}
autocorres [unsigned_word_abs=gcd max except, ts_force nondet=gcd] "simple.c"
text {*
   Enter the environment in which all of the C parser and AutoCorres output is placed
*} 
context simple begin

text {* 
  View the AutoCorres semantics of the max function
*}
thm max'_def

text {*
  This is its original semantics in SIMPL
*}
thm max_body_def

text {*
  The state type of the monad that AutoCorres produces is called @{typ lifted_globals}.

  It is a record containing a set of heaps, one for each pointer 
  type used in the program. Ours uses only unsigned *, i.e. 32-bit word pointers.
*}
term heap_w32
term heap_w32_update

text {*
  This is the AutoCorres semantics of the func function. Observe that it
  is very similar to the hand-written example from the last lecture.
*}
thm func'_def

text {*
  The automated tactic "wp" does autoatic rule application of the monadic
  weakest precondition style rules we saw last lecture.
*}
lemma func'_partial_wp: 
  "\<lbrace>\<lambda>s. heap_w32 s p \<ge> 10 \<and> Q () s\<rbrace> func' p \<lbrace>Q\<rbrace>"
  apply(unfold func'_def)
  apply wp 
  apply fastforce
  done

text {*
  AutoCorres gives the gcd function a semantics in the nondeterministic
  state monad with failure (from last lecture). Observe that the guard to
  check for the absence of division by zero in the SIMPL is absent from the
  state monad version, because AutoCorres can prove it isn't needed due to the
  loop condition.
*}
thm gcd'_def gcd_body_def

text {*
  AutoCorres also proves that its (monadic) abstractions of each function
  correspond to their semantics in SIMPL. In this sense AutoCorres is a
  self-certifying tool, and doesn't need to be trusted.
*}
thm gcd'_ccorres max'_ccorres func'_ccorres

lemma gcd'_correct:
  "\<lbrace>\<lambda>_. True\<rbrace> gcd' a b \<lbrace>\<lambda>r s. r = gcd a b\<rbrace>"
  apply(unfold gcd'_def)
  apply(rule hoare_weaken_pre)
   apply wp
   apply(rule_tac I="\<lambda>(x,y) s. gcd x y = gcd a b" in  whileLoop_wp)
    apply wp
    apply clarsimp
    apply (metis gcd_red_nat gcd_semilattice_nat.inf_commute)
   apply clarsimp+
  done

text {*
  AutoCorres loops can be annotated with invariants which will be used by
  the wp ruleset when doing automated proofs
*}
lemma gcd'_le:
  "\<lbrace>\<lambda>_. True\<rbrace> gcd' a b \<lbrace>\<lambda>r s. r \<le> max a b\<rbrace>"
  apply(unfold gcd'_def)
  apply(subst whileLoop_add_inv[where I="\<lambda>(x,y) s. max x y \<le> max a b"])
  apply(rule hoare_weaken_pre)
   apply wp
    apply (clarsimp)
    apply (metis le_trans  mod_le_divisor)
   apply clarsimp+
  done

text {*
  wp tends to handle most reasoning about exceptions over AutoCorres output
*}
lemma except'_result:
  "\<lbrace>\<lambda>_. True\<rbrace> except' u \<lbrace>\<lambda>r _. r \<ge> 6 \<and> r \<le> 8\<rbrace>"
  apply(unfold except'_def)
  apply(subst whileLoopE_add_inv[where I="\<lambda>(ret,u) _. u \<le> 8"])
  apply wp
    apply clarsimp
   apply clarsimp
  apply simp
  apply wp
  done

end (* context simple *)
end