lindy-labs / aegis Goto Github PK
View Code? Open in Web Editor NEWVerify Cairo contracts in Lean 4
License: GNU General Public License v3.0
Verify Cairo contracts in Lean 4
License: GNU General Public License v3.0
It currently can only refer to calling contracts deployed at an address known at verification time, which doesn't make the command particularly useful. References to other contracts are usually contained in a contract's storage and read from there, so aegis_use_contract_call
must be able to make the registry dependent on the storage content at least (or allow arbitrary variables?). Furthermore we must address the following errors in the current implementation:
callerAddress
of the metadata variable of the called contract currently is the same as the callers callerAddress
, need to check if that's correct.contractAddress
of the metadata variable of the called contract currently is the same as the callers contractAddress
, which is probably incorrect.It's often useful to know which function call a certain part of the autogenerated spec comes from. We could use the MData
of the expressions to track that.
Right now series of confluent branchings blow up the generated term exponentially. This path explosion issue is not really necessary if we replace the use of AndOrTree
in the semantics by a suitable data structure of series-parallel graphs that treat confluence points correctly (exactly the Sierra statements containing branch_align
). The control flow of process_state
in Aegis.Analyzer
has to be changed to account for that.
Currently we conflate some types in SierraType
which we shouldn't, Span<T>
and Array<T>
being one example. Those should be distinguished and only conflated on semantics level (at .toQuote
).
So far, we've relied on Sierra files being always in SSA form, but as we can see here, this is not required. We need to keep an eye on the compiler output to spot if this will be a problem in the future.
These should all be reference tests of the libfunc implementations.
Some of them are already in Tests.Commands
but it would be better to have them each in their own file and complete.
As can be seen in here. Low priority because these don't seem to show up in Sierra generated from Cairo.
Maybe see how mathlib4
and std4
run their tests.
We can use Lean.Data.Json
for that. This would have the advantage of not needing to add sierra-text = true
to Scarb.toml
files whever we want to gain a Sierra output that's usable in Aegis.
Aegis will time out on backward jumps since we assume that those don't show up in Sierra code generated by the compiler. This is because loops will usually be transformed into recursive calls. We'll need to emulate that transformation on the Aegis side if we want to support backward jumps.
Aegis should be able to support types like
struct Node {
value: felt252,
left: Option::<Box<Node>>,
}
Appears when using a storageaccess_bug.cairo
containing
use debug::PrintTrait;
use core::result;
use core::result::ResultTrait;
use core::integer;
use core::starknet::contract_address::ContractAddress;
use core::starknet;
use core::starknet::SyscallResult;
use core::starknet::SyscallResultTrait;
use core::starknet::info::ExecutionInfo;
use core::array::ArrayTrait;
use starknet::{StorageAccess, StorageBaseAddress, StorageAddress};
use starknet::syscalls::{storage_read_syscall, storage_write_syscall};
use starknet::storage_access::{StorageAccessU8, StorageAccessU32, StorageAccessU64, StorageAccessU128};
use starknet::storage_access::{StorageAccessU256, StorageAccessBool, StorageAccessContractAddress};
use core::hash::LegacyHash;
fn main(contract_address : ContractAddress,
syscall_result_contract_address : SyscallResult<ContractAddress>,
syscall_result_u8 : SyscallResult<u8>,
syscall_result_u128 : SyscallResult<u128>,
syscall_result_unit : SyscallResult<()>,
syscall_result_box_execution_info : SyscallResult<Box<ExecutionInfo>>,
syscall_result_span_felt252 : SyscallResult<Span<felt252>>,
syscall_result_u256 : SyscallResult<u256>,
syscall_result_felt252 : SyscallResult<felt252>,
syscall_result_bool : SyscallResult<bool>,
storage_base_address : StorageBaseAddress,
storage_address : StorageAddress,
ref ref_array_felt252 : Array<felt252>) {
//core::result::ResultTraitImpl<core::integer::u32, core::integer::u32>::expect<core::integer::u32Drop>();
let x : Result<u32, u32> = Result::Ok(0_u32);
let x : u32 = x.expect('foo');
//core::result::ResultTraitImpl<core::integer::u64, core::integer::u64>::expect<core::integer::u64Drop>
let x : Result<u64, u64> = Result::Ok(0_u64);
let x : u64 = x.expect('foo');
//core::result::ResultTraitImpl<core::integer::u8, core::integer::u8>::expect<core::integer::u8Drop>
let x : Result<u8, u8> = Result::Ok(0_u8);
let x : u8 = x.expect('foo');
//core::integer::U8Sub::sub
let x = 42_u8 - 23_u8;
//core::integer::u128_checked_mul
let x = core::integer::u128_checked_mul(0_u128, 0_u128);
//core::integer::U128Mul::mul
let x = core::integer::U128Mul::mul(0_u128, 0_u128);
//core::result::ResultTraitImpl<core::integer::u128, core::integer::u128>::expect<core::integer::u128Drop>
let x : Result<u128, u128> = Result::Ok(0_u128);
let x : u128 = x.expect('foo');
//core::integer::U128Sub::sub
let x = core::integer::U128Sub::sub(0, 0);
//core::integer::u128_try_from_felt252
let x = core::integer::u128_try_from_felt252(0);
//core::integer::U128BitNot::bitnot
let x = core::integer::U128BitNot::bitnot(0);
//core::integer::u64_try_as_non_zero
let x = core::integer::u64_try_as_non_zero(0);
//core::integer::u128_try_as_non_zero
let x = core::integer::u128_try_as_non_zero(0);
//core::integer::u256_try_as_non_zero
let x = core::integer::u256_try_as_non_zero(0);
//core::integer::u64_as_non_zero
let x = core::integer::u64_as_non_zero(0);
//core::integer::u128_as_non_zero
let x = core::integer::u128_as_non_zero(0);
//core::integer::u256_as_non_zero
let x = core::integer::u256_as_non_zero(0);
//core::integer::u256_from_felt252
let x = core::integer::u256_from_felt252(0);
//core::integer::U64TryIntoNonZero::try_into
let x = core::integer::U64TryIntoNonZero::try_into(0);
//core::integer::U128TryIntoNonZero::try_into
let x = core::integer::U128TryIntoNonZero::try_into(0);
//core::integer::U256TryIntoNonZero::try_into
let x = core::integer::U256TryIntoNonZero::try_into(0);
//core::integer::Felt252TryIntoU8::try_into
let x = core::integer::Felt252TryIntoU8::try_into(0);
//core::integer::Felt252TryIntoU32::try_into
let x = core::integer::Felt252TryIntoU32::try_into(0);
//core::integer::Felt252TryIntoU64::try_into
let x = core::integer::Felt252TryIntoU64::try_into(0);
//core::integer::U32Add::add
let x = core::integer::U32Add::add(0, 0);
//core::integer::U32Sub::sub
let x = core::integer::U32Sub::sub(0, 0);
//core::integer::U64Add::add
let x = core::integer::U64Add::add(0, 0);
//core::integer::U64Sub::sub
let x = core::integer::U64Sub::sub(0, 0);
//core::integer::U64Div::div
let x = core::integer::U64Div::div(0, 0);
//core::integer::U128Div::div
let x = core::integer::U128Div::div(0, 0);
//core::integer::U128Add::add
let x = core::integer::U128Add::add(0, 0);
//core::integer::u256_overflowing_add
let x = core::integer::u256_overflowing_add(0, 0);
//core::integer::u256_checked_add
let x = core::integer::u256_checked_add(0, 0);
//core::integer::U256Add::add
let x = core::integer::U256Add::add(0, 0);
//core::integer::u256_overflow_sub
let x = core::integer::u256_overflow_sub(0, 0);
//core::integer::u256_checked_sub
let x = core::integer::u256_checked_sub(0, 0);
//core::integer::U256Sub::sub
let x = core::integer::U256Sub::sub(0, 0);
//core::integer::u256_overflow_mul
let x = core::integer::u256_overflow_mul(0, 0);
//core::integer::u256_checked_mul
let x = core::integer::u256_checked_mul(0, 0);
//core::integer::U256Mul::mul
let x = core::integer::U256Mul::mul(0, 0);
//core::integer::U256PartialOrd::lt
let x = core::integer::U256PartialOrd::lt(0, 0);
//core::integer::U256Div::div
let x = core::integer::U256Div::div(0, 0);
//core::hash::LegacyHashContractAddress::hash
let x = core::hash::LegacyHashContractAddress::hash(0, contract_address);
//core::starknet::contract_address::Felt252TryIntoContractAddress::try_into
let x = core::starknet::contract_address::Felt252TryIntoContractAddress::try_into(0);
//core::starknet::info::get_execution_info
let x = core::starknet::info::get_execution_info();
//core::starknet::info::get_caller_address
let x = core::starknet::info::get_caller_address();
//core::starknet::info::get_contract_address
let x = core::starknet::info::get_contract_address();
//core::starknet::info::get_block_timestamp
let x = core::starknet::info::get_block_timestamp();
//core::starknet::SyscallResultTraitImpl<core::starknet::contract_address::ContractAddress>::unwrap_syscall
let x = syscall_result_contract_address.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::integer::u8>::unwrap_syscall
let x = syscall_result_u8.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::integer::u128>::unwrap_syscall
let x = syscall_result_u128.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<()>::unwrap_syscall
let x = syscall_result_unit.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::box::Box<core::starknet::info::ExecutionInfo>>::unwrap_syscall
let x = syscall_result_box_execution_info.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::array::Span<core::felt252>>::unwrap_syscall
let x = syscall_result_span_felt252.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::integer::u256>::unwrap_syscall
let x = syscall_result_u256.unwrap_syscall();
//core::starknet::SyscallResultTraitImpl<core::felt252>::unwrap_syscall
let x = syscall_result_felt252.unwrap_syscall();
//core::starknet::storage_access::StorageAccessU8::read
let x = StorageAccessU8::read(0, storage_base_address).unwrap_syscall();
}
and try to solve it using
import Aegis.Commands
import CorelibVerification.Corelib.Integer
import CorelibVerification.Corelib.Starknet.StorageAccess
import CorelibVerification.Corelib.Starknet.SyscallResult
import CorelibVerification.Corelib.Starknet
import CorelibVerification.Corelib.Starknet.Info
import CorelibVerification.Corelib.Hash
aegis_load_file "storageaccess_bug.sierra"
aegis_spec "storageaccess_bug::storageaccess_bug::main" :=
fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => True
aegis_prove "storageaccess_bug::storageaccess_bug::main" :=
fun m _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => True.intro
aegis_complete
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.