Bug 902 - Formal proof for nmutil byterev.py
Summary: Formal proof for nmutil byterev.py
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Jacob Lifshay
URL:
Depends on:
Blocks: 198
  Show dependency tree / graph
 
Reported: 2022-08-04 08:08 BST by Jacob Lifshay
Modified: 2022-08-28 17:53 BST (History)
3 users (show)

See Also:
NLnet milestone: ---
total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Jacob Lifshay 2022-08-04 08:08:53 BST 

    


    


      



        
          Comment 1
        

        
          Jacob Lifshay

        

        
        

        
          2022-08-04 08:11:33 BST
        

      






Finished formal proof.

https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/formal/test_byterev.py;h=6df71bda009411ae8390bde879f11e0928fac616;hb=02ce4630db0814025c25a97d38f9a9357062bca3

byte_reverse zeroing everything other than the `length` least-significant bits threw me off for a while...I added a note to the docs specifically pointing that out so others don't get confused.

    


    


      



        
          Comment 2
        

        
          Luke Kenneth Casson Leighton

        

        
        

        
          2022-08-04 11:30:41 BST
        

      






(In reply to Jacob Lifshay from comment #1)

> byte_reverse zeroing everything other than the `length` least-significant
> bits threw me off for a while...I added a note to the docs specifically
> pointing that out so others don't get confused.

ah good, yes sensible.  breaking expectations bad.