Created
February 14, 2026 22:38
-
-
Save ngmachado/63e3fb7278b2f86325c1b918894ef26b to your computer and use it in GitHub Desktop.
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
| // ERC20-style token that combines: | |
| // 1) bitfields for compact configuration/account metadata, | |
| // 2) comptime values, | |
| // 3) generic helpers + generic struct instantiation. | |
| bitfield TokenFlags : u256 { | |
| initialized: bool; | |
| paused: bool; | |
| mint_enabled: bool; | |
| burn_enabled: bool; | |
| decimals: u8; | |
| version: u8; | |
| } | |
| bitfield AccountFlags : u256 { | |
| frozen: bool; | |
| has_kyc: bool; | |
| privileged: bool; | |
| nonce: u16; | |
| } | |
| contract ERC20BitfieldComptimeGenerics { | |
| struct TransferBook(comptime T: type) { | |
| amount: T; | |
| sender_before: T; | |
| recipient_before: T; | |
| } | |
| storage var token_flags: TokenFlags; | |
| storage var total_supply: u256; | |
| storage balances: map<address, u256>; | |
| storage allowances: map<address, map<address, u256>>; | |
| storage account_flags: map<address, AccountFlags>; | |
| log Transfer(from: address, to: address, amount: u256); | |
| log Approval(owner: address, spender: address, amount: u256); | |
| fn add(comptime T: type, a: T, b: T) -> T { | |
| return a + b; | |
| } | |
| fn sub(comptime T: type, a: T, b: T) -> T { | |
| return a - b; | |
| } | |
| fn ct(comptime T: type, comptime value: T) -> T { | |
| return value; | |
| } | |
| pub fn init(initial_supply: u256) { | |
| let deployer: NonZeroAddress = std.msg.sender(); | |
| total_supply = initial_supply; | |
| balances[deployer] = initial_supply; | |
| let f: TokenFlags = .{ | |
| .initialized = true, | |
| .paused = false, | |
| .mint_enabled = true, | |
| .burn_enabled = true, | |
| .decimals = ct(u8, 18), | |
| .version = ct(u8, 1), | |
| }; | |
| token_flags = f; | |
| let a: AccountFlags = .{ | |
| .frozen = false, | |
| .has_kyc = true, | |
| .privileged = true, | |
| .nonce = ct(u16, 1), | |
| }; | |
| account_flags[deployer] = a; | |
| log Transfer(std.constants.ZERO_ADDRESS, deployer, initial_supply); | |
| } | |
| pub fn decimals() -> u8 { | |
| let f: TokenFlags = token_flags; | |
| return f.decimals; | |
| } | |
| pub fn isPaused() -> bool { | |
| let f: TokenFlags = token_flags; | |
| return f.paused; | |
| } | |
| pub fn setPaused(next: bool) { | |
| let f: TokenFlags = token_flags; | |
| f.paused = next; | |
| token_flags = f; | |
| } | |
| pub fn balanceOf(owner: address) -> u256 { | |
| return balances[owner]; | |
| } | |
| pub fn allowance(owner: address, spender: address) -> u256 { | |
| return allowances[owner][spender]; | |
| } | |
| pub fn approve(spender: NonZeroAddress, amount: u256) -> bool { | |
| let owner: address = std.msg.sender(); | |
| allowances[owner][spender] = amount; | |
| log Approval(owner, spender, amount); | |
| return true; | |
| } | |
| pub fn transfer(to: NonZeroAddress, amount: MinValue<u256, 1>) -> bool { | |
| let sender: NonZeroAddress = std.msg.sender(); | |
| let sender_before: u256 = balances[sender]; | |
| if (sender_before < amount) { | |
| return false; | |
| } | |
| let recipient_before: u256 = balances[to]; | |
| let book = TransferBook(u256) { | |
| amount: amount, | |
| sender_before: sender_before, | |
| recipient_before: recipient_before, | |
| }; | |
| balances[sender] = sub(u256, book.sender_before, book.amount); | |
| balances[to] = add(u256, book.recipient_before, book.amount); | |
| let meta: AccountFlags = account_flags[sender]; | |
| meta.nonce = meta.nonce + 1; | |
| account_flags[sender] = meta; | |
| log Transfer(sender, to, amount); | |
| return true; | |
| } | |
| pub fn transferFrom(from: NonZeroAddress, to: NonZeroAddress, amount: MinValue<u256, 1>) -> bool { | |
| let spender: NonZeroAddress = std.msg.sender(); | |
| let current_allowance: u256 = allowances[from][spender]; | |
| if (current_allowance < amount) { | |
| return false; | |
| } | |
| let sender_balance: u256 = balances[from]; | |
| if (sender_balance < amount) { | |
| return false; | |
| } | |
| allowances[from][spender] = sub(u256, current_allowance, amount); | |
| balances[from] = sub(u256, sender_balance, amount); | |
| let recipient_balance: u256 = balances[to]; | |
| balances[to] = add(u256, recipient_balance, amount); | |
| log Transfer(from, to, amount); | |
| return true; | |
| } | |
| pub fn mint(to: NonZeroAddress, amount: MinValue<u256, 1>) -> bool { | |
| let f: TokenFlags = token_flags; | |
| if (f.mint_enabled == false) { | |
| return false; | |
| } | |
| total_supply = add(u256, total_supply, amount); | |
| let balance: u256 = balances[to]; | |
| balances[to] = add(u256, balance, amount); | |
| log Transfer(std.constants.ZERO_ADDRESS, to, amount); | |
| return true; | |
| } | |
| } |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
SMT reported that is the companion for auditors
SMT Encoding Report
1. Run Metadata
ora-example/apps/erc20_bitfield_comptime_generics.ora1771155094basictruetruetrue600002. Summary
2722500008true083. Query Kind Counts
6500884. Findings
Diagnostic 1
guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:totransferv_40178867904 = #x0000000000000000000000000000000000000000Diagnostic 2
guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amounttransferv_40178867952 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178867904 = #xffffffffffffffffffffffffffffffffffffffffDiagnostic 3
guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:tomintv_40178868288 = #x0000000000000000000000000000000000000000Diagnostic 4
guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amountmintv_40178868336 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178868288 = #xffffffffffffffffffffffffffffffffffffffffDiagnostic 5
guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:fromtransferFromv_40178868144 = #x0000000000000000000000000000000000000000Diagnostic 6
guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:totransferFromv_40178868144 = #xffffffffffffffffffffffffffffffffffffffffv_40178868192 = #x0000000000000000000000000000000000000000Diagnostic 7
guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amounttransferFromv_40178868144 = #xffffffffffffffffffffffffffffffffffffffffv_40178868240 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178868192 = #xffffffffffffffffffffffffffffffffffffffffDiagnostic 8
guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spenderapprovev_40178867712 = #x00000000000000000000000000000000000000005. Query Catalog
Q1 - base
transferloc("erc20_bitfield_comptime_generics.ora":108:0SAT0Q2 - obligation
transferloc("erc20_bitfield_comptime_generics.ora":127:0UNSAT0contract invariantQ3 - guard_satisfy
transferloc("erc20_bitfield_comptime_generics.ora":108:0SAT0guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:toQ4 - guard_violate
transferloc("erc20_bitfield_comptime_generics.ora":108:0SAT0guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:tov_40178867904 -> #x0000000000000000000000000000000000000000Q5 - guard_satisfy
transferloc("erc20_bitfield_comptime_generics.ora":108:0SAT1guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amountQ6 - guard_violate
transferloc("erc20_bitfield_comptime_generics.ora":108:0SAT1guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amountQ7 - base
mintloc("erc20_bitfield_comptime_generics.ora":157:0SAT0Q8 - obligation
mintloc("erc20_bitfield_comptime_generics.ora":159:0UNSAT0contract invariantQ9 - obligation
mintloc("erc20_bitfield_comptime_generics.ora":159:0UNSAT0contract invariantQ10 - guard_satisfy
mintloc("erc20_bitfield_comptime_generics.ora":157:0SAT0guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:toQ11 - guard_violate
mintloc("erc20_bitfield_comptime_generics.ora":157:0SAT0guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:tov_40178868288 -> #x0000000000000000000000000000000000000000Q12 - guard_satisfy
mintloc("erc20_bitfield_comptime_generics.ora":157:0SAT1guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amountQ13 - guard_violate
mintloc("erc20_bitfield_comptime_generics.ora":157:0SAT1guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amountQ14 - base
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT0Q15 - guard_satisfy
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT0guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:fromQ16 - guard_violate
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT0guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:fromv_40178868144 -> #x0000000000000000000000000000000000000000Q17 - guard_satisfy
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT0guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:toQ18 - guard_violate
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT0guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:toQ19 - guard_satisfy
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT1guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amountQ20 - guard_violate
transferFromloc("erc20_bitfield_comptime_generics.ora":134:0SAT1guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amountQ21 - base
approveloc("erc20_bitfield_comptime_generics.ora":101:0SAT0Q22 - guard_satisfy
approveloc("erc20_bitfield_comptime_generics.ora":101:0SAT0guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spenderQ23 - guard_violate
approveloc("erc20_bitfield_comptime_generics.ora":101:0SAT0guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spenderv_40178867712 -> #x0000000000000000000000000000000000000000Q24 - base
isPausedloc("erc20_bitfield_comptime_generics.ora":84:0SAT0Q25 - obligation
isPausedloc("erc20_bitfield_comptime_generics.ora":84:0UNSAT0contract invariantQ26 - base
decimalsloc("erc20_bitfield_comptime_generics.ora":79:0SAT0Q27 - obligation
decimalsloc("erc20_bitfield_comptime_generics.ora":79:0UNSAT0contract invariant