mamonet

> Thanks Maamoun, that's really neat! To follow up on this: > > * can you attach a patch for the generated C code so that we can see precisely...

> Thanks @mamonet that looks great. Just to clarify, do you plan on submitting PRs that implement these two changes or are you just filing bugs in the hope that...

Thank you. Any assistance or hints would be great. I'm able to upload my first try to modify Hacl.Impl.Poly1305.fst to reflect the change if that helps the code maintainer.

It seems a tuning flags has been added to the configure without me noticing. However, I've submitted a proper configure patch in PR #455 with slight performance boost on POWER9.

@MrDracoG, this issue is more specialized than the issue you have mentioned, working on this issue requires specific qualifications and experience. Let me explain what kind of work is required...

@msprotz @Chris-Hawblitzel To organize things more, I suggest creating a new branch in this repository to receive the pull requests once verified by IBM crypto team to submit them to...

Thanks, that makes adding support of another architecture much simpler for starters. I noticed that x64simple's modules utilize the the modules in directory https://github.com/project-everest/vale/tree/master/fstar/specs/hardware so I think I need to...

> My advice is to start as simple as possible. I just added a directory https://github.com/project-everest/vale/tree/master/fstar/code/arch/x64simple to show simple definitions of x64 code. I've added the basic PowerPC support to...

In order to proceed with the roadmap, I've pushed a PR https://github.com/project-everest/vale/pull/51 into Vale repository that adds basic PowerPC support. The patch covers more testing cases than the initial one...

I've added SHA implementation with HACL integration of vale support into my fork of repository https://github.com/mamonet/hacl-star/commit/46e7e73eea9c84cd3aa57f5193007ca67de67759 Hacl integration includes the following features. - Basic vale support of PowerPC architecture. -...