// =============================================================================
// SourcePrecedenceLatticePropertyTests.cs
// Property-based tests for lattice properties
// Part of Task T25: Write property-based tests
// =============================================================================

using StellaOps.AirGap.Importer.Reconciliation;

namespace StellaOps.AirGap.Importer.Tests.Reconciliation;

/// <summary>
/// Property-based tests verifying lattice algebraic properties.
/// A lattice must satisfy: associativity, commutativity, idempotence, and absorption.
/// </summary>
public sealed class SourcePrecedenceLatticePropertyTests
{
    private static readonly SourcePrecedence[] AllPrecedences =
    [
        SourcePrecedence.Unknown,
        SourcePrecedence.ThirdParty,
        SourcePrecedence.Maintainer,
        SourcePrecedence.Vendor
    ];

    #region Lattice Algebraic Properties

    /// <summary>
    /// Property: Join is commutative - Join(a, b) = Join(b, a)
    /// </summary>
    [Fact]
    public void Join_IsCommutative()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var joinAB = SourcePrecedenceLattice.Join(a, b);
                var joinBA = SourcePrecedenceLattice.Join(b, a);

                Assert.Equal(joinAB, joinBA);
            }
        }
    }

    /// <summary>
    /// Property: Meet is commutative - Meet(a, b) = Meet(b, a)
    /// </summary>
    [Fact]
    public void Meet_IsCommutative()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var meetAB = SourcePrecedenceLattice.Meet(a, b);
                var meetBA = SourcePrecedenceLattice.Meet(b, a);

                Assert.Equal(meetAB, meetBA);
            }
        }
    }

    /// <summary>
    /// Property: Join is associative - Join(Join(a, b), c) = Join(a, Join(b, c))
    /// </summary>
    [Fact]
    public void Join_IsAssociative()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                foreach (var c in AllPrecedences)
                {
                    var left = SourcePrecedenceLattice.Join(SourcePrecedenceLattice.Join(a, b), c);
                    var right = SourcePrecedenceLattice.Join(a, SourcePrecedenceLattice.Join(b, c));

                    Assert.Equal(left, right);
                }
            }
        }
    }

    /// <summary>
    /// Property: Meet is associative - Meet(Meet(a, b), c) = Meet(a, Meet(b, c))
    /// </summary>
    [Fact]
    public void Meet_IsAssociative()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                foreach (var c in AllPrecedences)
                {
                    var left = SourcePrecedenceLattice.Meet(SourcePrecedenceLattice.Meet(a, b), c);
                    var right = SourcePrecedenceLattice.Meet(a, SourcePrecedenceLattice.Meet(b, c));

                    Assert.Equal(left, right);
                }
            }
        }
    }

    /// <summary>
    /// Property: Join is idempotent - Join(a, a) = a
    /// </summary>
    [Fact]
    public void Join_IsIdempotent()
    {
        foreach (var a in AllPrecedences)
        {
            var result = SourcePrecedenceLattice.Join(a, a);
            Assert.Equal(a, result);
        }
    }

    /// <summary>
    /// Property: Meet is idempotent - Meet(a, a) = a
    /// </summary>
    [Fact]
    public void Meet_IsIdempotent()
    {
        foreach (var a in AllPrecedences)
        {
            var result = SourcePrecedenceLattice.Meet(a, a);
            Assert.Equal(a, result);
        }
    }

    /// <summary>
    /// Property: Absorption law 1 - Join(a, Meet(a, b)) = a
    /// </summary>
    [Fact]
    public void Absorption_JoinMeet_ReturnsFirst()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var meet = SourcePrecedenceLattice.Meet(a, b);
                var result = SourcePrecedenceLattice.Join(a, meet);

                Assert.Equal(a, result);
            }
        }
    }

    /// <summary>
    /// Property: Absorption law 2 - Meet(a, Join(a, b)) = a
    /// </summary>
    [Fact]
    public void Absorption_MeetJoin_ReturnsFirst()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var join = SourcePrecedenceLattice.Join(a, b);
                var result = SourcePrecedenceLattice.Meet(a, join);

                Assert.Equal(a, result);
            }
        }
    }

    #endregion

    #region Ordering Properties

    /// <summary>
    /// Property: Compare is antisymmetric - if Compare(a,b) > 0 then Compare(b,a) < 0
    /// </summary>
    [Fact]
    public void Compare_IsAntisymmetric()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var compareAB = SourcePrecedenceLattice.Compare(a, b);
                var compareBA = SourcePrecedenceLattice.Compare(b, a);

                if (compareAB > 0)
                {
                    Assert.True(compareBA < 0);
                }
                else if (compareAB < 0)
                {
                    Assert.True(compareBA > 0);
                }
                else
                {
                    Assert.Equal(0, compareBA);
                }
            }
        }
    }

    /// <summary>
    /// Property: Compare is transitive - if Compare(a,b) > 0 and Compare(b,c) > 0 then Compare(a,c) > 0
    /// </summary>
    [Fact]
    public void Compare_IsTransitive()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                foreach (var c in AllPrecedences)
                {
                    var ab = SourcePrecedenceLattice.Compare(a, b);
                    var bc = SourcePrecedenceLattice.Compare(b, c);
                    var ac = SourcePrecedenceLattice.Compare(a, c);

                    if (ab > 0 && bc > 0)
                    {
                        Assert.True(ac > 0);
                    }

                    if (ab < 0 && bc < 0)
                    {
                        Assert.True(ac < 0);
                    }
                }
            }
        }
    }

    /// <summary>
    /// Property: Compare is reflexive - Compare(a, a) = 0
    /// </summary>
    [Fact]
    public void Compare_IsReflexive()
    {
        foreach (var a in AllPrecedences)
        {
            Assert.Equal(0, SourcePrecedenceLattice.Compare(a, a));
        }
    }

    #endregion

    #region Join/Meet Bound Properties

    /// <summary>
    /// Property: Join returns an upper bound - Join(a, b) >= a AND Join(a, b) >= b
    /// </summary>
    [Fact]
    public void Join_ReturnsUpperBound()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var join = SourcePrecedenceLattice.Join(a, b);

                Assert.True(SourcePrecedenceLattice.Compare(join, a) >= 0);
                Assert.True(SourcePrecedenceLattice.Compare(join, b) >= 0);
            }
        }
    }

    /// <summary>
    /// Property: Meet returns a lower bound - Meet(a, b) <= a AND Meet(a, b) <= b
    /// </summary>
    [Fact]
    public void Meet_ReturnsLowerBound()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var meet = SourcePrecedenceLattice.Meet(a, b);

                Assert.True(SourcePrecedenceLattice.Compare(meet, a) <= 0);
                Assert.True(SourcePrecedenceLattice.Compare(meet, b) <= 0);
            }
        }
    }

    /// <summary>
    /// Property: Join is least upper bound - for all c, if c >= a and c >= b then c >= Join(a,b)
    /// </summary>
    [Fact]
    public void Join_IsLeastUpperBound()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var join = SourcePrecedenceLattice.Join(a, b);

                foreach (var c in AllPrecedences)
                {
                    var cGeA = SourcePrecedenceLattice.Compare(c, a) >= 0;
                    var cGeB = SourcePrecedenceLattice.Compare(c, b) >= 0;

                    if (cGeA && cGeB)
                    {
                        Assert.True(SourcePrecedenceLattice.Compare(c, join) >= 0);
                    }
                }
            }
        }
    }

    /// <summary>
    /// Property: Meet is greatest lower bound - for all c, if c <= a and c <= b then c <= Meet(a,b)
    /// </summary>
    [Fact]
    public void Meet_IsGreatestLowerBound()
    {
        foreach (var a in AllPrecedences)
        {
            foreach (var b in AllPrecedences)
            {
                var meet = SourcePrecedenceLattice.Meet(a, b);

                foreach (var c in AllPrecedences)
                {
                    var cLeA = SourcePrecedenceLattice.Compare(c, a) <= 0;
                    var cLeB = SourcePrecedenceLattice.Compare(c, b) <= 0;

                    if (cLeA && cLeB)
                    {
                        Assert.True(SourcePrecedenceLattice.Compare(c, meet) <= 0);
                    }
                }
            }
        }
    }

    #endregion

    #region Bounded Lattice Properties

    /// <summary>
    /// Property: Unknown is the bottom element - Join(Unknown, a) = a
    /// </summary>
    [Fact]
    public void Unknown_IsBottomElement()
    {
        foreach (var a in AllPrecedences)
        {
            var result = SourcePrecedenceLattice.Join(SourcePrecedence.Unknown, a);
            Assert.Equal(a, result);
        }
    }

    /// <summary>
    /// Property: Vendor is the top element - Meet(Vendor, a) = a
    /// </summary>
    [Fact]
    public void Vendor_IsTopElement()
    {
        foreach (var a in AllPrecedences)
        {
            var result = SourcePrecedenceLattice.Meet(SourcePrecedence.Vendor, a);
            Assert.Equal(a, result);
        }
    }

    #endregion

    #region Merge Determinism

    /// <summary>
    /// Property: Merge is deterministic - same inputs always produce same output
    /// </summary>
    [Fact]
    public void Merge_IsDeterministic()
    {
        var lattice = new SourcePrecedenceLattice();
        var timestamp = new DateTimeOffset(2025, 12, 4, 12, 0, 0, TimeSpan.Zero);

        var statements = new[]
        {
            CreateStatement("CVE-2024-001", "product-1", VexStatus.Affected, SourcePrecedence.ThirdParty, timestamp),
            CreateStatement("CVE-2024-001", "product-1", VexStatus.NotAffected, SourcePrecedence.Vendor, timestamp),
            CreateStatement("CVE-2024-001", "product-1", VexStatus.Fixed, SourcePrecedence.Maintainer, timestamp)
        };

        // Run merge 100 times and verify same result
        var firstResult = lattice.Merge(statements);

        for (int i = 0; i < 100; i++)
        {
            var result = lattice.Merge(statements);

            Assert.Equal(firstResult.Status, result.Status);
            Assert.Equal(firstResult.Source, result.Source);
            Assert.Equal(firstResult.VulnerabilityId, result.VulnerabilityId);
        }
    }

    /// <summary>
    /// Property: Higher precedence always wins in merge
    /// </summary>
    [Fact]
    public void Merge_HigherPrecedenceWins()
    {
        var lattice = new SourcePrecedenceLattice();
        var timestamp = new DateTimeOffset(2025, 12, 4, 12, 0, 0, TimeSpan.Zero);

        // Vendor should win over ThirdParty
        var vendorStatement = CreateStatement("CVE-2024-001", "product-1", VexStatus.NotAffected, SourcePrecedence.Vendor, timestamp);
        var thirdPartyStatement = CreateStatement("CVE-2024-001", "product-1", VexStatus.Affected, SourcePrecedence.ThirdParty, timestamp);

        var result = lattice.Merge(vendorStatement, thirdPartyStatement);

        Assert.Equal(SourcePrecedence.Vendor, result.Source);
        Assert.Equal(VexStatus.NotAffected, result.Status);
    }

    /// <summary>
    /// Property: More recent timestamp wins when precedence is equal
    /// </summary>
    [Fact]
    public void Merge_MoreRecentTimestampWins_WhenPrecedenceEqual()
    {
        var lattice = new SourcePrecedenceLattice();
        var olderTimestamp = new DateTimeOffset(2025, 12, 1, 12, 0, 0, TimeSpan.Zero);
        var newerTimestamp = new DateTimeOffset(2025, 12, 4, 12, 0, 0, TimeSpan.Zero);

        var olderStatement = CreateStatement("CVE-2024-001", "product-1", VexStatus.Affected, SourcePrecedence.Maintainer, olderTimestamp);
        var newerStatement = CreateStatement("CVE-2024-001", "product-1", VexStatus.Fixed, SourcePrecedence.Maintainer, newerTimestamp);

        var result = lattice.Merge(olderStatement, newerStatement);

        Assert.Equal(VexStatus.Fixed, result.Status);
        Assert.Equal(newerTimestamp, result.Timestamp);
    }

    private static VexStatement CreateStatement(
        string vulnId,
        string productId,
        VexStatus status,
        SourcePrecedence source,
        DateTimeOffset? timestamp)
    {
        return new VexStatement
        {
            VulnerabilityId = vulnId,
            ProductId = productId,
            Status = status,
            Source = source,
            Timestamp = timestamp
        };
    }

    #endregion
}