sprints enhancements

src/Policy/__Tests/StellaOps.Policy.Engine.Tests/Properties/RiskBudgetMonotonicityPropertyTests.cs

@@ -37,7 +37,7 @@ public sealed class RiskBudgetMonotonicityPropertyTests
                     MaxNewCriticalVulnerabilities = budget1MaxCritical,
                     MaxNewHighVulnerabilities = int.MaxValue, // Allow high
                     MaxRiskScoreIncrease = decimal.MaxValue,
-                    MaxMagnitude = DeltaMagnitude.Catastrophic
+                    MaxMagnitude = DeltaMagnitude.Major // Most permissive
                 };
 
                 var budget2MaxCritical = Math.Max(0, budget1MaxCritical - reductionAmount);
@@ -72,7 +72,7 @@ public sealed class RiskBudgetMonotonicityPropertyTests
                     MaxNewCriticalVulnerabilities = int.MaxValue,
                     MaxNewHighVulnerabilities = budget1MaxHigh,
                     MaxRiskScoreIncrease = decimal.MaxValue,
-                    MaxMagnitude = DeltaMagnitude.Catastrophic
+                    MaxMagnitude = DeltaMagnitude.Major // Most permissive
                 };
 
                 var budget2MaxHigh = Math.Max(0, budget1MaxHigh - reductionAmount);
@@ -104,7 +104,7 @@ public sealed class RiskBudgetMonotonicityPropertyTests
                     MaxNewCriticalVulnerabilities = int.MaxValue,
                     MaxNewHighVulnerabilities = int.MaxValue,
                     MaxRiskScoreIncrease = budget1MaxScore,
-                    MaxMagnitude = DeltaMagnitude.Catastrophic
+                    MaxMagnitude = DeltaMagnitude.Major // Most permissive
                 };
 
                 var budget2MaxScore = Math.Max(0, budget1MaxScore - reductionAmount);
@@ -170,7 +170,7 @@ public sealed class RiskBudgetMonotonicityPropertyTests
                     MaxNewCriticalVulnerabilities = int.MaxValue,
                     MaxNewHighVulnerabilities = int.MaxValue,
                     MaxRiskScoreIncrease = decimal.MaxValue,
-                    MaxMagnitude = DeltaMagnitude.Catastrophic,
+                    MaxMagnitude = DeltaMagnitude.Major, // Most permissive
                     BlockedVulnerabilities = ImmutableHashSet<string>.Empty
                 };
 
@@ -233,6 +233,10 @@ public sealed class RiskBudgetMonotonicityPropertyTests
 /// </summary>
 internal static class DeltaVerdictArbs
 {
+    // DeltaMagnitude enum: None, Minimal, Small, Medium, Large, Major
+    // Mapping from old values:
+    //   Low -> Small, High -> Large, Severe -> Major, Catastrophic -> Major
+
     public static Arbitrary<int> NonNegativeInt() =>
         Arb.From(Gen.Choose(0, 50));
 
@@ -240,11 +244,10 @@ internal static class DeltaVerdictArbs
         Arb.From(Gen.Elements(
             DeltaMagnitude.None,
             DeltaMagnitude.Minimal,
-            DeltaMagnitude.Low,
+            DeltaMagnitude.Small,
             DeltaMagnitude.Medium,
-            DeltaMagnitude.High,
-            DeltaMagnitude.Severe,
-            DeltaMagnitude.Catastrophic));
+            DeltaMagnitude.Large,
+            DeltaMagnitude.Major));
 
     public static Arbitrary<DeltaVerdict.Models.DeltaVerdict> AnyDeltaVerdict() =>
         Arb.From(
@@ -254,11 +257,10 @@ internal static class DeltaVerdictArbs
             from magnitude in Gen.Elements(
                 DeltaMagnitude.None,
                 DeltaMagnitude.Minimal,
-                DeltaMagnitude.Low,
+                DeltaMagnitude.Small,
                 DeltaMagnitude.Medium,
-                DeltaMagnitude.High,
-                DeltaMagnitude.Severe,
-                DeltaMagnitude.Catastrophic)
+                DeltaMagnitude.Large,
+                DeltaMagnitude.Major)
             select CreateDeltaVerdict(criticalCount, highCount, riskScoreChange, magnitude));
 
     public static Arbitrary<RiskBudget> AnyRiskBudget() =>
@@ -269,11 +271,10 @@ internal static class DeltaVerdictArbs
             from maxMagnitude in Gen.Elements(
                 DeltaMagnitude.None,
                 DeltaMagnitude.Minimal,
-                DeltaMagnitude.Low,
+                DeltaMagnitude.Small,
                 DeltaMagnitude.Medium,
-                DeltaMagnitude.High,
-                DeltaMagnitude.Severe,
-                DeltaMagnitude.Catastrophic)
+                DeltaMagnitude.Large,
+                DeltaMagnitude.Major)
             select new RiskBudget
             {
                 MaxNewCriticalVulnerabilities = maxCritical,
@@ -292,35 +293,73 @@ internal static class DeltaVerdictArbs
 
         for (var i = 0; i < criticalCount; i++)
         {
+            // VulnerabilityDelta constructor: (VulnerabilityId, Severity, CvssScore?, ComponentPurl?, ReachabilityStatus?)
             addedVulns.Add(new VulnerabilityDelta(
-                $"CVE-2024-{1000 + i}",
-                "Critical",
-                9.8m,
-                VulnerabilityDeltaType.Added,
-                null));
+                VulnerabilityId: $"CVE-2024-{1000 + i}",
+                Severity: "Critical",
+                CvssScore: 9.8m,
+                ComponentPurl: null,
+                ReachabilityStatus: null));
         }
 
         for (var i = 0; i < highCount; i++)
         {
             addedVulns.Add(new VulnerabilityDelta(
-                $"CVE-2024-{2000 + i}",
-                "High",
-                7.5m,
-                VulnerabilityDeltaType.Added,
-                null));
+                VulnerabilityId: $"CVE-2024-{2000 + i}",
+                Severity: "High",
+                CvssScore: 7.5m,
+                ComponentPurl: null,
+                ReachabilityStatus: null));
         }
 
+        var now = DateTimeOffset.UtcNow;
+        var baseVerdict = new VerdictReference(
+            VerdictId: Guid.NewGuid().ToString(),
+            Digest: "sha256:baseline",
+            ArtifactRef: null,
+            ScannedAt: now.AddHours(-1));
+
+        var headVerdict = new VerdictReference(
+            VerdictId: Guid.NewGuid().ToString(),
+            Digest: "sha256:current",
+            ArtifactRef: null,
+            ScannedAt: now);
+
+        var trend = riskScoreChange > 0 ? RiskTrend.Degraded
+                  : riskScoreChange < 0 ? RiskTrend.Improved
+                  : RiskTrend.Stable;
+        var percentChange = riskScoreChange == 0 ? 0m : (decimal)riskScoreChange * 100m / 100m;
+
+        var riskDelta = new RiskScoreDelta(
+            OldScore: 0m,
+            NewScore: riskScoreChange,
+            Change: riskScoreChange,
+            PercentChange: percentChange,
+            Trend: trend);
+
+        var totalChanges = addedVulns.Count;
+        var summary = new DeltaSummary(
+            ComponentsAdded: 0,
+            ComponentsRemoved: 0,
+            ComponentsChanged: 0,
+            VulnerabilitiesAdded: addedVulns.Count,
+            VulnerabilitiesRemoved: 0,
+            VulnerabilityStatusChanges: 0,
+            TotalChanges: totalChanges,
+            Magnitude: magnitude);
+
         return new DeltaVerdict.Models.DeltaVerdict
         {
-            Id = Guid.NewGuid(),
-            Timestamp = DateTime.UtcNow,
-            BaselineDigest = "sha256:baseline",
-            CurrentDigest = "sha256:current",
-            AddedVulnerabilities = addedVulns,
+            DeltaId = Guid.NewGuid().ToString(),
+            SchemaVersion = "1.0.0",
+            BaseVerdict = baseVerdict,
+            HeadVerdict = headVerdict,
+            AddedVulnerabilities = addedVulns.ToImmutableArray(),
             RemovedVulnerabilities = [],
-            ChangedVulnerabilities = [],
-            RiskScoreDelta = new RiskScoreDelta(0, riskScoreChange, riskScoreChange),
-            Summary = new DeltaSummary(magnitude, addedVulns.Count, 0, 0)
+            ChangedVulnerabilityStatuses = [],
+            RiskScoreDelta = riskDelta,
+            Summary = summary,
+            ComputedAt = now
         };
     }
 }

src/Policy/__Tests/StellaOps.Policy.Engine.Tests/Properties/ScoreRuleMonotonicityPropertyTests.cs

@@ -0,0 +1,376 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+// SPDX-FileCopyrightText: 2025 StellaOps Contributors
+// Sprint: SPRINT_8200_0012_0003_policy_engine_integration
+// Task: PINT-8200-015 - Add property tests: rule monotonicity
+
+using System.Collections.Immutable;
+using FluentAssertions;
+using FsCheck;
+using FsCheck.Xunit;
+using StellaOps.Policy.Engine.Evaluation;
+using StellaOps.Policy.Exceptions.Models;
+using StellaOps.Policy.Unknowns.Models;
+using StellaOps.PolicyDsl;
+using StellaOps.Signals.EvidenceWeightedScore;
+using Xunit;
+
+namespace StellaOps.Policy.Engine.Tests.Properties;
+
+/// <summary>
+/// Property-based tests for score-based rule monotonicity.
+/// Verifies that higher scores lead to stricter verdicts when policies are configured
+/// with monotonic (score-threshold) rules.
+/// </summary>
+[Trait("Category", "Property")]
+[Trait("Sprint", "8200.0012.0003")]
+public sealed class ScoreRuleMonotonicityPropertyTests
+{
+    /// <summary>
+    /// Property: For threshold rules like "score >= T", increasing score cannot flip true→false.
+    /// If score S₁ satisfies (S₁ >= T), then any S₂ >= S₁ must also satisfy (S₂ >= T).
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property IncreasingScore_GreaterThanOrEqual_Monotonic()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.ThreeScores(),
+            values =>
+            {
+                var (threshold, score1, score2) = values;
+                var lowerScore = Math.Min(score1, score2);
+                var higherScore = Math.Max(score1, score2);
+
+                var expression = $"score >= {threshold}";
+                var evaluator1 = CreateEvaluator(lowerScore);
+                var evaluator2 = CreateEvaluator(higherScore);
+
+                var result1 = evaluator1.EvaluateBoolean(ParseExpression(expression));
+                var result2 = evaluator2.EvaluateBoolean(ParseExpression(expression));
+
+                // If lower score satisfies threshold, higher score must also
+                return (!result1 || result2)
+                    .Label($"score >= {threshold}: lower({lowerScore})={result1}, higher({higherScore})={result2}");
+            });
+    }
+
+    /// <summary>
+    /// Property: For threshold rules like "score > T", increasing score cannot flip true→false.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property IncreasingScore_GreaterThan_Monotonic()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.ThreeScores(),
+            values =>
+            {
+                var (threshold, score1, score2) = values;
+                var lowerScore = Math.Min(score1, score2);
+                var higherScore = Math.Max(score1, score2);
+
+                var expression = $"score > {threshold}";
+                var evaluator1 = CreateEvaluator(lowerScore);
+                var evaluator2 = CreateEvaluator(higherScore);
+
+                var result1 = evaluator1.EvaluateBoolean(ParseExpression(expression));
+                var result2 = evaluator2.EvaluateBoolean(ParseExpression(expression));
+
+                return (!result1 || result2)
+                    .Label($"score > {threshold}: lower({lowerScore})={result1}, higher({higherScore})={result2}");
+            });
+    }
+
+    /// <summary>
+    /// Property: For threshold rules like "score <= T", increasing score cannot flip false→true.
+    /// If S₁ violates (S₁ > T), then any S₂ >= S₁ must also violate.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property IncreasingScore_LessThanOrEqual_AntiMonotonic()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.ThreeScores(),
+            values =>
+            {
+                var (threshold, score1, score2) = values;
+                var lowerScore = Math.Min(score1, score2);
+                var higherScore = Math.Max(score1, score2);
+
+                var expression = $"score <= {threshold}";
+                var evaluator1 = CreateEvaluator(lowerScore);
+                var evaluator2 = CreateEvaluator(higherScore);
+
+                var result1 = evaluator1.EvaluateBoolean(ParseExpression(expression));
+                var result2 = evaluator2.EvaluateBoolean(ParseExpression(expression));
+
+                // If higher score violates threshold, lower score must also violate or pass
+                // Equivalently: if higher score passes, lower score must also pass
+                return (!result2 || result1)
+                    .Label($"score <= {threshold}: lower({lowerScore})={result1}, higher({higherScore})={result2}");
+            });
+    }
+
+    /// <summary>
+    /// Property: For between rules "score.between(min, max)",
+    /// scores within range always match, scores outside never match.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property ScoreBetween_RangeConsistency()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.ThreeScores(),
+            values =>
+            {
+                var (bound1, bound2, score) = values;
+                var min = Math.Min(bound1, bound2);
+                var max = Math.Max(bound1, bound2);
+
+                var expression = $"score.between({min}, {max})";
+                var evaluator = CreateEvaluator(score);
+
+                var result = evaluator.EvaluateBoolean(ParseExpression(expression));
+                var expectedInRange = score >= min && score <= max;
+
+                return (result == expectedInRange)
+                    .Label($"between({min}, {max}) with score={score}: got={result}, expected={expectedInRange}");
+            });
+    }
+
+    /// <summary>
+    /// Property: Bucket ordering is consistent with score ranges.
+    /// ActNow (highest urgency) should have highest scores.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property BucketFlags_ConsistentWithBucketValue()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.AnyBucket(),
+            bucket =>
+            {
+                var score = BucketToTypicalScore(bucket);
+                var evaluator = CreateEvaluatorWithBucket(score, bucket);
+
+                // Verify bucket flag matches
+                var bucketName = bucket.ToString().ToLowerInvariant();
+                var bucketExpression = bucketName switch
+                {
+                    "actnow" => "score.is_act_now",
+                    "schedulenext" => "score.is_schedule_next",
+                    _ => $"score.is_{bucketName}"
+                };
+
+                var result = evaluator.EvaluateBoolean(ParseExpression(bucketExpression));
+
+                return result
+                    .Label($"Bucket {bucket} flag should be true for score={score}");
+            });
+    }
+
+    /// <summary>
+    /// Property: Combining AND conditions with >= preserves monotonicity.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property AndConditions_PreserveMonotonicity()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.FourScores(),
+            values =>
+            {
+                var (threshold1, threshold2, score1, score2) = values;
+                var lowerScore = Math.Min(score1, score2);
+                var higherScore = Math.Max(score1, score2);
+
+                var expression = $"score >= {threshold1} and score >= {threshold2}";
+                var evaluator1 = CreateEvaluator(lowerScore);
+                var evaluator2 = CreateEvaluator(higherScore);
+
+                var result1 = evaluator1.EvaluateBoolean(ParseExpression(expression));
+                var result2 = evaluator2.EvaluateBoolean(ParseExpression(expression));
+
+                // If lower passes both thresholds, higher must also pass
+                return (!result1 || result2)
+                    .Label($"AND monotonicity: lower({lowerScore})={result1}, higher({higherScore})={result2}");
+            });
+    }
+
+    /// <summary>
+    /// Property: Combining OR conditions with >= preserves monotonicity.
+    /// </summary>
+    [Property(MaxTest = 100)]
+    public Property OrConditions_PreserveMonotonicity()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.FourScores(),
+            values =>
+            {
+                var (threshold1, threshold2, score1, score2) = values;
+                var lowerScore = Math.Min(score1, score2);
+                var higherScore = Math.Max(score1, score2);
+
+                var expression = $"score >= {threshold1} or score >= {threshold2}";
+                var evaluator1 = CreateEvaluator(lowerScore);
+                var evaluator2 = CreateEvaluator(higherScore);
+
+                var result1 = evaluator1.EvaluateBoolean(ParseExpression(expression));
+                var result2 = evaluator2.EvaluateBoolean(ParseExpression(expression));
+
+                // If lower passes either threshold, higher must also pass at least one
+                return (!result1 || result2)
+                    .Label($"OR monotonicity: lower({lowerScore})={result1}, higher({higherScore})={result2}");
+            });
+    }
+
+    /// <summary>
+    /// Property: Score equality is reflexive.
+    /// </summary>
+    [Property(MaxTest = 50)]
+    public Property ScoreEquality_IsReflexive()
+    {
+        return Prop.ForAll(
+            ScoreRuleArbs.ValidScore(),
+            score =>
+            {
+                var expression = $"score == {score}";
+                var evaluator = CreateEvaluator(score);
+                var result = evaluator.EvaluateBoolean(ParseExpression(expression));
+
+                return result
+                    .Label($"score == {score} should be true when score is {score}");
+            });
+    }
+
+    #region Helper Methods
+
+    private static PolicyExpressionEvaluator CreateEvaluator(int score)
+    {
+        var context = CreateTestContext();
+        var ewsResult = CreateTestScore(score, ScoreToBucket(score));
+        return new PolicyExpressionEvaluator(context, ewsResult);
+    }
+
+    private static PolicyExpressionEvaluator CreateEvaluatorWithBucket(int score, ScoreBucket bucket)
+    {
+        var context = CreateTestContext();
+        var ewsResult = CreateTestScore(score, bucket);
+        return new PolicyExpressionEvaluator(context, ewsResult);
+    }
+
+    private static ScoreBucket ScoreToBucket(int score) => score switch
+    {
+        >= 80 => ScoreBucket.ActNow,
+        >= 60 => ScoreBucket.ScheduleNext,
+        >= 40 => ScoreBucket.Investigate,
+        _ => ScoreBucket.Watchlist
+    };
+
+    private static int BucketToTypicalScore(ScoreBucket bucket) => bucket switch
+    {
+        ScoreBucket.ActNow => 90,
+        ScoreBucket.ScheduleNext => 70,
+        ScoreBucket.Investigate => 50,
+        ScoreBucket.Watchlist => 20,
+        _ => 50
+    };
+
+    private static PolicyEvaluationContext CreateTestContext()
+    {
+        return new PolicyEvaluationContext(
+            new PolicyEvaluationSeverity("High"),
+            new PolicyEvaluationEnvironment(ImmutableDictionary<string, string>.Empty
+                .Add("exposure", "internal")),
+            new PolicyEvaluationAdvisory("TEST", ImmutableDictionary<string, string>.Empty),
+            PolicyEvaluationVexEvidence.Empty,
+            PolicyEvaluationSbom.Empty,
+            PolicyEvaluationExceptions.Empty,
+            ImmutableArray<Unknown>.Empty,
+            ImmutableArray<ExceptionObject>.Empty,
+            PolicyEvaluationReachability.Unknown,
+            PolicyEvaluationEntropy.Unknown,
+            EvaluationTimestamp: DateTimeOffset.UtcNow);
+    }
+
+    private static EvidenceWeightedScoreResult CreateTestScore(int score, ScoreBucket bucket)
+    {
+        return new EvidenceWeightedScoreResult
+        {
+            FindingId = "test-finding",
+            Score = score,
+            Bucket = bucket,
+            Inputs = new EvidenceInputValues(0.5, 0.5, 0.5, 0.5, 0.5, 0.5),
+            Weights = new EvidenceWeights { Rch = 0.2, Rts = 0.15, Bkp = 0.1, Xpl = 0.25, Src = 0.1, Mit = 0.2 },
+            Breakdown = CreateDefaultBreakdown(),
+            Flags = [],
+            Explanations = [],
+            Caps = new AppliedGuardrails(),
+            PolicyDigest = "sha256:test-policy",
+            CalculatedAt = DateTimeOffset.UtcNow
+        };
+    }
+
+    private static List<DimensionContribution> CreateDefaultBreakdown()
+    {
+        return
+        [
+            new DimensionContribution { Dimension = "Reachability", Symbol = "RCH", InputValue = 0.5, Weight = 0.2, Contribution = 10, IsSubtractive = false },
+            new DimensionContribution { Dimension = "Runtime", Symbol = "RTS", InputValue = 0.5, Weight = 0.15, Contribution = 7.5, IsSubtractive = false },
+            new DimensionContribution { Dimension = "Backport", Symbol = "BKP", InputValue = 0.5, Weight = 0.1, Contribution = 5, IsSubtractive = false },
+            new DimensionContribution { Dimension = "Exploit", Symbol = "XPL", InputValue = 0.5, Weight = 0.25, Contribution = 12.5, IsSubtractive = false },
+            new DimensionContribution { Dimension = "SourceTrust", Symbol = "SRC", InputValue = 0.5, Weight = 0.1, Contribution = 5, IsSubtractive = false },
+            new DimensionContribution { Dimension = "Mitigation", Symbol = "MIT", InputValue = 0.5, Weight = 0.2, Contribution = -10, IsSubtractive = true }
+        ];
+    }
+
+    private static PolicyExpression ParseExpression(string expression)
+    {
+        var compiler = new PolicyCompiler();
+        var policySource = $$"""
+            policy "Test" syntax "stella-dsl@1" {
+              rule test { when {{expression}} then status := "matched" because "test" }
+            }
+            """;
+
+        var result = compiler.Compile(policySource);
+        if (!result.Success || result.Document is null)
+        {
+            throw new InvalidOperationException(
+                $"Failed to parse expression '{expression}': {string.Join(", ", result.Diagnostics.Select(i => i.Message))}");
+        }
+
+        return result.Document.Rules[0].When;
+    }
+
+    #endregion
+}
+
+/// <summary>
+/// Custom FsCheck arbitraries for score rule testing.
+/// </summary>
+internal static class ScoreRuleArbs
+{
+    /// <summary>Valid score range: 0-100.</summary>
+    public static Arbitrary<int> ValidScore() =>
+        Arb.From(Gen.Choose(0, 100));
+
+    /// <summary>Any valid bucket.</summary>
+    public static Arbitrary<ScoreBucket> AnyBucket() =>
+        Arb.From(Gen.Elements(
+            ScoreBucket.ActNow,
+            ScoreBucket.ScheduleNext,
+            ScoreBucket.Investigate,
+            ScoreBucket.Watchlist));
+
+    /// <summary>Combined tuple of 3 scores for ForAll parameter limit.</summary>
+    public static Arbitrary<(int, int, int)> ThreeScores() =>
+        Arb.From(
+            from s1 in Gen.Choose(0, 100)
+            from s2 in Gen.Choose(0, 100)
+            from s3 in Gen.Choose(0, 100)
+            select (s1, s2, s3));
+
+    /// <summary>Combined tuple of 4 scores for ForAll parameter limit.</summary>
+    public static Arbitrary<(int, int, int, int)> FourScores() =>
+        Arb.From(
+            from s1 in Gen.Choose(0, 100)
+            from s2 in Gen.Choose(0, 100)
+            from s3 in Gen.Choose(0, 100)
+            from s4 in Gen.Choose(0, 100)
+            select (s1, s2, s3, s4));
+}

src/Policy/__Tests/StellaOps.Policy.Engine.Tests/Properties/UnknownsBudgetPropertyTests.cs

@@ -100,12 +100,10 @@ public sealed class UnknownsBudgetPropertyTests
         return Prop.ForAll(
             UnknownsBudgetArbs.AnyUnknownsCounts(),
             UnknownsBudgetArbs.AnyUnknownsBudgetConfig(),
-            UnknownsBudgetArbs.NonNegativeInt(),
-            UnknownsBudgetArbs.NonNegativeInt(),
-            UnknownsBudgetArbs.NonNegativeInt(),
-            UnknownsBudgetArbs.NonNegativeInt(),
-            (counts, baseBudget, criticalReduction, highReduction, mediumReduction, lowReduction) =>
+            UnknownsBudgetArbs.AnyBudgetReductions(),
+            (counts, baseBudget, reductions) =>
             {
+                var (criticalReduction, highReduction, mediumReduction, lowReduction) = reductions;
                 var looserBudget = baseBudget with
                 {
                     MaxCriticalUnknowns = baseBudget.MaxCriticalUnknowns + criticalReduction,
@@ -302,6 +300,15 @@ internal static class UnknownsBudgetArbs
     public static Arbitrary<int> NonNegativeInt() =>
         Arb.From(Gen.Choose(0, 100));
 
+    /// <summary>Combined budget reductions tuple to stay within Prop.ForAll parameter limits.</summary>
+    public static Arbitrary<(int Critical, int High, int Medium, int Low)> AnyBudgetReductions() =>
+        Arb.From(
+            from critical in Gen.Choose(0, 100)
+            from high in Gen.Choose(0, 100)
+            from medium in Gen.Choose(0, 100)
+            from low in Gen.Choose(0, 100)
+            select (critical, high, medium, low));
+
     public static Arbitrary<UnknownsCounts> AnyUnknownsCounts() =>
         Arb.From(
             from critical in Gen.Choose(0, 20)

src/Policy/__Tests/StellaOps.Policy.Engine.Tests/Properties/VexLatticeMergePropertyTests.cs

@@ -64,7 +64,7 @@ public sealed class VexLatticeMergePropertyTests
     }
 
     /// <summary>
-    /// Property: Join with bottom (unknown) yields the other element - Join(a, unknown) = a.
+    /// Property: Join with bottom (UnderInvestigation) yields the other element - Join(a, bottom) = a.
     /// </summary>
     [Property(MaxTest = 100)]
     public Property Join_WithBottom_YieldsOther()
@@ -73,14 +73,14 @@ public sealed class VexLatticeMergePropertyTests
             VexLatticeArbs.AnyVexClaim(),
             a =>
             {
-                var bottom = VexLatticeArbs.CreateClaim(VexClaimStatus.Unknown);
+                var bottom = VexLatticeArbs.CreateClaim(VexLatticeArbs.BottomStatus);
                 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;
+                var expected = a.Status == VexLatticeArbs.BottomStatus ? VexLatticeArbs.BottomStatus : a.Status;
 
                 return (result.ResultStatus == expected)
-                    .Label($"Join({a.Status}, Unknown) = {result.ResultStatus}, expected {expected}");
+                    .Label($"Join({a.Status}, {VexLatticeArbs.BottomStatus}) = {result.ResultStatus}, expected {expected}");
             });
     }
 
@@ -143,7 +143,7 @@ public sealed class VexLatticeMergePropertyTests
     }
 
     /// <summary>
-    /// Property: Meet with bottom (unknown) yields bottom - Meet(a, unknown) = unknown.
+    /// Property: Meet with bottom (UnderInvestigation) yields bottom - Meet(a, bottom) = bottom.
     /// </summary>
     [Property(MaxTest = 100)]
     public Property Meet_WithBottom_YieldsBottom()
@@ -152,11 +152,11 @@ public sealed class VexLatticeMergePropertyTests
             VexLatticeArbs.AnyVexClaim(),
             a =>
             {
-                var bottom = VexLatticeArbs.CreateClaim(VexClaimStatus.Unknown);
+                var bottom = VexLatticeArbs.CreateClaim(VexLatticeArbs.BottomStatus);
                 var result = _lattice.Meet(a, bottom);
 
-                return (result.ResultStatus == VexClaimStatus.Unknown)
-                    .Label($"Meet({a.Status}, Unknown) = {result.ResultStatus}, expected Unknown");
+                return (result.ResultStatus == VexLatticeArbs.BottomStatus)
+                    .Label($"Meet({a.Status}, {VexLatticeArbs.BottomStatus}) = {result.ResultStatus}, expected {VexLatticeArbs.BottomStatus}");
             });
     }
 
@@ -287,7 +287,7 @@ public sealed class VexLatticeMergePropertyTests
     }
 
     /// <summary>
