Bug 840 - Formal proofs and unit tests for cryptoprimitives
Summary: Formal proofs and unit tests for cryptoprimitives
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: Other Linux
: High enhancement
Assignee: Konstantinos Margaritis (markos)
URL:
Depends on:
Blocks: 589
  Show dependency tree / graph
 
Reported: 2022-05-21 16:29 BST by Luke Kenneth Casson Leighton
Modified: 2023-09-19 22:51 BST (History)
5 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:

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 
konstantinos again i am assigning this bug to you as a reminder
to create unit-test sub-bugs for ed25519 (just like we did for
chacha20) and another sub-bug for the long-mul REMAPper
(which is best done *not straight away* in the pypowersim style
but first in a new test_caller_svp64_longmul.py, just like
test_caller_svp64_chacha20.py and others, *and then* an actual
long-mul pypowersim test)