Proptests of chain building block behavior.

This commit is contained in:
gram-signal 2026-01-16 12:51:06 -08:00 committed by GitHub
parent d310c99c57
commit f8788e9c74
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 268 additions and 19 deletions

1
.gitignore vendored
View File

@ -2,3 +2,4 @@
tarpaulin-report.html
rust-toolchain.toml
/.fstar-cache
proptest-regressions

83
Cargo.lock generated
View File

@ -73,6 +73,21 @@ version = "1.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
[[package]]
name = "bit-set"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "08807e080ed7f9d5433fa9b275196cfc35414f66a0c79d864dc51a0d825231a3"
dependencies = [
"bit-vec",
]
[[package]]
name = "bit-vec"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7"
[[package]]
name = "bitflags"
version = "2.9.0"
@ -257,6 +272,12 @@ version = "0.5.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99"
[[package]]
name = "fnv"
version = "1.0.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
[[package]]
name = "galois_field_2pm"
version = "0.1.0"
@ -732,6 +753,25 @@ dependencies = [
"unicode-ident",
]
[[package]]
name = "proptest"
version = "1.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bee689443a2bd0a16ab0348b52ee43e3b2d1b1f931c8aa5c9f8de4c86fbe8c40"
dependencies = [
"bit-set",
"bit-vec",
"bitflags",
"num-traits",
"rand 0.9.1",
"rand_chacha 0.9.0",
"rand_xorshift",
"regex-syntax",
"rusty-fork",
"tempfile",
"unarray",
]
[[package]]
name = "prost"
version = "0.14.1"
@ -784,6 +824,12 @@ dependencies = [
"prost",
]
[[package]]
name = "quick-error"
version = "1.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0"
[[package]]
name = "quote"
version = "1.0.40"
@ -868,6 +914,15 @@ dependencies = [
"rand 0.9.1",
]
[[package]]
name = "rand_xorshift"
version = "0.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a"
dependencies = [
"rand_core 0.9.3",
]
[[package]]
name = "regex"
version = "1.11.1"
@ -919,6 +974,18 @@ dependencies = [
"windows-sys 0.59.0",
]
[[package]]
name = "rusty-fork"
version = "0.3.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cc6bf79ff24e648f6da1f8d1f011e9cac26491b619e6b9280f2b47f1774e6ee2"
dependencies = [
"fnv",
"quick-error",
"tempfile",
"wait-timeout",
]
[[package]]
name = "ryu"
version = "1.0.20"
@ -1024,6 +1091,7 @@ dependencies = [
"log",
"matches",
"num_enum",
"proptest",
"prost",
"prost-build",
"rand 0.8.5",
@ -1109,6 +1177,12 @@ version = "1.18.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1dccffe3ce07af9386bfd29e80c0ab1a8205a2fc34e4bcd40364df902cfa8f3f"
[[package]]
name = "unarray"
version = "0.1.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94"
[[package]]
name = "unicode-ident"
version = "1.0.18"
@ -1136,6 +1210,15 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "wait-timeout"
version = "0.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11"
dependencies = [
"libc",
]
[[package]]
name = "wasi"
version = "0.11.0+wasi-snapshot-preview1"

View File

@ -32,6 +32,7 @@ galois_field_2pm = "0.1.0"
hex = "0.4"
hmac = "0.12.1"
matches = "0.1.10"
proptest = "1.7"
rand_08 = { package = "rand", version = "0.8" }
rand_distr = "0.5.1"

View File

@ -227,7 +227,7 @@ impl ChainEpochDirection {
fn next_key_internal(next: &mut [u8], ctr: &mut u32) -> (u32, [u8; 32]) {
assert!(!next.is_empty());
*ctr += 1;
let mut gen = [0u8; 64];
let mut genr8r = [0u8; 64];
kdf::hkdf_to_slice(
&[0u8; 32], // 32 is the hash output length
&*next,
@ -236,10 +236,10 @@ impl ChainEpochDirection {
b"Signal PQ Ratchet V1 Chain Next",
]
.concat(),
&mut gen,
&mut genr8r,
);
next.copy_from_slice(&gen[..32]);
(*ctr, gen[32..].try_into().expect("correct size"))
next.copy_from_slice(&genr8r[..32]);
(*ctr, genr8r[32..].try_into().expect("correct size"))
}
fn key(&mut self, at: u32, params: &pqrpb::ChainParams) -> Result<Vec<u8>, Error> {
@ -305,31 +305,31 @@ impl ChainEpochDirection {
#[hax_lib::attributes]
impl Chain {
#[hax_lib::requires(gen.len() == 96)]
fn ced_for_direction(gen: &[u8], dir: &Direction) -> ChainEpochDirection {
#[hax_lib::requires(genr8r.len() == 96)]
fn ced_for_direction(genr8r: &[u8], dir: &Direction) -> ChainEpochDirection {
ChainEpochDirection::new(match dir {
Direction::A2B => &gen[32..64],
Direction::B2A => &gen[64..96],
Direction::A2B => &genr8r[32..64],
Direction::B2A => &genr8r[64..96],
})
}
pub fn new(initial_key: &[u8], dir: Direction, params: ChainParamsPB) -> Result<Self, Error> {
let mut gen = [0u8; 96];
let mut genr8r = [0u8; 96];
kdf::hkdf_to_slice(
&[0u8; 32],
initial_key,
b"Signal PQ Ratchet V1 Chain Start",
&mut gen,
&mut genr8r,
);
Ok(Self {
dir,
current_epoch: 0,
send_epoch: 0,
links: VecDeque::from([ChainEpoch {
send: Self::ced_for_direction(&gen, &dir),
recv: Self::ced_for_direction(&gen, &dir.switch()),
send: Self::ced_for_direction(&genr8r, &dir),
recv: Self::ced_for_direction(&genr8r, &dir.switch()),
}]),
next_root: gen[0..32].to_vec(),
next_root: genr8r[0..32].to_vec(),
params,
})
}
@ -340,18 +340,18 @@ impl Chain {
self.current_epoch < u64::MAX && epoch_secret.epoch == self.current_epoch + 1
);
assert!(epoch_secret.epoch == self.current_epoch + 1);
let mut gen = [0u8; 96];
let mut genr8r = [0u8; 96];
kdf::hkdf_to_slice(
&self.next_root,
&epoch_secret.secret,
b"Signal PQ Ratchet V1 Chain Add Epoch",
&mut gen,
&mut genr8r,
);
self.current_epoch = epoch_secret.epoch;
self.next_root = gen[0..32].to_vec();
self.next_root = genr8r[0..32].to_vec();
self.links.push_back(ChainEpoch {
send: Self::ced_for_direction(&gen, &self.dir),
recv: Self::ced_for_direction(&gen, &self.dir.switch()),
send: Self::ced_for_direction(&genr8r, &self.dir),
recv: Self::ced_for_direction(&genr8r, &self.dir.switch()),
});
}
@ -443,8 +443,9 @@ impl Chain {
mod test {
use super::*;
use crate::{Direction, EpochSecret, Error};
use rand::seq::SliceRandom;
use proptest::prelude::*;
use rand::TryRngCore;
use rand::seq::SliceRandom;
#[test]
fn directions_match() {
@ -526,4 +527,167 @@ mod test {
Error::SendKeyEpochDecreased(1, 0)
));
}
#[derive(Clone, Debug)]
enum KeyHistoryAction {
AddNewNext,
AddNewSkip,
RequestStored(usize),
RequestNotStored(usize),
GarbageCollect,
}
impl KeyHistoryAction {
fn strategy() -> impl Strategy<Value = Self> {
proptest::prop_oneof![
Just(Self::AddNewNext),
Just(Self::AddNewSkip),
any::<usize>().prop_map(Self::RequestStored),
any::<usize>().prop_map(Self::RequestNotStored),
Just(Self::GarbageCollect),
]
}
}
#[test]
fn key_history_prop_test() {
let _ = env_logger::builder().is_test(true).try_init();
proptest!(|(actions in proptest::collection::vec(KeyHistoryAction::strategy(), ..25))| {
let mut kh = KeyHistory::new();
let mut stored = vec![];
let mut not_stored = vec![];
let mut ctr = 0u32;
let params = pqrpb::ChainParams {
max_ooo_keys: 3u32,
max_jump: 5u32,
};
log::debug!("========= STARTING =========");
for action in actions {
match action {
KeyHistoryAction::AddNewNext => {
log::debug!("adding {}", ctr);
kh.add((ctr, [1u8; 32]), &params);
stored.push(ctr);
ctr += 1;
}
KeyHistoryAction::AddNewSkip => {
log::debug!("skipping {}", ctr);
not_stored.push(ctr);
ctr += 1;
}
KeyHistoryAction::RequestStored(i) => {
if !stored.is_empty() {
let k = stored.swap_remove(i % stored.len());
log::debug!("requesting stored {}", k);
kh.get(k, ctr, &params).unwrap();
not_stored.push(k);
}
}
KeyHistoryAction::RequestNotStored(i) => {
if !not_stored.is_empty() {
let k = not_stored.swap_remove(i % not_stored.len());
log::debug!("requesting not stored {}", k);
kh.get(k, ctr, &params).unwrap_err();
}
}
KeyHistoryAction::GarbageCollect => {
log::debug!("gc at {}", ctr);
kh.gc(ctr, &params);
}
}
let mut fell_off = vec![];
(fell_off, stored) = stored.into_iter().partition(
|n| n + params.max_ooo_keys < ctr);
if !fell_off.is_empty() {
log::debug!("fell off: {:?}", fell_off);
}
not_stored.extend(fell_off.into_iter());
}
});
}
#[derive(Clone, Debug)]
enum CEDAction {
NextKey,
NextKeyAt(u32),
RequestStored(usize),
RequestNotStored(usize),
TooHigh,
}
impl CEDAction {
fn strategy() -> impl Strategy<Value = Self> {
proptest::prop_oneof![
Just(Self::NextKey),
any::<u32>().prop_map(Self::NextKeyAt),
any::<usize>().prop_map(Self::RequestStored),
any::<usize>().prop_map(Self::RequestNotStored),
Just(Self::TooHigh),
]
}
}
#[test]
fn ced_prop_test() {
let _ = env_logger::builder().is_test(true).try_init();
proptest!(|(actions in proptest::collection::vec(CEDAction::strategy(), ..25))| {
let mut ced = ChainEpochDirection::new(&[1u8; 32]);
let mut stored = vec![];
let mut not_stored = vec![0];
let mut ctr = 0u32;
let params = pqrpb::ChainParams {
max_ooo_keys: 3u32,
max_jump: 5u32,
};
log::debug!("========= STARTING =========");
for action in actions {
match action {
CEDAction::NextKey => {
ctr += 1;
log::debug!("next_key {}", ctr);
let k = ced.next_key().0;
not_stored.push(k);
}
CEDAction::NextKeyAt(i) => {
let jump = i % params.max_jump;
ctr += 1;
for at in ctr..ctr+jump {
stored.push(at);
}
ctr += jump;
log::debug!("next_key_at {}", ctr);
ced.key(ctr, &params).unwrap();
not_stored.push(ctr);
}
CEDAction::RequestStored(i) => {
if !stored.is_empty() {
let k = stored.swap_remove(i % stored.len());
log::debug!("requesting stored {}", k);
ced.key(k, &params).unwrap();
not_stored.push(k);
}
}
CEDAction::RequestNotStored(i) => {
if !not_stored.is_empty() {
let k = not_stored.swap_remove(i % not_stored.len());
log::debug!("requesting not stored {}", k);
ced.key(k, &params).unwrap_err();
}
}
CEDAction::TooHigh => {
let high = ctr + params.max_jump + 1;
log::debug!("too high {}", high);
ced.key(high, &params).unwrap_err();
}
}
let mut fell_off = vec![];
(fell_off, stored) = stored.into_iter().partition(
|n| n + params.max_ooo_keys < ctr);
if !fell_off.is_empty() {
log::debug!("fell off: {:?}", fell_off);
}
not_stored.extend(fell_off.into_iter());
}
});
}
}