Ensure no Bytes2Int in proof's regs cells to terminate the proof
#43
Conversation
src/tests/integration/test_prove.py
Outdated
| if isinstance(kinner, KApply) and kinner.label == 'Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness': | ||
| no_int2bytes_flag = True |
There was a problem hiding this comment.
| if isinstance(kinner, KApply) and kinner.label == 'Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness': | |
| no_int2bytes_flag = True | |
| match kinner: | |
| case KApply(KLabel('Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness')): | |
| no_int2bytes_flag = True |
There was a problem hiding this comment.
I remember you mentioned a similar suggestion before, but the Python pattern matching didn’t seem to work as intended at the time. I can’t find a suitable test case for this issue right now, so would it be okay to stick with the current implementation for now?
There was a problem hiding this comment.
Sure, but I'm pretty sure this will work as intended.
There was a problem hiding this comment.
Even there are arguments for Int2Bytes?
There was a problem hiding this comment.
Sorry, I'm not familiar with Python's pattern match. But if you are sure about this fact, I can refactor it and see how it works during proving.
There was a problem hiding this comment.
Just refactored the implementation with pattern matching. But I still want to know more about the Python pattern matching functionality.
…tes` check and update proof reporting mechanism
…collect_int2bytes` helper for improved `Int2Bytes` collection and reporting
Stevengre
force-pushed
the
jh/check_result
branch
from
b575709 to
996c6db
Compare
…rn matching for `Int2Bytes` collection, enhancing readability and maintainability
src/tests/integration/test_prove.py
Outdated
| return int2bytes_list | ||
|
|
||
|
|
||
| def check_proof(proof: APRProof, symtool: SymTools) -> str: |
There was a problem hiding this comment.
Consider a more expressive name:
| def check_proof(proof: APRProof, symtool: SymTools) -> str: | |
| def generate_int2bytes_report(proof: APRProof, symtool: SymTools) -> str: |
There was a problem hiding this comment.
Because we might not only check int2bytes, I want to use this name to handle all the checks for the proof.
There was a problem hiding this comment.
Still, the name is somewhat misleading: it does not check anything (i.e., no assert or bool return value), just generates a textual report. How about generate_report then?
There was a problem hiding this comment.
Sure, let me refactor it.
…rting of `Int2Bytes` in `regs` cells, improving clarity and performance
Co-authored-by: Tamás Tóth <[email protected]>
…t`, consolidating proof reporting logic and enhancing clarity
automergerpr-permission-manager
bot
merged commit ed6d043
into
master
No description provided.