// SPDX-License-Identifier: AGPL-3.0-or-later
// SPDX-FileCopyrightText: 2025 StellaOps Contributors

using FluentAssertions;
using FsCheck;
using FsCheck.Xunit;
using Microsoft.Extensions.Logging.Abstractions;
using StellaOps.Excititor.Core;
using StellaOps.Excititor.Core.Lattice;

namespace StellaOps.Policy.Engine.Tests.Properties;

/// <summary>
/// Property-based tests for VEX lattice merge semantics.
/// Verifies that join/meet operations satisfy lattice algebraic properties.
/// </summary>
public sealed class VexLatticeMergePropertyTests
{
    private readonly IVexLatticeProvider _lattice;

    public VexLatticeMergePropertyTests()
    {
        // Use the default K4 lattice provider
        _lattice = new K4VexLatticeProvider(NullLogger<K4VexLatticeProvider>.Instance);
    }

    #region Join Properties (Least Upper Bound)

    /// <summary>
    /// Property: Join is commutative - Join(a, b) = Join(b, a).
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Join_IsCommutative()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var joinAB = _lattice.Join(a, b);
                var joinBA = _lattice.Join(b, a);

                return (joinAB.ResultStatus == joinBA.ResultStatus)
                    .Label($"Join({a.Status}, {b.Status}) = {joinAB.ResultStatus}, Join({b.Status}, {a.Status}) = {joinBA.ResultStatus}");
            });
    }

    /// <summary>
    /// Property: Join is idempotent - Join(a, a) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Join_IsIdempotent()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var result = _lattice.Join(a, a);

                return (result.ResultStatus == a.Status)
                    .Label($"Join({a.Status}, {a.Status}) = {result.ResultStatus}, expected {a.Status}");
            });
    }

    /// <summary>
    /// Property: Join with bottom (unknown) yields the other element - Join(a, unknown) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Join_WithBottom_YieldsOther()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var bottom = VexLatticeArbs.CreateClaim(VexClaimStatus.Unknown);
                var result = _lattice.Join(a, bottom);

                // Join with bottom should yield the non-bottom element (or bottom if both are bottom)
                var expected = a.Status == VexClaimStatus.Unknown ? VexClaimStatus.Unknown : a.Status;

                return (result.ResultStatus == expected)
                    .Label($"Join({a.Status}, Unknown) = {result.ResultStatus}, expected {expected}");
            });
    }

    /// <summary>
    /// Property: Join with top (affected) yields top - Join(a, affected) = affected.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Join_WithTop_YieldsTop()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var top = VexLatticeArbs.CreateClaim(VexClaimStatus.Affected);
                var result = _lattice.Join(a, top);

                return (result.ResultStatus == VexClaimStatus.Affected)
                    .Label($"Join({a.Status}, Affected) = {result.ResultStatus}, expected Affected");
            });
    }

    #endregion

    #region Meet Properties (Greatest Lower Bound)

    /// <summary>
    /// Property: Meet is commutative - Meet(a, b) = Meet(b, a).
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Meet_IsCommutative()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var meetAB = _lattice.Meet(a, b);
                var meetBA = _lattice.Meet(b, a);

                return (meetAB.ResultStatus == meetBA.ResultStatus)
                    .Label($"Meet({a.Status}, {b.Status}) = {meetAB.ResultStatus}, Meet({b.Status}, {a.Status}) = {meetBA.ResultStatus}");
            });
    }

    /// <summary>
    /// Property: Meet is idempotent - Meet(a, a) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Meet_IsIdempotent()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var result = _lattice.Meet(a, a);

                return (result.ResultStatus == a.Status)
                    .Label($"Meet({a.Status}, {a.Status}) = {result.ResultStatus}, expected {a.Status}");
            });
    }

    /// <summary>
    /// Property: Meet with bottom (unknown) yields bottom - Meet(a, unknown) = unknown.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Meet_WithBottom_YieldsBottom()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var bottom = VexLatticeArbs.CreateClaim(VexClaimStatus.Unknown);
                var result = _lattice.Meet(a, bottom);

                return (result.ResultStatus == VexClaimStatus.Unknown)
                    .Label($"Meet({a.Status}, Unknown) = {result.ResultStatus}, expected Unknown");
            });
    }

    /// <summary>
    /// Property: Meet with top (affected) yields the other element - Meet(a, affected) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Meet_WithTop_YieldsOther()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            a =>
            {
                var top = VexLatticeArbs.CreateClaim(VexClaimStatus.Affected);
                var result = _lattice.Meet(a, top);

                var expected = a.Status == VexClaimStatus.Affected ? VexClaimStatus.Affected : a.Status;

                return (result.ResultStatus == expected)
                    .Label($"Meet({a.Status}, Affected) = {result.ResultStatus}, expected {expected}");
            });
    }

    #endregion

    #region Absorption Laws

    /// <summary>
    /// Property: Absorption law 1 - Join(a, Meet(a, b)) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Absorption_JoinMeet()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var meet = _lattice.Meet(a, b);
                var meetClaim = VexLatticeArbs.CreateClaim(meet.ResultStatus);
                var result = _lattice.Join(a, meetClaim);

                return (result.ResultStatus == a.Status)
                    .Label($"Join({a.Status}, Meet({a.Status}, {b.Status})) = {result.ResultStatus}, expected {a.Status}");
            });
    }

    /// <summary>
    /// Property: Absorption law 2 - Meet(a, Join(a, b)) = a.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Absorption_MeetJoin()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var join = _lattice.Join(a, b);
                var joinClaim = VexLatticeArbs.CreateClaim(join.ResultStatus);
                var result = _lattice.Meet(a, joinClaim);

                return (result.ResultStatus == a.Status)
                    .Label($"Meet({a.Status}, Join({a.Status}, {b.Status})) = {result.ResultStatus}, expected {a.Status}");
            });
    }

    #endregion

    #region IsHigher / Ordering Properties

    /// <summary>
    /// Property: IsHigher is antisymmetric - if a > b and b > a then a = b.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property IsHigher_IsAntisymmetric()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaimStatus(),
            VexLatticeArbs.AnyVexClaimStatus(),
            (a, b) =>
            {
                var aHigherB = _lattice.IsHigher(a, b);
                var bHigherA = _lattice.IsHigher(b, a);

                // If both are true, they must be equal
                return (!(aHigherB && bHigherA) || a == b)
                    .Label($"IsHigher({a}, {b}) = {aHigherB}, IsHigher({b}, {a}) = {bHigherA}");
            });
    }

    /// <summary>
    /// Property: IsHigher is reflexive for equality - IsHigher(a, a) is well-defined.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property IsHigher_IsReflexive()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaimStatus(),
            a =>
            {
                var result = _lattice.IsHigher(a, a);

                // Same status should not be "higher" than itself
                return (!result)
                    .Label($"IsHigher({a}, {a}) = {result}, expected false");
            });
    }

    /// <summary>
    /// Property: Top element (Affected) is higher than all non-top elements.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Top_IsHigherThanAllNonTop()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaimStatus(),
            a =>
            {
                if (a == VexClaimStatus.Affected)
                    return true.Label("Skip: comparing top with itself");

                var result = _lattice.IsHigher(VexClaimStatus.Affected, a);

                return result
                    .Label($"IsHigher(Affected, {a}) = {result}, expected true");
            });
    }

    /// <summary>
    /// Property: Bottom element (Unknown) is not higher than any element.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property Bottom_IsNotHigherThanAnything()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaimStatus(),
            a =>
            {
                if (a == VexClaimStatus.Unknown)
                    return true.Label("Skip: comparing bottom with itself");

                var result = _lattice.IsHigher(VexClaimStatus.Unknown, a);

                return (!result)
                    .Label($"IsHigher(Unknown, {a}) = {result}, expected false");
            });
    }

    #endregion

    #region Conflict Resolution Properties

    /// <summary>
    /// Property: Conflict resolution always produces a valid winner.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property ConflictResolution_ProducesValidWinner()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var resolution = _lattice.ResolveConflict(a, b);

                // Winner must be one of the inputs
                var winnerIsValid = resolution.Winner.Status == a.Status || resolution.Winner.Status == b.Status;

                return winnerIsValid
                    .Label($"Winner status {resolution.Winner.Status} must be {a.Status} or {b.Status}");
            });
    }

    /// <summary>
    /// Property: Conflict resolution is deterministic.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property ConflictResolution_IsDeterministic()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var resolution1 = _lattice.ResolveConflict(a, b);
                var resolution2 = _lattice.ResolveConflict(a, b);

                return (resolution1.Winner.Status == resolution2.Winner.Status &&
                        resolution1.Reason == resolution2.Reason)
                    .Label($"Determinism: {resolution1.Winner.Status}/{resolution1.Reason} vs {resolution2.Winner.Status}/{resolution2.Reason}");
            });
    }

    /// <summary>
    /// Property: Higher trust weight wins in conflict.
    /// </summary>
    [Property(MaxTest = 100)]
    public Property ConflictResolution_HigherTrustWins()
    {
        return Prop.ForAll(
            VexLatticeArbs.AnyVexClaim(),
            VexLatticeArbs.AnyVexClaim(),
            (a, b) =>
            {
                var trustA = _lattice.GetTrustWeight(a);
                var trustB = _lattice.GetTrustWeight(b);
                var resolution = _lattice.ResolveConflict(a, b);

                // If trust weights differ significantly, higher should win
                if (Math.Abs(trustA - trustB) > 0.01m)
                {
                    var expectedWinner = trustA > trustB ? a : b;
                    return (resolution.Winner.Status == expectedWinner.Status ||
                            resolution.Reason != ConflictResolutionReason.TrustWeight)
                        .Label($"Trust: A={trustA}, B={trustB}, Winner={resolution.Winner.Status}");
                }

                // Otherwise, any result is acceptable
                return true.Label("Trust weights equal, any result acceptable");
            });
    }

    #endregion
}

