Skip to content

Add verified µRust examples#211

Closed
ethan-kharitonov wants to merge 3 commits into
awslabs:mainfrom
ethan-kharitonov:micro-rust-examples
Closed

Add verified µRust examples#211
ethan-kharitonov wants to merge 3 commits into
awslabs:mainfrom
ethan-kharitonov:micro-rust-examples

Conversation

@ethan-kharitonov
Copy link
Copy Markdown

@ethan-kharitonov ethan-kharitonov commented Apr 26, 2026

Description of changes: Adds some more examples of µRust programs, verified using AutoCorrode.

  • Number_Theory.thy: Fibonacci, GCD, extended GCD, Euler's totient, modular exponentiation, and a simple primality test
  • FSet_Ref.thy: Reference-backed finite sets
  • Stack.thy: Linked-list backed stack
  • Graph.thy: Finite directed graphs with verified depth-first search

(Also adds .DS_Store to .gitignore. .DS_Store is a hidden macOS Finder settings file.)

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 hanno-becker self-assigned this Apr 27, 2026
@ethan-kharitonov
Copy link
Copy Markdown
Author

Splitting into smaller PRs for easier review: #212, #213, #214. Will create another PR for the Graph example once FSet and Stack are merged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants