Franziskus Kiefer comments

Results 353 comments of


                                            Franziskus Kiefer

Coq backend: handle constructors with bases (aka `{field: expr, ..base}` in rust)

Please re-open @cmester0 if still relevant.

Inlining of a macro call comming from another macro expansion

We will remove all legacy hacspec lib code.

Document the generic printer and how to write a backend

There's a draft from @jschneider-bensch https://github.com/hacspec/book/pull/14

F*: pattern matching is disallowed on `usize`s, `isize`s (+`u128`/`i128`)

There's a design in #806 that needs to get implemented.

Add utility function to deal with mutual dependency across different modules

@W95Psp please look at this to see what it takes to get this fixed.

ci/kyber: unify hax' job with licbrux' one

This should still happen

Fix `attempted to read from stolen value`

Another code snippet that panics ```rust #[repr(u16)] pub enum ProtocolVersion { Mls10 = 1, } impl ProtocolVersion { #[allow(non_upper_case_globals)] fn tls_deserialize(bytes: &[u8]) -> core::result::Result { const __TLS_CODEC_Mls10: u16 = ProtocolVersion::Mls10...

Fix `attempted to read from stolen value`

[It looks like](https://hax-playground.cryspen.com/#fstar/2a66ae9ad5/gist=4d63927f53589866dd694a98838e2613) the two examples here are not triggering the stealing bug anymore.

Fix `attempted to read from stolen value`

I can't reproduce with any of the examples in here. Unless we have a reproducer, let's close this and open something new when we hit it again.

Fix `attempted to read from stolen value`

This is still an issue (see linked libcrux issue above).