//! Kani proofs for GDPR consent and purpose tracking
//!
//! These proofs verify correctness properties of consent management
//! using bounded model checking.
//!
//! **Proof Count**: 3 proofs (#41-43)
//!
//! Run with: `cargo kani --tests --harness verify_*`

#[cfg(kani)]
use crate::classification::DataClass;
#[cfg(kani)]
use crate::consent::{ConsentRecord, ConsentScope, ConsentTracker};
#[cfg(kani)]
use crate::purpose::Purpose;
#[cfg(kani)]
use crate::validator::ConsentValidator;

/// Proof #41: Consent grant/withdraw correctness
///
/// **Property**: Withdrawn consent is never valid
///
/// **Verification**:
/// - Grant consent for any subject/purpose
/// - Withdraw the consent
/// - Verify is_valid() returns false
/// - Verify tracker reports it as withdrawn
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn verify_consent_withdraw_correctness() {
    let mut tracker = ConsentTracker::new();

    // Grant consent (symbolically)
    let subject_id = "user@example.com";
    let purpose = Purpose::Marketing;

    let consent_id = tracker.grant_consent(subject_id, purpose).unwrap();

    // Precondition: Consent is initially valid
    let record_before = tracker.get_consent(consent_id).unwrap();
    assert!(record_before.is_valid());
    assert!(!record_before.is_withdrawn());

    // Withdraw consent
    tracker.withdraw_consent(consent_id).unwrap();

    // Postcondition 1: Consent is now invalid
    let record_after = tracker.get_consent(consent_id).unwrap();
    assert!(!record_after.is_valid());

    // Postcondition 2: Consent is marked as withdrawn
    assert!(record_after.is_withdrawn());

    // Postcondition 3: withdrawn_at timestamp is set
    assert!(record_after.withdrawn_at.is_some());

    // Postcondition 4: Cannot query with withdrawn consent
    assert!(!tracker.check_consent(subject_id, purpose));
}

/// Proof #42: Purpose validation for data classes
///
/// **Property**: Invalid purpose/data class combinations are rejected
///
/// **Verification**:
/// - Marketing purpose + PHI data class → Should fail
/// - Marketing purpose + PCI data class → Should fail
/// - Contractual purpose + PHI data class → Should succeed
/// - Security purpose + all data classes → Should succeed
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(10)]
fn verify_purpose_validation() {
    // Test 1: Marketing not allowed for PHI (HIPAA violation)
    assert!(!Purpose::Marketing.is_valid_for(DataClass::PHI));

    // Test 2: Marketing not allowed for PCI (PCI DSS violation)
    assert!(!Purpose::Marketing.is_valid_for(DataClass::PCI));

    // Test 3: Contractual allowed for PHI (healthcare delivery)
    assert!(Purpose::Contractual.is_valid_for(DataClass::PHI));

    // Test 4: Security allowed for all (fraud prevention)
    assert!(Purpose::Security.is_valid_for(DataClass::PHI));
    assert!(Purpose::Security.is_valid_for(DataClass::PCI));
    assert!(Purpose::Security.is_valid_for(DataClass::PII));
    assert!(Purpose::Security.is_valid_for(DataClass::Sensitive));

    // Test 5: Public data allows all purposes
    assert!(Purpose::Marketing.is_valid_for(DataClass::Public));
    assert!(Purpose::Analytics.is_valid_for(DataClass::Public));
}

/// Proof #43: Consent validator enforcement
///
/// **Property**: Validator rejects queries without required consent
///
/// **Verification**:
/// - Purpose requiring consent + no consent granted → Rejected
/// - Purpose requiring consent + consent granted → Allowed
/// - Purpose not requiring consent + no consent → Allowed
/// - Valid purpose + consent withdrawn → Rejected
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(8)]
fn verify_consent_validator_enforcement() {
    let mut validator = ConsentValidator::new();
    let subject_id = "user@example.com";

    // Test 1: Marketing requires consent, none granted → Reject
    let result = validator.validate_query(subject_id, Purpose::Marketing, DataClass::PII);
    assert!(result.is_err());

    // Test 2: Grant consent → Allow
    validator
        .grant_consent(subject_id, Purpose::Marketing)
        .unwrap();
    let result = validator.validate_query(subject_id, Purpose::Marketing, DataClass::PII);
    assert!(result.is_ok());

    // Test 3: Contractual doesn't require consent → Allow
    let result = validator.validate_query(subject_id, Purpose::Contractual, DataClass::PII);
    assert!(result.is_ok());

    // Test 4: Invalid purpose/data class combination → Reject
    validator
        .grant_consent(subject_id, Purpose::Analytics)
        .unwrap();
    let result = validator.validate_query(
        subject_id,
        Purpose::Marketing, // Marketing + PHI invalid
        DataClass::PHI,
    );
    assert!(result.is_err());
}

/// Proof #44 (Bonus): Consent expiry handling
///
/// **Property**: Expired consent is treated as invalid
///
/// **Verification**:
/// - Create consent record
/// - Set expiry to past timestamp
/// - Verify is_valid() returns false
/// - Verify is_expired() returns true
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(3)]
fn verify_consent_expiry() {
    let mut record = ConsentRecord::new(
        "user@example.com".to_string(),
        Purpose::Marketing,
        ConsentScope::AllData,
    );

    // Initially valid (no expiry)
    assert!(record.is_valid());
    assert!(!record.is_expired());

    // Set expiry to past (simulated)
    record.expires_at = Some(chrono::Utc::now() - chrono::Duration::days(1));

    // Now invalid due to expiry
    assert!(!record.is_valid());
    assert!(record.is_expired());
}

/// Proof #45 (Bonus): Multiple consents per subject
///
/// **Property**: Subject can have multiple valid consents for different purposes
///
/// **Verification**:
/// - Grant Marketing consent
/// - Grant Analytics consent
/// - Both can be checked independently
/// - Withdrawing one doesn't affect the other
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(10)]
fn verify_multiple_consents() {
    let mut tracker = ConsentTracker::new();
    let subject_id = "user@example.com";

    // Grant two consents
    let marketing_id = tracker
        .grant_consent(subject_id, Purpose::Marketing)
        .unwrap();
    let analytics_id = tracker
        .grant_consent(subject_id, Purpose::Analytics)
        .unwrap();

    // Both are valid
    assert!(tracker.check_consent(subject_id, Purpose::Marketing));
    assert!(tracker.check_consent(subject_id, Purpose::Analytics));

    // Withdraw Marketing
    tracker.withdraw_consent(marketing_id).unwrap();

    // Marketing invalid, Analytics still valid
    assert!(!tracker.check_consent(subject_id, Purpose::Marketing));
    assert!(tracker.check_consent(subject_id, Purpose::Analytics));

    // Withdraw Analytics
    tracker.withdraw_consent(analytics_id).unwrap();

    // Both invalid
    assert!(!tracker.check_consent(subject_id, Purpose::Marketing));
    assert!(!tracker.check_consent(subject_id, Purpose::Analytics));
}

/// Proof #45b (M-5): Consent tracker isolates subjects
///
/// **AUDIT-2026-04 M-5.** Proofs #41–45 all use a single hard-coded
/// `SUBJECT` constant, so every isolation property has historically
/// been trivially true — a shared-keyed consent store with
/// `HashMap<Purpose, ConsentId>` would pass them all. This proof
/// constructs two distinct subject identifiers and asserts that
/// withdrawing subject A's consent has no effect on subject B's
/// same-purpose consent.
///
/// **Property**: Consent state is keyed per (subject, purpose); two
/// subjects sharing a purpose are not linked.
///
/// **Verification**:
/// - Grant Marketing consent to subjects A and B (distinct IDs).
/// - Assert both are initially valid.
/// - Withdraw A's consent.
/// - Assert B's consent remains valid — the withdraw must not leak
///   across the subject boundary.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(10)]
fn verify_consent_per_subject_isolation() {
    let mut tracker = ConsentTracker::new();

    let subject_a = "alice@example.com";
    let subject_b = "bob@example.com";

    let a_id = tracker
        .grant_consent(subject_a, Purpose::Marketing)
        .unwrap();
    let _b_id = tracker
        .grant_consent(subject_b, Purpose::Marketing)
        .unwrap();

    // Precondition: both subjects have valid consent.
    assert!(tracker.check_consent(subject_a, Purpose::Marketing));
    assert!(tracker.check_consent(subject_b, Purpose::Marketing));

    // Withdraw A's consent only.
    tracker.withdraw_consent(a_id).unwrap();

    // Postcondition: A is withdrawn, B is untouched.
    assert!(!tracker.check_consent(subject_a, Purpose::Marketing));
    assert!(tracker.check_consent(subject_b, Purpose::Marketing));
}

// ============================================================================
// Export Module Proofs (#50-52)
// ============================================================================

#[cfg(kani)]
use crate::export::{ExportEngine, ExportFormat, ExportRecord};

/// Proof #50: Export content hash is non-zero for non-empty data
///
/// **Property**: A non-empty export always produces a non-genesis content hash
///
/// **Verification**:
/// - Export records in JSON format
/// - Content hash must not be all zeros
/// - Record count must match input
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn verify_export_content_hash_nonzero() {
    let mut engine = ExportEngine::new();

    let records = vec![ExportRecord {
        stream_id: kimberlite_types::StreamId::new(1),
        stream_name: "test_stream".to_string(),
        offset: 0,
        data: serde_json::json!({"field": "value"}),
        timestamp: chrono::Utc::now(),
    }];

    let export = engine
        .export_subject_data("user@example.com", &records, ExportFormat::Json, "system")
        .unwrap();

    // Postcondition: content hash is not genesis (all zeros)
    assert!(!export.content_hash.is_genesis());

    // Postcondition: record count matches
    assert_eq!(export.record_count, 1);
}

/// Proof #51: Export audit trail completeness
///
/// **Property**: Every export creates exactly one audit record
///
/// **Verification**:
/// - Start with empty audit trail
/// - Export subject data
/// - Audit trail contains exactly one record with matching fields
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn verify_export_audit_trail() {
    let mut engine = ExportEngine::new();

    // Precondition: empty audit trail
    assert!(engine.get_audit_trail().is_empty());

    let records = vec![ExportRecord {
        stream_id: kimberlite_types::StreamId::new(1),
        stream_name: "patients".to_string(),
        offset: 0,
        data: serde_json::json!({"name": "Jane"}),
        timestamp: chrono::Utc::now(),
    }];

    let export = engine
        .export_subject_data("user@example.com", &records, ExportFormat::Json, "system")
        .unwrap();

    // Postcondition: exactly one audit record
    let trail = engine.get_audit_trail();
    assert_eq!(trail.len(), 1);

    // Postcondition: audit record matches export
    assert_eq!(trail[0].export_id, export.export_id);
    assert_eq!(trail[0].subject_id, "user@example.com");
    assert_eq!(trail[0].record_count, export.record_count);
    assert_eq!(trail[0].content_hash, export.content_hash);
}

/// Proof #52: HMAC signature correctness
///
/// **Property**: Signing and verifying with the same key succeeds;
/// verifying with a different key fails
///
/// **Verification**:
/// - Export and sign with key A
/// - Verify with key A → true
/// - Verify with key B → false
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn verify_export_signature_correctness() {
    let mut engine = ExportEngine::new();
    let key_a = b"correct-key-for-signing-abcdefgh";
    let key_b = b"wrong-key-should-fail-verify!!!!";

    let records = vec![ExportRecord {
        stream_id: kimberlite_types::StreamId::new(1),
        stream_name: "test".to_string(),
        offset: 0,
        data: serde_json::json!({"x": 1}),
        timestamp: chrono::Utc::now(),
    }];

    let export = engine
        .export_subject_data("user@example.com", &records, ExportFormat::Json, "system")
        .unwrap();
    let export_id = export.export_id;

    // Sign with key A
    engine.sign_export(export_id, key_a).unwrap();
    let signed = engine.get_export(export_id).unwrap();

    // Verify with correct key → true
    let data = ExportEngine::format_as_json(&records).unwrap();
    let valid = ExportEngine::verify_export_signature(signed, &data, key_a).unwrap();
    assert!(valid);

    // Verify with wrong key → false
    let invalid = ExportEngine::verify_export_signature(signed, &data, key_b).unwrap();
    assert!(!invalid);
}

#[cfg(test)]
mod tests {
    #[test]
    fn test_proof_count() {
        // This test documents that we have 8 Kani proofs (#41-45 consent, #50-52 export)
        let proof_count = 8;
        assert_eq!(
            proof_count, 8,
            "Expected 8 Kani proofs for compliance crate"
        );
    }
}
