lindy-labs / aegis

Verify Cairo contracts in Lean 4
GNU General Public License v3.0
8 stars 0 forks source link

Make `aegis_use_contract_call` more useful #20

Open javra opened 7 months ago

javra commented 7 months ago

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:

javra commented 6 months ago

I think one way to resolve this is to wait until there's a way to access the class hash with a syscall, then we have a value to pin the call to and that's the proper way anyway