Bug 840

Summary:	Formal proofs and unit tests for cryptoprimitives
Product:	Libre-SOC's first SoC	Reporter:	Luke Kenneth Casson Leighton <lkcl>
Component:	Source Code	Assignee:	Luke Kenneth Casson Leighton <lkcl>
Status:	RESOLVED FIXED
Severity:	enhancement	CC:	cestrauss, libre-soc-bugs, programmerjake
Priority:	High
Version:	unspecified
Hardware:	Other
OS:	Linux
See Also:	https://bugs.libre-soc.org/show_bug.cgi?id=771 https://bugs.libre-soc.org/show_bug.cgi?id=772 https://bugs.libre-soc.org/show_bug.cgi?id=755 https://bugs.libre-soc.org/show_bug.cgi?id=785
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
Bug Depends on:
Bug Blocks:	589

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)