Panic freedom with F* #133
Conversation
Cargo.toml
Outdated
| ]} | ||
| hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true } | ||
| hax-lib = { git = "https://github.com/hacspec/hax" } | ||
| hax-lib = { git = "https://github.com/hacspec/hax/", branch= "pq11-fstar-libs" } |
There was a problem hiding this comment.
Let's remember to update this before merging.
src/tls13cert.rs
Outdated
| let mut u32word = [U8(0); 4]; | ||
| u32word[0..len].copy_from_slice(&b[offset..offset + len]); | ||
| Ok(u32_from_be_bytes(u32word).declassify() as usize >> ((4 - len) * 8)) | ||
| if b.len() >= offset + len { |
There was a problem hiding this comment.
I'm not sure if this is how it's used. This requires the caller to pass in only the exact slice that's read. I don't think that's how this should be defined.
| if b[offset].declassify() & 0x80u8 == 0u8 { | ||
| Ok((b[offset].declassify() & 0x7fu8) as usize) | ||
| } else { | ||
| if b.len() > offset { |
There was a problem hiding this comment.
Since we can use early returns. We should that in checks like these.
|
Made good progress on this. |
|
Not all functions are yet panic-free, but enough passes that we can put this on CI and make improvements. |
| #[cfg(feature = "hax-pv")] | ||
| use hax_lib::{pv_constructor, pv_handwritten}; | ||
|
|
||
| use hax_lib::ToInt; |
| @@ -0,0 +1,211 @@ | |||
| <<<<<<< HEAD | |||
There was a problem hiding this comment.
This file probably shouldn't be here.
| Result::Ok(l) => b.len() > offset && l <= 255, | ||
| _ => true })] | ||
| fn length_length(b: &Bytes, offset: usize) -> Result<usize, Asn1Error> { | ||
| if b.len() > offset { |
There was a problem hiding this comment.
Since we have early returns now, using that to error out early would make all this code much more readable. Doesn't have to happen in this PR though.
|
Closing in favor of #148 which contains all these changes. |
3 participants
This PR addresses [...] described in issue #.
Type of change
Motivation and Context
This PR adds panic freedom proofs (and relevant annotations) to the core protocol code.
Changes
TODO
Checklist
Fixes #