From fbd7e21ce75200a7671d0359b19a1e956295a8b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=96rs=20Nagy?= Date: Sat, 10 Oct 2026 10:11:15 +0200 Subject: [PATCH 1/2] Micro_Rust_Examples: Verify iterative Fibonacci MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a Micro Rust function that computes Fibonacci numbers with two mutable `nat` accumulators. Its contract returns `fib (unat n)`, and the loop invariant relates the accumulators to consecutive Fibonacci values. Import the theory from `Micro_Rust_Examples`. Signed-off-by: Örs Nagy --- Micro_Rust_Examples/Fibonacci_Iterative.thy | 87 +++++++++++++++++++++ Micro_Rust_Examples/Micro_Rust_Examples.thy | 1 + 2 files changed, 88 insertions(+) create mode 100644 Micro_Rust_Examples/Fibonacci_Iterative.thy diff --git a/Micro_Rust_Examples/Fibonacci_Iterative.thy b/Micro_Rust_Examples/Fibonacci_Iterative.thy new file mode 100644 index 00000000..3ac45fa9 --- /dev/null +++ b/Micro_Rust_Examples/Fibonacci_Iterative.thy @@ -0,0 +1,87 @@ +theory Fibonacci_Iterative + imports Micro_Rust_Std_Lib.StdLib_All +begin + +locale fibonacci_ctx = + reference reference_types + + ref_word64: reference_allocatable reference_types _ _ _ _ _ _ _ word64_prism + + ref_nat: reference_allocatable reference_types _ _ _ _ _ _ _ nat_prism + for + reference_types :: \'s::{sepalg} \ 'addr \ 'gv \ 'abort \ 'i prompt \ 'o prompt_output \ unit\ + + and word64_prism :: \('gv, 64 word) 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_update_const \ update_fun +adhoc_overloading urust_add \ \bind2 (lift_exp2 (plus :: nat \ nat \ nat))\ + +section\Iterative Fibonacci Function\ + +text\This example demonstrates an iterative Fibonacci function implementation +with a complete correctness proof. We verify that the implementation matches +the mathematical definition of Fibonacci numbers.\ + +subsection\Mathematical Specification\ + +text\First, we define the mathematical Fibonacci function recursively. +Solution taken from: https://isabelle.in.tum.de/library/HOL/HOL-Number_Theory/Fib.html \ + +fun fib :: \nat \ nat\ where + fib0: \fib 0 = 0\ | + fib1: \fib (Suc 0) = 1\ | + fib2: \fib (Suc (Suc n)) = fib (Suc n) + fib n\ + +lemma fib_plus_2: + shows \fib (n + 2) = fib (n + 1) + fib n\ + by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3)) + +subsection\Iterative Implementation\ + +text\Implementation of an iterative version in Micro Rust that computes +the nth Fibonacci number efficiently without recursion.\ + +definition fib_iterative :: \64 word \ (_, nat, _, _, _) function_body\ where + \fib_iterative n \ FunctionBody \ + let mut a = \0 :: nat\; + let mut b = \1 :: nat\; + for i in 0..n { + let temp = *a + *b; + a = *b; + b = temp + }; + *a + \\ + +text\Contract specification and correctness proof for the iterative Fibonacci function.\ + +definition fib_correct_contract :: \64 word \ ('s, nat, 'b) function_contract\ where + \fib_correct_contract n \ + let pre = can_alloc_reference in + let post = \r. \r = fib (unat n)\ \ can_alloc_reference in + make_function_contract pre post\ +ucincl_auto fib_correct_contract + +lemma fib_correct_spec: + shows \\; fib_iterative n \\<^sub>F fib_correct_contract n\ +proof (crush_boot f: fib_iterative_def contract: fib_correct_contract_def, goal_cases) + case 1 + then show ?case + apply crush_base + subgoal for a_ref b_ref + apply (ucincl_discharge\ + rule_tac + INV=\\_ i. \ ga gb. a_ref \\\\ ga\(fib i) \ b_ref \\\\ gb\(fib (i + 1))\ + and \=\\_. \False\\ + and \=\\_. \False\\ + in wp_raw_for_loop_framedI' + \) + apply (crush_base simp add: fib_plus_2) + done + done +qed + +end +end diff --git a/Micro_Rust_Examples/Micro_Rust_Examples.thy b/Micro_Rust_Examples/Micro_Rust_Examples.thy index 33d3e514..6bc27feb 100644 --- a/Micro_Rust_Examples/Micro_Rust_Examples.thy +++ b/Micro_Rust_Examples/Micro_Rust_Examples.thy @@ -6,6 +6,7 @@ theory Micro_Rust_Examples Basic_Micro_Rust Common_Pitfalls Crush_Examples + Fibonacci_Iterative Pullback_Example Linked_List Linked_List_Executable_Heap From 5c5617962c657a4112244f6bed503e59ac66f4b3 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 8 Sep 2026 08:43:33 +0000 Subject: [PATCH 2/2] Micro_Rust_Examples: Add Fibonacci license header Add the standard copyright and SPDX header to the new iterative Fibonacci theory. Remove the three trailing spaces reported by `git diff --check`. The definitions and proof are unchanged. Signed-off-by: Hanno Becker --- Micro_Rust_Examples/Fibonacci_Iterative.thy | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Micro_Rust_Examples/Fibonacci_Iterative.thy b/Micro_Rust_Examples/Fibonacci_Iterative.thy index 3ac45fa9..1bd0e042 100644 --- a/Micro_Rust_Examples/Fibonacci_Iterative.thy +++ b/Micro_Rust_Examples/Fibonacci_Iterative.thy @@ -1,3 +1,6 @@ +(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + SPDX-License-Identifier: MIT *) + theory Fibonacci_Iterative imports Micro_Rust_Std_Lib.StdLib_All begin @@ -6,7 +9,7 @@ locale fibonacci_ctx = reference reference_types + ref_word64: reference_allocatable reference_types _ _ _ _ _ _ _ word64_prism + ref_nat: reference_allocatable reference_types _ _ _ _ _ _ _ nat_prism - for + for reference_types :: \'s::{sepalg} \ 'addr \ 'gv \ 'abort \ 'i prompt \ 'o prompt_output \ unit\ and word64_prism :: \('gv, 64 word) prism\ @@ -34,7 +37,7 @@ fun fib :: \nat \ nat\ where fib1: \fib (Suc 0) = 1\ | fib2: \fib (Suc (Suc n)) = fib (Suc n) + fib n\ -lemma fib_plus_2: +lemma fib_plus_2: shows \fib (n + 2) = fib (n + 1) + fib n\ by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3)) @@ -72,7 +75,7 @@ proof (crush_boot f: fib_iterative_def contract: fib_correct_contract_def, goal_ apply crush_base subgoal for a_ref b_ref apply (ucincl_discharge\ - rule_tac + rule_tac INV=\\_ i. \ ga gb. a_ref \\\\ ga\(fib i) \ b_ref \\\\ gb\(fib (i + 1))\ and \=\\_. \False\\ and \=\\_. \False\\