/// <summary>
/// Custom FsCheck arbitraries for VEX lattice types.
/// </summary>
internal static class VexLatticeArbs
{
    private static readonly VexClaimStatus[] AllStatuses =
    [
        VexClaimStatus.Unknown,
        VexClaimStatus.NotAffected,
        VexClaimStatus.Fixed,
        VexClaimStatus.UnderInvestigation,
        VexClaimStatus.Affected
    ];

    public static Arbitrary<VexClaimStatus> AnyVexClaimStatus() =>
        Arb.From(Gen.Elements(AllStatuses));

    public static Arbitrary<VexClaim> AnyVexClaim() =>
        Arb.From(
            from status in Gen.Elements(AllStatuses)
            from providerId in Gen.Elements("vendor", "maintainer", "third-party", "scanner")
            from dayOffset in Gen.Choose(0, 365)
            select CreateClaim(status, providerId, DateTime.UtcNow.AddDays(-dayOffset)));

    public static VexClaim CreateClaim(
        VexClaimStatus status,
        string providerId = "test-provider",
        DateTime? lastSeen = null)
    {
        var now = lastSeen ?? DateTime.UtcNow;
        return new VexClaim
        {
            VulnerabilityId = "CVE-2024-0001",
            Status = status,
            ProviderId = providerId,
            Product = new VexProduct
            {
                Key = "test-product",
                Name = "Test Product",
                Version = "1.0.0"
            },
            Document = new VexDocumentSource
            {
                SourceUri = new Uri($"https://example.com/vex/{Guid.NewGuid()}"),
                Digest = $"sha256:{Guid.NewGuid():N}",
                Format = VexFormat.OpenVex
            },
            FirstSeen = now.AddDays(-30),
            LastSeen = now
        };
    }
}

/// <summary>
/// Default K4 lattice provider for testing.
/// The K4 lattice: Unknown < {NotAffected, Fixed, UnderInvestigation} < Affected
/// </summary>
internal sealed class K4VexLatticeProvider : IVexLatticeProvider
{
    private readonly ILogger<K4VexLatticeProvider> _logger;

    // K4 lattice ordering (higher value = higher in lattice)
    private static readonly Dictionary<VexClaimStatus, int> LatticeOrder = new()
    {
        [VexClaimStatus.Unknown] = 0,
        [VexClaimStatus.NotAffected] = 1,
        [VexClaimStatus.Fixed] = 1,
        [VexClaimStatus.UnderInvestigation] = 1,
        [VexClaimStatus.Affected] = 2
    };

    // Trust weights by provider type
    private static readonly Dictionary<string, decimal> TrustWeights = new(StringComparer.OrdinalIgnoreCase)
    {
        ["vendor"] = 1.0m,
        ["maintainer"] = 0.9m,
        ["third-party"] = 0.7m,
        ["scanner"] = 0.5m
    };

    public K4VexLatticeProvider(ILogger<K4VexLatticeProvider> logger)
    {
        _logger = logger;
    }

    public VexLatticeResult Join(VexClaim left, VexClaim right)
    {
        var leftOrder = LatticeOrder.GetValueOrDefault(left.Status, 0);
        var rightOrder = LatticeOrder.GetValueOrDefault(right.Status, 0);

        if (leftOrder >= rightOrder)
        {
            return new VexLatticeResult(left.Status, left, "Left is higher or equal in lattice", null);
        }

        return new VexLatticeResult(right.Status, right, "Right is higher in lattice", null);
    }

    public VexLatticeResult Meet(VexClaim left, VexClaim right)
    {
        var leftOrder = LatticeOrder.GetValueOrDefault(left.Status, 0);
        var rightOrder = LatticeOrder.GetValueOrDefault(right.Status, 0);

        if (leftOrder <= rightOrder)
        {
            return new VexLatticeResult(left.Status, left, "Left is lower or equal in lattice", null);
        }

        return new VexLatticeResult(right.Status, right, "Right is lower in lattice", null);
    }

    public bool IsHigher(VexClaimStatus a, VexClaimStatus b)
    {
        var aOrder = LatticeOrder.GetValueOrDefault(a, 0);
        var bOrder = LatticeOrder.GetValueOrDefault(b, 0);
        return aOrder > bOrder;
    }

    public decimal GetTrustWeight(VexClaim statement)
    {
        return TrustWeights.GetValueOrDefault(statement.ProviderId, 0.5m);
    }

    public VexConflictResolution ResolveConflict(VexClaim left, VexClaim right)
    {
        var leftTrust = GetTrustWeight(left);
        var rightTrust = GetTrustWeight(right);

        ConflictResolutionReason reason;
        VexClaim winner;
        VexClaim loser;

        if (Math.Abs(leftTrust - rightTrust) > 0.01m)
        {
            winner = leftTrust > rightTrust ? left : right;
            loser = leftTrust > rightTrust ? right : left;
            reason = ConflictResolutionReason.TrustWeight;
        }
        else if (left.LastSeen != right.LastSeen)
        {
            winner = left.LastSeen > right.LastSeen ? left : right;
            loser = left.LastSeen > right.LastSeen ? right : left;
            reason = ConflictResolutionReason.Freshness;
        }
        else
        {
            var leftOrder = LatticeOrder.GetValueOrDefault(left.Status, 0);
            var rightOrder = LatticeOrder.GetValueOrDefault(right.Status, 0);
            winner = leftOrder >= rightOrder ? left : right;
            loser = leftOrder >= rightOrder ? right : left;
            reason = leftOrder != rightOrder ? ConflictResolutionReason.LatticePosition : ConflictResolutionReason.Tie;
        }

        return new VexConflictResolution(winner, loser, reason, new MergeTrace
        {
            LeftSource = left.ProviderId,
            RightSource = right.ProviderId,
            LeftStatus = left.Status,
            RightStatus = right.Status,
            LeftTrust = leftTrust,
            RightTrust = rightTrust,
            ResultStatus = winner.Status,
            Explanation = $"Resolved by {reason}: {winner.Status} from {winner.ProviderId}",
            EvaluatedAt = DateTimeOffset.UtcNow
        });
    }
}