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
Author
SMT reported that is the companion for auditors
SMT Encoding Report
1. Run Metadata
- Source file:
ora-example/apps/erc20_bitfield_comptime_generics.ora - Generated at (unix):
1771155094 - Verification mode:
basic - verify_calls:
true - verify_state:
true - parallel:
true - timeout_ms:
60000
2. Summary
- Total queries:
27 - SAT:
22 - UNSAT:
5 - UNKNOWN:
0 - Failed obligations:
0 - Inconsistent assumption bases:
0 - Proven guards:
0 - Violatable guards:
8 - Verification success:
true - Verification errors:
0 - Verification diagnostics:
8
3. Query Kind Counts
- base:
6 - obligation:
5 - loop_invariant_step:
0 - loop_invariant_post:
0 - guard_satisfy:
8 - guard_violate:
8
4. Findings
Diagnostic 1
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:to - Function:
transfer - Counterexample:
v_40178867904 = #x0000000000000000000000000000000000000000
Diagnostic 2
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amount - Function:
transfer - Counterexample:
v_40178867952 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178867904 = #xffffffffffffffffffffffffffffffffffffffff
Diagnostic 3
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:to - Function:
mint - Counterexample:
v_40178868288 = #x0000000000000000000000000000000000000000
Diagnostic 4
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amount - Function:
mint - Counterexample:
v_40178868336 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178868288 = #xffffffffffffffffffffffffffffffffffffffff
Diagnostic 5
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:from - Function:
transferFrom - Counterexample:
v_40178868144 = #x0000000000000000000000000000000000000000
Diagnostic 6
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:to - Function:
transferFrom - Counterexample:
v_40178868144 = #xffffffffffffffffffffffffffffffffffffffffv_40178868192 = #x0000000000000000000000000000000000000000
Diagnostic 7
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amount - Function:
transferFrom - Counterexample:
v_40178868144 = #xffffffffffffffffffffffffffffffffffffffffv_40178868240 = #x0000000000000000000000000000000000000000000000000000000000000000v_40178868192 = #xffffffffffffffffffffffffffffffffffffffff
Diagnostic 8
- Guard ID:
guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spender - Function:
approve - Counterexample:
v_40178867712 = #x0000000000000000000000000000000000000000
5. Query Catalog
Q1 - base
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":108:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
Q2 - obligation
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":127:0 - Status:
UNSAT - Elapsed ms:
0 - Obligation kind:
contract invariant - SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
(assert (not (bvult #x0000000000000000000000000000000000000000000000000000000000000003
#x0000000000000000000000000000000000000000000000000000000000000100)))
Q3 - guard_satisfy
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":108:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:to - SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(declare-fun v_40178867904 () (_ BitVec 160))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
(assert (not (= ((_ extract 159 0) v_40178867904)
#x0000000000000000000000000000000000000000)))
Q4 - guard_violate
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":108:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:21:2:non_zero_address:to - Model:
v_40178867904 -> #x0000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(declare-fun v_40178867904 () (_ BitVec 160))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
(assert (not (not (= ((_ extract 159 0) v_40178867904)
#x0000000000000000000000000000000000000000))))
Q5 - guard_satisfy
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":108:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amount - SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(declare-fun v_40178867904 () (_ BitVec 160))
(declare-fun v_40178867952 () (_ BitVec 256))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
(assert (not (= ((_ extract 159 0) v_40178867904)
#x0000000000000000000000000000000000000000)))
(assert (bvuge v_40178867952
#x0000000000000000000000000000000000000000000000000000000000000001))
Q6 - guard_violate
- Function:
transfer - Location:
loc("erc20_bitfield_comptime_generics.ora":108:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:108:41:6:min_value:amount - Model:
v_40178867904 -> #xffffffffffffffffffffffffffffffffffffffff
v_40178867952 -> #x0000000000000000000000000000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun env_evm_caller () (_ BitVec 160))
(declare-fun g_account_flags () (Array (_ BitVec 160) (_ BitVec 256)))
(declare-fun v_40178867904 () (_ BitVec 160))
(declare-fun v_40178867952 () (_ BitVec 256))
(assert (bvule (bvand (bvlshr (select g_account_flags env_evm_caller)
#x0000000000000000000000000000000000000000000000000000000000000003)
#x000000000000000000000000000000000000000000000000000000000000ffff)
#x000000000000000000000000000000000000000000000000000000000000ffff))
(assert (not (= ((_ extract 159 0) v_40178867904)
#x0000000000000000000000000000000000000000)))
(assert (not (bvuge v_40178867952
#x0000000000000000000000000000000000000000000000000000000000000001)))
Q7 - base
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":157:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
Q8 - obligation
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":159:0 - Status:
UNSAT - Elapsed ms:
0 - Obligation kind:
contract invariant - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (bvult #x0000000000000000000000000000000000000000000000000000000000000002
#x0000000000000000000000000000000000000000000000000000000000000100)))
Q9 - obligation
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":159:0 - Status:
UNSAT - Elapsed ms:
0 - Obligation kind:
contract invariant - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (bvult #x0000000000000000000000000000000000000000000000000000000000000002
#x0000000000000000000000000000000000000000000000000000000000000100)))
Q10 - guard_satisfy
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":157:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:to - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(declare-fun v_40178868288 () (_ BitVec 160))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (= ((_ extract 159 0) v_40178868288)
#x0000000000000000000000000000000000000000)))
Q11 - guard_violate
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":157:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:17:2:non_zero_address:to - Model:
v_40178868288 -> #x0000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(declare-fun v_40178868288 () (_ BitVec 160))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (not (= ((_ extract 159 0) v_40178868288)
#x0000000000000000000000000000000000000000))))
Q12 - guard_satisfy
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":157:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amount - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(declare-fun v_40178868288 () (_ BitVec 160))
(declare-fun v_40178868336 () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (= ((_ extract 159 0) v_40178868288)
#x0000000000000000000000000000000000000000)))
(assert (bvuge v_40178868336
#x0000000000000000000000000000000000000000000000000000000000000001))
Q13 - guard_violate
- Function:
mint - Location:
loc("erc20_bitfield_comptime_generics.ora":157:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:157:37:6:min_value:amount - Model:
v_40178868288 -> #xffffffffffffffffffffffffffffffffffffffff
v_40178868336 -> #x0000000000000000000000000000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(declare-fun v_40178868288 () (_ BitVec 160))
(declare-fun v_40178868336 () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000002)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (= ((_ extract 159 0) v_40178868288)
#x0000000000000000000000000000000000000000)))
(assert (not (bvuge v_40178868336
#x0000000000000000000000000000000000000000000000000000000000000001)))
Q14 - base
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
Q15 - guard_satisfy
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:from - SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(assert (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000)))
Q16 - guard_violate
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:25:4:non_zero_address:from - Model:
v_40178868144 -> #x0000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(assert (not (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000))))
Q17 - guard_satisfy
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:to - SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(declare-fun v_40178868192 () (_ BitVec 160))
(assert (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40178868192)
#x0000000000000000000000000000000000000000)))
Q18 - guard_violate
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:47:2:non_zero_address:to - Model:
v_40178868144 -> #xffffffffffffffffffffffffffffffffffffffff
v_40178868192 -> #x0000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(declare-fun v_40178868192 () (_ BitVec 160))
(assert (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000)))
(assert (not (not (= ((_ extract 159 0) v_40178868192)
#x0000000000000000000000000000000000000000))))
Q19 - guard_satisfy
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amount - SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(declare-fun v_40178868192 () (_ BitVec 160))
(declare-fun v_40178868240 () (_ BitVec 256))
(assert (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40178868192)
#x0000000000000000000000000000000000000000)))
(assert (bvuge v_40178868240
#x0000000000000000000000000000000000000000000000000000000000000001))
Q20 - guard_violate
- Function:
transferFrom - Location:
loc("erc20_bitfield_comptime_generics.ora":134:0 - Status:
SAT - Elapsed ms:
1 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amount - Model:
v_40178868144 -> #xffffffffffffffffffffffffffffffffffffffff
v_40178868192 -> #xffffffffffffffffffffffffffffffffffffffff
v_40178868240 -> #x0000000000000000000000000000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun v_40178868144 () (_ BitVec 160))
(declare-fun v_40178868192 () (_ BitVec 160))
(declare-fun v_40178868240 () (_ BitVec 256))
(assert (not (= ((_ extract 159 0) v_40178868144)
#x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40178868192)
#x0000000000000000000000000000000000000000)))
(assert (not (bvuge v_40178868240
#x0000000000000000000000000000000000000000000000000000000000000001)))
Q21 - base
- Function:
approve - Location:
loc("erc20_bitfield_comptime_generics.ora":101:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
Q22 - guard_satisfy
- Function:
approve - Location:
loc("erc20_bitfield_comptime_generics.ora":101:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spender - SMT-LIB:
(declare-fun v_40178867712 () (_ BitVec 160))
(assert (not (= ((_ extract 159 0) v_40178867712)
#x0000000000000000000000000000000000000000)))
Q23 - guard_violate
- Function:
approve - Location:
loc("erc20_bitfield_comptime_generics.ora":101:0 - Status:
SAT - Elapsed ms:
0 - Guard ID:
guard:erc20_bitfield_comptime_generics.ora:101:20:7:non_zero_address:spender - Model:
v_40178867712 -> #x0000000000000000000000000000000000000000
- SMT-LIB:
(declare-fun v_40178867712 () (_ BitVec 160))
(assert (not (not (= ((_ extract 159 0) v_40178867712)
#x0000000000000000000000000000000000000000))))
Q24 - base
- Function:
isPaused - Location:
loc("erc20_bitfield_comptime_generics.ora":84:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
Q25 - obligation
- Function:
isPaused - Location:
loc("erc20_bitfield_comptime_generics.ora":84:0 - Status:
UNSAT - Elapsed ms:
0 - Obligation kind:
contract invariant - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001)
#x0000000000000000000000000000000000000000000000000000000000000001))
(assert (not (bvult #x0000000000000000000000000000000000000000000000000000000000000001
#x0000000000000000000000000000000000000000000000000000000000000100)))
Q26 - base
- Function:
decimals - Location:
loc("erc20_bitfield_comptime_generics.ora":79:0 - Status:
SAT - Elapsed ms:
0 - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000004)
#x00000000000000000000000000000000000000000000000000000000000000ff)
#x00000000000000000000000000000000000000000000000000000000000000ff))
Q27 - obligation
- Function:
decimals - Location:
loc("erc20_bitfield_comptime_generics.ora":79:0 - Status:
UNSAT - Elapsed ms:
0 - Obligation kind:
contract invariant - SMT-LIB:
(declare-fun g_token_flags () (_ BitVec 256))
(assert (bvule (bvand (bvlshr g_token_flags
#x0000000000000000000000000000000000000000000000000000000000000004)
#x00000000000000000000000000000000000000000000000000000000000000ff)
#x00000000000000000000000000000000000000000000000000000000000000ff))
(assert (not (bvult #x0000000000000000000000000000000000000000000000000000000000000004
#x0000000000000000000000000000000000000000000000000000000000000100)))
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Anvil tests