Implement vm.record cheat code
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 35/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- blockchain
Direzione di ricerca
Inizia da foundry.md e dalle regole EVM esistenti in evm.md, quindi confronta la documentazione di Foundry collegata relativa a vm.record e vm.accesses. Implementa lo stato di registrazione, l’intercettazione dei cheat code e la registrazione di SLOAD/SSTORE descritti nell’issue; il lavoro è completato quando l’integrazione Foundry di ercx non si ferma più a vm.record e i relativi dati di accesso vengono acquisiti.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
When testing an ercx test with the kevm foundry integration, the proof ended because it reached an unimplemented cheat code vm.record. The documentation for record can be found here.
As a suggestion, you can try this implementation:
- extending the configuration in
foundry.mdto add these cells:
<recordAccess>
<recordActive> false </recordActive>
<records>
<record multiplicity="*" type="Map">
<recordKey> 0 </recordKey>
<reads> .List </reads>
<writes> .List </writes>
</record>
</records>
</recordAccess>
- add a
#call_foundryrule that intercepts the call of the cheat code
rule [foundry.call.record]:
<k> #call_foundry SELECTOR _ => #enableRecord ... </k>
requires SELECTOR ==Int selector ( "record()" )
Here, #enableRecord will start recording the storage operations.
rule <k> #enableRecord => . ... </k>
<recordAccess>
<recordActive> _ => true </recordActive>
...
</recordAccess>
- overwrite rules for
SLOADandSSTOREto write in the records cells whilerecordActiveistrue.
rule [foundry.recordSLOAD]:
<k> SLOAD INDEX => #recordRead INDEX ~> #pauseRecord ~> SLOAD INDEX ~> #resumeRecord ... </k>
<recordAccess> <recordActive> true </recordActive> ... </recordAccess>
[priority(39)]
rule [foundry.recordSSTORE]:
<k> SSTORE INDEX NEW => #recordRead INDEX ~> #recordWrite INDEX ~> #pauseRecord ~> SSTORE INDEX NEW ~> #resumeRecord ... </k>
<recordAccess> <recordActive> true </recordActive> ... </recordAccess>
[priority(39)]
Here, #pauseRecord and #unpauseRecord could be used to allow the original SLOAD/SSTORE rules from evm.md to be executed by disabling/reenabling the recording.
rule <k> #resumeRecord => . ... </k>
<recordAccess> <recordActive> _ => true </recordActive> ... </recordAccess>
rule <k> #pauseRecord => . ... </k>
<recordAccess> <recordActive> _ => false </recordActive> ... </recordAccess>
And #recordRead and #recordWrite can record the operations.
rule <k> #recordRead V => . </k>
<id> KEY </id>
<recordAccess>
<record>
<recordKey> KEY </recordKey>
<reads> R => R ListItem(#buf(32, V)) </reads>
...
</record>
...
</recordAccess>
rule <k> #recordRead V => . </k>
<id> KEY </id>
<recordAccess>
<records>
( .Bag
=> <record>
<recordKey> KEY </recordKey>
<reads> ListItem(#buf(32, V)) </reads>
...
</record>
)
</records>
...
</recordAccess> [owise]
rule <k> #recordWrite V => . </k>
<id> KEY </id>
<recordAccess>
<record>
<recordKey> KEY </recordKey>
<writes> R => R ListItem(#buf(32, V)) </writes>
...
</record>
...
</recordAccess>
This cheat code goes hand in hand with vm.accesses, so probably this needs to be implemented as well.
- Lingua principale
- KCL
- Stelle
- 592
- Fork
- 156
- Merge medio
- 2h 19m
- PR unite (30g)
- 1
Preparare l'ambiente
Non abbiamo ancora controllato i file di configurazione di questo progetto. Parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·
Tutte le issue di runtimeverification/evm-semantics
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
foundry-rs/foundry#17167 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 92/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 86/100
OpenZeppelin/openzeppelin-community-contracts#292 ·
I maintainer di solito rispondono entro 2 giorni
-
bogota
Difficoltà 2/5 1-3 ore Idoneità per principianti 84/100
NethermindEth/nethermind#14035 ·
I maintainer di solito rispondono entro 1 giorno
-
submission
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
Uniswap/hooklist#10463 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno