lindy-labs / aegis Goto Github PK

View Code? Open in Web Editor NEW

8.0 6.0 0.0 448 KB

Verify Cairo contracts in Lean 4

License: GNU General Public License v3.0

Lean 98.76% Python 1.19% Shell 0.05%

cairo-lang sierra starknet starkware verification

aegis's People

Contributors

Stargazers

Watchers

aegis's Issues

Make `aegis_use_contract_call` more useful

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:

The comment currently connects a spec to a certain contract instance, while it should instead connect the spec to the class hash, since the spec will be the same for all instances (member variables are storage variables under the hood).
The callerAddress of the metadata variable of the called contract currently is the same as the callers callerAddress, need to check if that's correct.
The contractAddress of the metadata variable of the called contract currently is the same as the callers contractAddress, which is probably incorrect.

Add useful metadata to the autogenerated specs

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.

Replace tree-based semantics by DAG based one

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.

Clean up `SierraType`

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).

Add support for non-SSA Sierra

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.

Port to Cairo v2

Add all Cairo e2e libfunc tests

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.

Add support for labels in Sierra files

As can be seen in here. Low priority because these don't seem to show up in Sierra generated from Cairo.

Set up proper testing infrastructure

Maybe see how mathlib4 and std4 run their tests.

Parse .sierra.json files

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.

Add support for backward jumps

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.

Support recurive types

Aegis should be able to support types like

struct Node {
    value: felt252,
    left: Option::<Box<Node>>,
}

Hard to trace bug possible mixing up free variables in the `aegis_proof` goal

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

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.