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.
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.
(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
(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)
what questions do you (NLnet) have which allow this 100% completed RFP to be paid? both jacob and i are waiting for payment on work that is 100% completed and has proof (comment #3) that it is completed.
as requested by nlnet, I added some documentation in the form of links on the wiki to where the hardware implementations and tests and formal proofs for gfbinv and gfbmadd can be found: https://git.libre-soc.org/?p=libreriscv.git;a=commitdiff;h=b215d742df3838addea3b425c16bf139e3d5f3c8;hp=67bec36c57df5d5de2ecc373026cd015d02c6c40
(In reply to Jacob Lifshay from comment #6) > as requested by nlnet, can you please publish that request. i.e. do not engage in private conversations. it is critically important to ensure full transparency. > I added some documentation in the form of links on > the wiki to where the hardware implementations and tests and formal proofs > for gfbinv and gfbmadd can be found: fantastic. i added an href name and updated the URL field. please get that request (any communication) from nlnet published here. really: it is *unsafe* to engage in private conversations with them. it is unfortunately not appropriate to explain why.
(In reply to Luke Kenneth Casson Leighton from comment #7) > (In reply to Jacob Lifshay from comment #6) > > as requested by nlnet, > > can you please publish that request. i.e. do not engage in private > conversations. > it is critically important to ensure full transparency. I asked for permission, we'll see what they say.
(In reply to Jacob Lifshay from comment #8) > I asked for permission, we'll see what they say. they should not have been speaking privately and directly to you in the first place. just fyi: you and i, as the primary developers, have been accused by nlnet of fabricating work or failing to do the correct or full work, all these years. of failing to meet milestone obligations in full (creating milestones, then submitting an RFP for work that has not been completed, as listed and stated in the milestone description). hence why it is so dangerous, now, to interact privately with them.
financial accounting and audit purposes only: put correct assignment to 2021-02-052 (not 2021-08-071) and correct submission RFP date as it crossed a day barrier, due to nlnet's server being in UTC+2 when the submission was done from the UK (UTC+1) and the records being done between 23:01 and 00:00 on the 21st in the UK, nlnet's server (in holland) recorded this as the *22nd*.
a private and secretive conversation took place between an agent of nlnet and jacob lifshay (see comment #6 for evidence of the existence of that private, secretive and non-transparent conversation) we have evidence of a review taking place, in the form of a disconnected message from nlnet's system (no cross-referencing provided). only by chance was it possible to make the connection that it was this bugreport that had been reviewed. https://lists.libre-soc.org/pipermail/libre-soc-dev/2024-August/006407.html
in checking the NLnet RFP records (their system) more closely, it is *jacob's* RFP that has been approved on this bugreport, but mine has *not* been approved. they are for the exact same work, the exact same bugreport, but jacob's RFP has been approved (payment now pending) and mine has not.
Michiel, I'll note that if the documentation I added to the wiki was sufficient for me to get paid for this task, I would assume it's also sufficient for Luke to get paid for the exact same task, him getting assigned EUR 3750 of the budget on this task is intentional and was agreed on by both of us.
(In reply to Jacob Lifshay from comment #13) > Michiel, I'll note that if the documentation I added to the wiki was > sufficient for me to get paid for this task, I would assume it's also > sufficient for Luke to get paid for the exact same task, him getting > assigned EUR 3750 of the budget on this task is intentional and was agreed > on by both of us. jacob please email them and/or call them directly as the obvious implication from what they have are saying is, "luke is an untrustworthy abuser whom we cannot listen to, therefore let's punish him by shutting down ALL RFPs". https://lists.libre-soc.org/pipermail/libre-soc-dev/2024-August/006419.html HELP.
(In reply to Jacob Lifshay from comment #13) Michiel gave me permission to quote the following reply: > > I would assume it's also sufficient for Luke to get paid for the exact same task > > That is an understandable but incorrect inference. Even within a single task, different people will have distinct roles and responsibilities. You made an engineering contribution. That part seems finished, and so it was paid. As the project lead, Luke is also responsible for integrating the outputs of this and all other dangling task into the documentation skeleton of this particular project. The project is claimed to be completed, so we are asking where the outputs we were promised by Luke can be found. > > At this moment, there is nothing even remotely shaped like a cryptorouter documented anywhere - not even a failed, incomplete one. We need Luke (or someone else knowledgeable) to provide this skeleton. > > I think this would probably be the right starting point: > > https://libre-soc.org/crypto_router_asic/ > > This page was last edited Thu Nov 25 17:13:51 2021, but from there it would seem feasible to get the heavily fragmented information into a presentable shape.