Add number-theory related uRust examples

[ethan-kharitonov]

Description of changes: Adds some (roughly) number theory related examples of µRust programs, verified using AutoCorrode.

• Number_Theory.thy: Adds uRust programs for Fibonacci, GCD, extended GCD, Euler's totient, modular exponentiation, and a simple primality test
• .gitignore: Adds .DS_Store and .idea/ to .gitignore
• ROOT: Adds Number_Theory theory and HOL-Number_Theory session dependency

Tested: isabelle build -d . Micro_Rust_Examples.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[hanno-becker]

Using subgoals should be avoided if possible. The reason is that the result of crush is difficult to predict, including the order of subgoals. If for some reason, the order of goals changes, subgoal based proofs would not work anymore.

The style we should, where possible, promote instead is to hoist pure facts into an "Isar preamble". This makes the proof more robust and also more readable, because the essence of the argument is available in plain sight and in structured proof language. The apply-style crush proof itself should be as short as possible, and merely grind through the symbolic execution.

This comment applies to the proofs in general, and I leave it to you adjust them, but for concreteness, here's what I mean for gcd_spec:

lemma gcd_spec:
  shows ‹Γ; gcd_prog a b ⊨⇩F gcd_contract a b›
proof (crush_boot f: gcd_prog_def contract: gcd_contract_def, goal_cases)
  case 1
  ―‹Isar preamble establishing some of the verification conditions generated
     by crush's symbolic execution.›
  { fix r n m assume ‹0 < r› and ‹r ≤ Suc n›
    then have ‹m mod r ≤ n›
      using mod_less_divisor[of r m] by linarith
  }
  ―‹Symbolic execution›
  then show ?case
  apply crush_base
  subgoal for x_ref y_ref
    apply (ucincl_discharge‹
      rule_tac
        INV=‹λk. ⨆ xv yv. fully_owns x_ref xv ⋆ fully_owns y_ref yv ⋆ ⟨gcd xv yv = gcd a b ∧ yv ≤ k⟩› and
        INV'=‹λk. ⨆ xv yv. fully_owns x_ref xv ⋆ fully_owns y_ref yv ⋆ ⟨gcd xv yv = gcd a b ∧ 0 < yv ∧ yv ≤ k + 1⟩› and
        τ=‹λ_. ⟨False⟩› and
        θ=‹λ_. ⟨False⟩›
      in wp_bounded_while_framedI
    ›)
  ―‹It's a judgement call what pure logic to hoist into the preamble and what to just 'inline',
     here e.g. by adding ▩‹gcd.commute› to the simpset.›
  apply (crush_base simp add: simp add: gcd.commute)
  done
qed

Could you look through your proofs and see if you can rework them to trade subgoal chains for moreover ... chains in the preamble?

[hanno-becker]

This is a convenient abbreviation for local, unstructured references, but it becomes problematic as soon as you work with references to compound data like records: If, say, r is a reference to the field of a record, you want to say not only how that field evolves as r is modified, but also that the rest of the record does not change. For that, you need to keep the 'global' value g around and use the f·(g↓v) pattern.

Even though this is an example only, I think we should set precedent for the right pattern; could you take a look at what it would take to remove fully_owns?

[hanno-becker]

@ethan-kharitonov Thank you so much, this is a great source of additional examples -- amazing! I'd love to have this in the repository.

Before we can merge, we should slightly restructure the proofs so the essential 'pure' argument is hoisted into an Isar preamble, while the symbolic execution is reduced to a few crush calls, ideally without subgoal.