Bug 840 - Formal proofs and unit tests for cryptoprimitives
Summary: Formal proofs and unit tests for cryptoprimitives
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: Other Linux
: High enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 589
  Show dependency tree / graph
 
Reported: 2022-05-21 16:29 BST by Luke Kenneth Casson Leighton
Modified: 2024-05-22 06:18 BST (History)
3 users (show)

See Also:
NLnet milestone: NLnet.2021.02A.052.CryptoRouter
total budget (EUR) for completion of task and all subtasks: 9500
budget (EUR) for this task, excluding subtasks' budget: 7750
parent task for budget allocation: 589
child tasks for budget allocation: 967 977 1159 1167
The table of payments (in EUR) for this task; TOML format:
lkcl={amount=3750, submitted=2024-05-21} [jacob] amount = 4000 submitted = 2024-05-21

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 Luke Kenneth Casson Leighton 2022-05-21 16:29:56 BST 
Formal correctness proofs and unit tests for the cryptoprimitives
are needed in the HDL and simulators, demonstrating or proving
that the ISA pseudocode, HDL, and simulator are correctly implemented.
Comment 1 Luke Kenneth Casson Leighton 2023-09-05 05:06:41 BST 

    


    


      



        
          Comment 2
        

        
          Luke Kenneth Casson Leighton

        

        
        

        
          2024-05-22 05:56:49 BST
        

      






jacob you put the foral proofs for the work you just did under the wrong bug.
can you please put the notes you added recently copied under THIS bug
which is specifically for Formal Proofs.

    


    


      



        
          Comment 3
        

        
          Jacob Lifshay

        

        
        

        
          2024-05-22 05:59:48 BST
        

      






(In reply to Luke Kenneth Casson Leighton from comment #2)
> jacob you put the foral proofs for the work you just did under the wrong bug.
> can you please put the notes you added recently copied under THIS bug
> which is specifically for Formal Proofs.

I'll just link to all the comments:
note about moving them:
https://bugs.libre-soc.org/show_bug.cgi?id=785#c14

completion of gfbinv's formal proof:
https://bugs.libre-soc.org/show_bug.cgi?id=785#c10

completion of gfbmul/gfbmadd's formal proof:
https://bugs.libre-soc.org/show_bug.cgi?id=785#c12

    


    


      



        
          Comment 4
        

        
          Luke Kenneth Casson Leighton

        

        
        

        
          2024-05-22 06:18:07 BST
        

      






(In reply to Jacob Lifshay from comment #3)

> I'll just link to all the comments:

that works. remember to cross-ref (edit those comments, link to here)