-    /// Property: Bottom element (Unknown) is not higher than any element.
+    /// Property: Bottom element (UnderInvestigation) is not higher than any element.
     /// </summary>
     [Property(MaxTest = 100)]
     public Property Bottom_IsNotHigherThanAnything()
@@ -296,13 +296,13 @@ public sealed class VexLatticeMergePropertyTests
             VexLatticeArbs.AnyVexClaimStatus(),
             a =>
             {
-                if (a == VexClaimStatus.Unknown)
+                if (a == VexLatticeArbs.BottomStatus)
                     return true.Label("Skip: comparing bottom with itself");
 
-                var result = _lattice.IsHigher(VexClaimStatus.Unknown, a);
+                var result = _lattice.IsHigher(VexLatticeArbs.BottomStatus, a);
 
                 return (!result)
-                    .Label($"IsHigher(Unknown, {a}) = {result}, expected false");
+                    .Label($"IsHigher({VexLatticeArbs.BottomStatus}, {a}) = {result}, expected false");
             });
     }
 
@@ -388,15 +388,19 @@ public sealed class VexLatticeMergePropertyTests
 /// </summary>
 internal static class VexLatticeArbs
 {
+    // Note: VexClaimStatus has 4 values: Affected, NotAffected, Fixed, UnderInvestigation.
+    // We treat UnderInvestigation as the "bottom" element (least certainty) in the K4 lattice.
     private static readonly VexClaimStatus[] AllStatuses =
     [
-        VexClaimStatus.Unknown,
+        VexClaimStatus.UnderInvestigation, // Bottom element (least certainty)
         VexClaimStatus.NotAffected,
         VexClaimStatus.Fixed,
-        VexClaimStatus.UnderInvestigation,
-        VexClaimStatus.Affected
+        VexClaimStatus.Affected // Top element (most certainty)
     ];
 
+    /// <summary>The bottom element in the K4 lattice (least certainty).</summary>
+    public static VexClaimStatus BottomStatus => VexClaimStatus.UnderInvestigation;
+
     public static Arbitrary<VexClaimStatus> AnyVexClaimStatus() =>
         Arb.From(Gen.Elements(AllStatuses));
 
@@ -413,45 +417,47 @@ internal static class VexLatticeArbs
         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
-        };
+        var firstSeen = new DateTimeOffset(now.AddDays(-30));
+        var lastSeenOffset = new DateTimeOffset(now);
+
+        var product = new VexProduct(
+            key: "test-product",
+            name: "Test Product",
+            version: "1.0.0");
+
+        var document = new VexClaimDocument(
+            format: VexDocumentFormat.OpenVex,
+            digest: $"sha256:{Guid.NewGuid():N}",
+            sourceUri: new Uri($"https://example.com/vex/{Guid.NewGuid()}"));
+
+        return new VexClaim(
+            vulnerabilityId: "CVE-2024-0001",
+            providerId: providerId,
+            product: product,
+            status: status,
+            document: document,
+            firstSeen: firstSeen,
+            lastSeen: lastSeenOffset);
     }
 }
 
 /// <summary>
 /// Default K4 lattice provider for testing.
