Theory Micro_Rust_Examples.Showcase

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Showcase
  imports
    Micro_Rust_Std_Lib.StdLib_All
begin
(*>*)

section‹AutoCorrode showcase›

text‹This file contains a concise showcase of some of AutoCorrode's verification infrastructure.
We start with below '▩‹locale›'. This is some boilerplate that you can ignore for now:
it is responsible for making various types available as being mutable and allocatable.›
locale showcase_ctx =
    reference reference_types +
    ― ‹Import ▩‹reference_allocatable› so we can allocate references for ▩‹64 word›.›
    ref_word64: reference_allocatable reference_types _ _ _ _ _ _ _ word64_prism +
    ref_nat: reference_allocatable reference_types _ _ _ _ _ _ _ nat_prism +
    ref_bool: reference_allocatable reference_types _ _ _ _ _ _ _ bool_prism
  for 
  reference_types :: ‹'s::{sepalg} ⇒ 'addr ⇒ 'gv ⇒ 'abort ⇒ 'i prompt ⇒ 'o prompt_output ⇒ unit›
  ― ‹Ignore for now›
  and word64_prism :: ‹('gv, 64 word) prism›
  and bool_prism :: ‹('gv, bool) prism›
  and nat_prism :: ‹('gv, nat) prism›
begin

adhoc_overloading store_reference_const ⇌ ref_word64.new
adhoc_overloading store_reference_const ⇌ ref_nat.new
adhoc_overloading store_reference_const ⇌ ref_bool.new
adhoc_overloading store_update_const ⇌ update_fun
text‹That was it for the boilerplate, now we can proceed with verifying some Rust!›

text‹This first example relies on local mutable variables. The syntax is eyeball-close
to Rust: this is a dialect of Rust we call uRust. uRust is shallowly embedded in
Isabelle/HOL, so we can 'escape' the uRust syntax if needed or convenient.
This is done here with ▩‹⟪_⟫›, used in this example for providing type annotations.›
definition ref_test where ‹ref_test ≡ FunctionBody ⟦
    let mut nat_ref = ⟪0 :: nat⟫;
    let mut bool_ref = ⟪False :: bool⟫;
    if *bool_ref {
      nat_ref = 42;
    } else {
      nat_ref = 12;
    };
    *nat_ref
  ⟧›

text‹For more in-depth details on uRust (including ways to symbolically evaluate it),
see 🗏‹Basic_Micro_Rust.thy›.›

text‹We can now write down the specification or ∗‹contract› of this function:
it should always return \<^term>‹12 :: nat›. However, executing this functions requires
the allocation of local mutables. Owning the \<^term>‹can_alloc_reference› resource makes
sure that we have the capability to do this.
Note also the embedding of a pure fact ▩‹r = 12› into separation logic via the
▩‹⟨_⟩› antiquotation.›
definition ref_test_contract where
  ‹ref_test_contract ≡
     let pre  = can_alloc_reference in
     let post = λr. can_alloc_reference ⋆ ⟨r = 12⟩ in
     make_function_contract pre post›
text‹The ▩‹ucincl_auto› command is necessary boilerplate for every contract, ignore for now.›
ucincl_auto ref_test_contract

text‹Now we prove that the function satisfies the contract!›
lemma ref_test_spec:
  shows ‹Γ; ref_test ⊨⇩F ref_test_contract›
― ‹▩‹crush_boot› unfolds function and contract, and turns the satisfies contract goal ▩‹⊨⇩F›
into a symbolic execution goal ▩‹Δ ⊢ WP e _› in weakest-precondition style.›
  apply (crush_boot f: ref_test_def contract: ref_test_contract_def)
― ‹▩‹crush_base› calls the automation, which fully automatically proves this goal›
  apply crush_base
  done

text‹Let's make this a bit more interesting, and verify the classic ▩‹swap› function›
definition swap_ref :: ‹('addr, 'gv, 'v) ref ⇒ ('addr, 'gv, 'v) ref ⇒ ('s, unit, 'abort, 'i prompt, 'o prompt_output) function_body› where
  ‹swap_ref rA rB ≡ FunctionBody ⟦
     let oldA = *rA;
     let oldB = *rB;
     rA = oldB;
     rB = oldA;
  ⟧›

text‹The contract of \<^term>‹swap_ref› might differ slightly from what you'd expect, specifically
in the arguments of the points-to connective ▩‹↦›. \<^term>‹l ↦⟨s⟩ g↓v› describes the resource where we
partially own (indicated by share \<^term>‹s :: share›) a location \<^term>‹l :: ('addr, 'gv, 'v) ref› that
points to a 'global' value \<^term>‹g :: 'gv›, which we currently read/interpret as a value
\<^term>‹v :: 'v›. You can think of \<^term>‹g :: 'gv› being a bitwise representation of an actual
value \<^term>‹v :: 'v›, where \<^term>‹g :: 'gv› might comprise bitfields for other values. Writing
to this location will only change the bits related to \<^term>‹v :: 'v›, while the rest remain the same.
This effect is captured with the \<^term>‹l ↦⟨s⟩ (λ_. w) · (g↓v)› resource, which describes that
we (partially) own a location \<^term>‹l› that points to a 'global' value \<^term>‹g›, but field \<^term>‹v›
of that global value has been overwritten with new content \<^term>‹w›.›
definition swap_ref_contract :: ‹('addr, 'gv, 'v) ref ⇒ ('addr, 'gv, 'v) ref ⇒ 'gv ⇒ 'gv ⇒ 'v ⇒ 'v ⇒ ('s, 'a, 'b) function_contract› where
  ‹swap_ref_contract lref rref lg rg lval rval ≡
    let pre  = lref ↦⟨⊤⟩ lg↓lval ⋆ rref ↦⟨⊤⟩ rg↓rval in
    let post = λ _.
               lref ↦⟨⊤⟩ (λ_. rval) · (lg↓lval) ⋆
               rref ↦⟨⊤⟩ (λ_. lval) · (rg↓rval) in
    make_function_contract pre post›
ucincl_auto swap_ref_contract

text‹Proving this specification is as straightforward as before›
lemma swap_ref_spec:
  shows ‹Γ; swap_ref lref rref ⊨⇩F swap_ref_contract lref rref lg rg lval rval›
  apply (crush_boot f: swap_ref_def contract: swap_ref_contract_def)
  apply crush_base
  done

text‹Now, let's use this function in some client program›
definition swap_client where
  ‹swap_client ≡ FunctionBody ⟦
    let mut left = ⟪42 :: nat⟫;
    let mut right = 72;
    swap_ref(left, right);
    *left
  ⟧›

text‹After swapping, the variable left should now contain the value \<^term>‹72 :: nat››
definition swap_client_contract where
  ‹swap_client_contract ≡
    let pre  = can_alloc_reference in
    let post = λ r. ⟨r = (72 :: nat)⟩ ⋆ can_alloc_reference in
    make_function_contract pre post›
ucincl_auto swap_client_contract

text‹We can verify this in two ways. Firstly, we can tell the automation to use the verified
specification of \<^term>‹swap_ref›, using the ▩‹specs add:› and ▩‹contracts add:› modifiers›
lemma swap_client_spec_using_swap_spec:
  shows ‹Γ; swap_client ⊨⇩F swap_client_contract›
  apply (crush_boot f: swap_client_def contract: swap_client_contract_def)
  apply (crush_base specs add: swap_ref_spec contracts add: swap_ref_contract_def )
  done

text‹Alternatively, we can just choose to inline/unfold \<^term>‹swap_ref›, and symbolically execute.›
lemma swap_client_inline_spec:
  shows ‹Γ; swap_client  ⊨⇩F swap_client_contract›
  apply (crush_boot f: swap_client_def contract: swap_client_contract_def)
  apply (crush_base inline: swap_ref_def)
  done

text‹For more details about the automation tactics like ▩‹crush_base› and ▩‹crush_boot›,
see 🗏‹Crush_Examples.thy›.›


text‹We will now verify a slightly more involved example, summing the contents of an array.
For simplicity, we will work with an array of natural numbers, to avoid possible overflow problems.›

text‹Adding two mathematical numbers of \<^typ>‹nat› is not allowed in uRust by default, so we need to
register the addition operator first. The next command takes care of that, this can be ignored. ›
adhoc_overloading urust_add ⇌ ‹bind2 (lift_exp2 (plus :: nat ⇒ nat ⇒ nat))›

text‹We can now define this summing operation of an array in uRust.
Note also the availability of indexing notation ▩‹nums[i]› for arrays.›
definition sum_array :: ‹(nat, 'a::len) array ⇒ 64 word ⇒ ('s, nat, 'abort, 'i prompt, 'o prompt_output) function_body› where
  ‹sum_array nums l ≡ FunctionBody ⟦
    let mut sum = ⟪0 :: nat⟫;
    for i in 0..l {
      let num = nums[i];
      sum = *sum + num;
    };
    *sum
  ⟧›

text‹The contract for \<^term>‹sum_array›: the stateful implementations returns the same value
as the functional implementation that uses \<^term>‹sum_list››
definition sum_array_contract :: ‹(nat, 'a::len) array ⇒ 64 word ⇒ ('s, nat, 'b) function_contract› where
  ‹sum_array_contract nums l ≡
    let pre  = can_alloc_reference ⋆ ⟨unat l = LENGTH('a)⟩ in
    let post = λ r.
               ⟨r = sum_list (array_to_list nums)⟩ ⋆ can_alloc_reference in
    make_function_contract pre post›
ucincl_auto sum_array_contract

text‹The proof of the specification is a bit more involved, since we need to deal with the loop›
lemma sum_spec:
  shows ‹Γ; sum_array nums l ⊨⇩F sum_array_contract nums l›
proof (crush_boot f: sum_array_def contract: sum_array_contract_def, goal_cases)
  case 1
― ‹We follow the Isar ▩‹moreover› .. ▩‹ultimately› pattern, first gathering required facts.
This first fact relates the partial sums from before and after executing the loop body.›
  moreover have ‹⋀ i. i < LENGTH('a) ⟹ sum_list (take (Suc i) (array_to_list nums)) = sum_list (take i (array_to_list nums)) + array_nth nums i›
    by (simp add: take_Suc_conv_app_nth)
― ‹Second fact asserts that \<^term>‹l› is bounded (since it is a \<^typ>‹64 word›). This boundedness
condition comes arises from using an ▩‹i ∈ 0..l› to index into \<^term>‹nums›.›
  moreover note More_Word.unat_lt2p[of l]
  ultimately show ?case
― ‹We can now start the proof. The first call to ▩‹crush_base› symbolically executes up until
the start of the loop.›
    apply crush_base
― ‹Some reference sum has been allocated in the mean time: give it a name with ▩‹subgoal›,
so that we can reference it in the loop invariant.›
    subgoal for sum_ref
― ‹Now, apply the rule for proving for-loops. The ▩‹INV=‹λ _ i. …›› states the loop-invariant
that we will use in the proof to verify our specification. The ▩‹τ=…› and ▩‹θ=…› refer to
conditions for raising exceptions or returning early while inside the loop body. Making these
equal to \<^term>‹λ_. ⟨False⟩› ensures that raising an exception or returning early is illegal,
like we would expect.›
      apply (ucincl_discharge‹
        rule_tac 
          INV=‹λ_ i. ⨆ g. sum_ref ↦⟨⊤⟩ g↓(sum_list (take i (array_to_list nums)))› and 
          τ=‹λ_. ⟨False⟩› and
          θ=‹λ_. ⟨False⟩›
        in wp_raw_for_loop_framedI'
      ›)
― ‹We are left with two subgoals:
- The first subgoal states that our current state entails the loop invariant after 0 iterations,
and that the loop invariant after all iterations entails our postcondition.
- The second subgoal states that executing the loop body is safe, given that the loop invariant
after n iterations holds. Moreover, the loop invariant after (n+1) iterations holds after execution
of the loop body has finished.
In this case, the automation requires one extra simplification rule to be able to finish the proof›
      by (crush_base simp add: More_Word.unat_of_nat_eq)
  done
qed

section‹Further reading›
text‹This file did not further discuss the ▩‹locale›/▩‹context› incantations
at the start of the file. To learn more about that, see 🗏‹Reference_Examples.thy›.
›

(*<*)
end
end
(*>*)