base64-ng 2.0.1

use super::v2::{
    secret::{SecretArrayFrame, SecretDecodeError, SecretFrame, SecretInput},
    specifications::STRICT_STANDARD_PADDED,
};

#[kani::proof]
#[kani::unwind(70)]
fn secret_frame_never_releases_more_than_its_bound() {
    let input = kani::any::<[u8; 4]>();
    let mut frame = SecretArrayFrame::<3>::new(&STRICT_STANDARD_PADDED)
        .expect("strict policy and bounded frame are valid");
    let progress = frame
        .update(&SecretInput::new(&input))
        .expect("one padded quantum fits the public bound");
    assert!(progress.input_consumed() == input.len());
    assert!(progress.output_produced() == 0);
    if let Ok(secret) = frame.finish() {
        assert!(secret.len() <= 3);
        assert!(
            secret.backing_for_proof()[secret.len()..]
                .iter()
                .all(|byte| *byte == 0)
        );
    }
}

#[kani::proof]
fn secret_frame_rejects_oversized_input_before_scanning() {
    let mut frame = SecretArrayFrame::<3>::new(&STRICT_STANDARD_PADDED)
        .expect("strict policy and bounded frame are valid");
    let error = frame
        .update(&SecretInput::new(b"QUJDRA=="))
        .expect_err("eight encoded bytes exceed a three-byte frame");
    assert!(matches!(error, SecretDecodeError::InputTooLarge { .. }));
    assert!(frame.state().is_failed());
}

#[kani::proof]
#[kani::unwind(70)]
fn borrowed_secret_frame_writes_public_output_only_after_valid_gate() {
    let input = if kani::any::<bool>() {
        *b"QQ=="
    } else {
        *b"Q!=="
    };
    let mut staging = [0xa5; 3];
    let mut output = [0xa5; 3];
    let accepted = {
        let mut frame = SecretFrame::new(&STRICT_STANDARD_PADDED, 3, &mut staging, &mut output)
            .expect("fixed ranges are disjoint and sufficient");
        frame
            .update(&SecretInput::new(&input))
            .expect("one padded quantum fits the public bound");
        match frame.finish() {
            Ok(secret) => {
                assert!(secret.len() <= 3);
                drop(secret);
                true
            }
            Err(SecretDecodeError::InvalidInput) => false,
            Err(error) => panic!("unexpected public-frame proof result: {error}"),
        }
    };
    assert!(staging.iter().all(|byte| *byte == 0));
    assert!(output.iter().all(|byte| *byte == 0));
    kani::cover!(accepted, "valid input reaches the release gate");
    kani::cover!(!accepted, "invalid input wipes without release");
}