-/// The K4 lattice: Unknown < {NotAffected, Fixed, UnderInvestigation} < Affected
+/// The K4 lattice: UnderInvestigation (bottom) < {NotAffected, Fixed} (middle) < Affected (top)
+/// UnderInvestigation represents the "unknown" state with least certainty.
 /// </summary>
 internal sealed class K4VexLatticeProvider : IVexLatticeProvider
 {
     private readonly ILogger<K4VexLatticeProvider> _logger;
 
     // K4 lattice ordering (higher value = higher in lattice)
+    // UnderInvestigation is bottom (least certainty), Affected is top (most certainty)
     private static readonly Dictionary<VexClaimStatus, int> LatticeOrder = new()
     {
-        [VexClaimStatus.Unknown] = 0,
-        [VexClaimStatus.NotAffected] = 1,
-        [VexClaimStatus.Fixed] = 1,
-        [VexClaimStatus.UnderInvestigation] = 1,
-        [VexClaimStatus.Affected] = 2
+        [VexClaimStatus.UnderInvestigation] = 0, // Bottom element (least certainty)
+        [VexClaimStatus.NotAffected] = 1,        // Middle tier
+        [VexClaimStatus.Fixed] = 1,              // Middle tier
+        [VexClaimStatus.Affected] = 2            // Top element (most certainty)
     };
 
     // Trust weights by provider type