Skip to content

Instantly share code, notes, and snippets.

@ngmachado
Created February 14, 2026 22:38
Show Gist options
  • Select an option

  • Save ngmachado/63e3fb7278b2f86325c1b918894ef26b to your computer and use it in GitHub Desktop.

Select an option

Save ngmachado/63e3fb7278b2f86325c1b918894ef26b to your computer and use it in GitHub Desktop.
// 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;
}
}
@ngmachado
Copy link
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 = #x0000000000000000000000000000000000000000000000000000000000000000
    • v_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 = #x0000000000000000000000000000000000000000000000000000000000000000
    • v_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 = #xffffffffffffffffffffffffffffffffffffffff
    • v_40178868192 = #x0000000000000000000000000000000000000000

Diagnostic 7

  • Guard ID: guard:erc20_bitfield_comptime_generics.ora:134:67:6:min_value:amount
  • Function: transferFrom
  • Counterexample:
    • v_40178868144 = #xffffffffffffffffffffffffffffffffffffffff
    • v_40178868240 = #x0000000000000000000000000000000000000000000000000000000000000000
    • v_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