Created
December 3, 2025 19:46
-
-
Save ngmachado/ac04ecf93e74d198e1c8b571992bcc03 to your computer and use it in GitHub Desktop.
silly example
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| const MAX_SUPPLY: u256 = 1_000_000; | |
| // storage variables with a refinement invariant on total_supply | |
| var total_supply: { s: u256 | s <= MAX_SUPPLY } @storage; | |
| var balances: mapping(address, u256) @storage; | |
| enum MintError { | |
| Overflow, | |
| ExceedsMaxSupply, | |
| } | |
| // ----------> Result monad over values (no regions here) <---------- | |
| // nice right? | |
| type Result(T, E) = | |
| | Ok(T) | |
| | Err(E); | |
| // map : Result<T,E> × (T → U) → Result<U,E> | |
| fun map(T, U, E) ( | |
| r: Result(T, E), | |
| f: fun(T) -> U, | |
| ) -> Result(U, E) { | |
| match r { // ora don't support match pattern matching yet, but this is a good example | |
| Ok(value) => Ok(f(value)), | |
| Err(e) => Err(e), | |
| } | |
| } | |
| // and_then / flatMap : Result<T,E> × (T → Result<U,E>) → Result<U,E> | |
| fun and_then(T, U, E)( | |
| r: Result(T, E), | |
| f: fun(T) -> Result(U, E), | |
| ) -> Result(U, E) { | |
| match r { | |
| Ok(value) => f(value), | |
| Err(e) => Err(e), | |
| } | |
| } | |
| // ---------- Pure helpers for arithmetic & constraints ---------- | |
| // checked addition returning a Result instead of reverting | |
| fun checked_add(a: u256, b: u256) -> Result(u256, MintError) { | |
| let c: u256 = a + b; | |
| // pretend we have some overflow check here | |
| if (c < a) { | |
| return Err(MintError.Overflow); | |
| } else { | |
| return Ok(c); | |
| } | |
| } | |
| // ensure total_supply + minted <= MAX_SUPPLY | |
| fun enforce_max_supply(total: u256, minted: u256) | |
| -> Result(u256, MintError) | |
| { | |
| // reuse checked_add, then clamp with a predicate | |
| let r: Result(u256, MintError) = checked_add(total, minted); | |
| return and_then(u256, u256, MintError)( | |
| r, | |
| fun(new_total: u256) -> Result(u256, MintError) { | |
| if (new_total <= MAX_SUPPLY) { | |
| Ok(new_total) | |
| } else { | |
| Err(MintError.ExceedsMaxSupply) | |
| } | |
| }, | |
| ); | |
| } | |
| // A tiny pure state record for balances + total | |
| struct MintState { | |
| total: u256, | |
| bal: u256, | |
| } | |
| // pure mint logic: from (total, balance, amount) to new state s -> s' | |
| // -----> All failure paths are in the Result monad <----- | |
| fun compute_mint_state( | |
| total: u256, | |
| bal: u256, | |
| amount: u256, | |
| ) -> Result(MintState, MintError) { | |
| // our silly fancy logic: inc twice = +2 | |
| fun inc(x: u256) -> u256 { x + 1 } | |
| fun apply_twice(f: fun(u256) -> u256, x: u256) -> u256 { | |
| f(f(x)) | |
| } | |
| let minted: u256 = apply_twice(inc, amount); | |
| // 1) new balance = bal + minted (checked) | |
| let bal_res: Result(u256, MintError) = checked_add(bal, minted); | |
| // 2) new total = total + minted (checked + constrained) | |
| return and_then(u256, MintState, MintError)( | |
| bal_res, | |
| fun(new_bal: u256) -> Result(MintState, MintError) { | |
| let tot_res: Result(u256, MintError) = | |
| enforce_max_supply(total, minted); | |
| and_then(u256, MintState, MintError)( | |
| tot_res, | |
| fun(new_total: u256) -> Result(MintState, MintError) { | |
| Ok(MintState{ | |
| total = new_total, | |
| bal = new_bal, | |
| }) | |
| }, | |
| ) | |
| }, | |
| ); | |
| } | |
| // ---------- Effectful boundary: we are actually touching @storage ---------- | |
| // This is where regions + side effects appear | |
| // Everything “business logic” above was pure over values, now we bring it all together and commit the state transition | |
| fn mint(to: address, amount: u256) { | |
| // snapshot current storage into @memory values | |
| let cur_total: u256 = total_supply; | |
| let cur_bal: u256 = balances[to]; | |
| // run the pure mint logic in the Result monad | |
| let res: Result(MintState, MintError) = | |
| compute_mint_state(cur_total, cur_bal, amount); | |
| match res { | |
| Ok(state) => { | |
| // only in the success branch do we touch @storage | |
| // Region transition: @memory → @storage, invariant-preserving | |
| let new_total_refined: | |
| { s: u256 | s <= MAX_SUPPLY } @memory = state.total; | |
| total_supply = new_total_refined; // storage store | |
| balances[to] = state.bal; // storage store | |
| @lock(total_supply); // no more writes this tx | |
| } | |
| Err(e) => { | |
| // Handle failure (revert, emit event, etc.) | |
| // From the type system's POV this branch has no storage writes. | |
| revert(e); | |
| } | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment