Add verifier process supervisor and broaden analyzer/contracts/effects coverage

.editorconfig

@@ -39,6 +39,18 @@ dotnet_style_collection_initializer = true:suggestion
 dotnet_style_object_initializer = true:suggestion
 dotnet_style_prefer_collection_expression = true:suggestion
 
+[SharpProof.BuildTasks/InvalidatePublishedResult.cs]
+dotnet_diagnostic.CA1515.severity = none
+
+[SharpProof.BuildTasks/ResetPublishedVerification.cs]
+dotnet_diagnostic.CA1515.severity = none
+
+[SharpProof.BuildTasks/RunVerifier.cs]
+dotnet_diagnostic.CA1515.severity = none
+
+[SharpProof.BuildTasks/ValidatePublishedVerificationResult.cs]
+dotnet_diagnostic.CA1515.severity = none
+
 [SharpProof.Dataflow/IntervalDomain.cs]
 dotnet_diagnostic.CA1822.severity = none
 

Directory.Build.props

@@ -36,6 +36,7 @@
       '$(MSBuildProjectName)' == 'SharpProof.Dataflow' Or
       '$(MSBuildProjectName)' == 'SharpProof.Effects' Or
       '$(MSBuildProjectName)' == 'SharpProof.Frontend' Or
+      '$(MSBuildProjectName)' == 'SharpProof.Fuzz' Or
       '$(MSBuildProjectName)' == 'SharpProof.Gates' Or
       '$(MSBuildProjectName)' == 'SharpProof.Host' Or
       '$(MSBuildProjectName)' == 'SharpProof.Ir' Or

README.md

@@ -145,7 +145,7 @@ both implemented feature groups:
   verification.
 
 `SharpProofFeatures` values are `effects`, `contracts`, and `all` (the
-default). The effective selection is sealed into the schema-14 compiler
+default). The effective selection is sealed into the schema-15 compiler
 artifact and filters its manifest: `contracts` excludes effect-only
 annotations, `effects` excludes postcondition claims and contract assumptions,
 and `all` selects both surfaces. Every effective effect contract has one typed
@@ -425,7 +425,7 @@ Each manifest claim receives:
 
 Effect claims use canonical compiler-produced evidence. They are `Proven` only
 when a complete effect summary establishes the selected contract. Compiler
-artifact schema 14 retains schema 10's independently replayable,
+artifact schema 15 retains schema 10's independently replayable,
 unconditional direct event for a definite managed object or array allocation.
 The worker validates the event's order, source-tree hash and span, semantic
 identity, selected constraint, and compiler witness, then derives the
@@ -524,7 +524,7 @@ unsupported opcodes, recursive dependencies, and exhausted budgets abstain as
 typed `Unknown`; they are never treated as implementation proof authority.
 Every composed call seals its origin, evidence digest, optional pack identity,
 and complete transitive dependency-evidence closure into compiler artifact
-schema 14. Relational-summary schema version 2 and specification-pack schema
+schema 15. Relational-summary schema version 2 and specification-pack schema
 version 1 govern those evidence records.
 
 Specification packs are off by default. The preview ships one data-driven
@@ -720,7 +720,7 @@ host shadowing and arbitrary relative overrides are rejected before any push.
 
 ## Closed compiler artifact and remaining release gaps
 
-The build-only collector now emits compiler artifact schema version 14 from the
+The build-only collector now emits compiler artifact schema version 15 from the
 final post-generator Roslyn `Compilation`. It seals the feature-selected claim
 manifest and, for each selected callable, either a typed lowering failure or
 portable whole-body CFG/IR with bound contract clauses, canonical variables,

SEMANTICS.md

@@ -60,7 +60,7 @@ manifest claims while sharing the effective combined constraint and evidence.
 Each effect claim is `Proven` only when a complete compiler-produced effect
 summary establishes its contract. The compiler can record a structured
 `DefiniteViolation` candidate for a simple unconditional direct operation.
-Compiler artifact schema 14 carries an independently replayable event only for
+Compiler artifact schema 15 carries an independently replayable event only for
 a definite managed object or array allocation whose operands are already
 known to complete and whose allocation is not static-initialization-sensitive.
 The worker derives `Allocates` from that event rather than trusting the
@@ -209,7 +209,7 @@ identity-mismatched pack never contributes a fact.
 
 Every summary call seals its origin, SHA-256 evidence, pack identity when
 applicable, and the canonical transitive provenance of every composed
-dependency. Compiler artifact schema 14, relational-summary schema version 2,
+dependency. Compiler artifact schema 15, relational-summary schema version 2,
 and specification-pack schema version 1 validate that closure before backend
 creation.
 Unsupported or incomplete calls remain `Unknown`; neither a convenient method
@@ -376,7 +376,7 @@ its outcome is not combined with the containing callable. Unavailable captured
 facts remain unknown. An expression-tree lambda is quoted code and is not
 treated as an executing call site.
 
-The packaged verifier consumes compiler artifact schema version 14 produced
+The packaged verifier consumes compiler artifact schema version 15 produced
 from the final post-generator compilation. The artifact contains the sealed
 feature-selected manifest and, for every selected callable, either a typed
 lowering failure or portable whole-body CFG/IR with bound clauses, canonical

SharpProof.Analyzer.Core/AnalyzerFeaturePipeline.cs

@@ -417,9 +417,7 @@ internal static void AnalyzeMemberInitializer(
     {
         context.CancellationToken.ThrowIfCancellationRequested();
         if (context.Node is not EqualsValueClauseSyntax initializer ||
-            initializer.Parent is not VariableDeclaratorSyntax and not PropertyDeclarationSyntax ||
-            AnalyzerGeneratedCodePolicy.IsGenerated(
-                initializer.SyntaxTree, context.Compilation, context.CancellationToken))
+            initializer.Parent is not VariableDeclaratorSyntax and not PropertyDeclarationSyntax)
         {
             return;
         }
@@ -431,31 +429,79 @@ initializer.Parent is not VariableDeclaratorSyntax and not PropertyDeclarationSy
                 property, context.CancellationToken),
             _ => null
         };
-        if (symbol is not IFieldSymbol and not IPropertySymbol ||
+        if (symbol is not IFieldSymbol and
+            not IPropertySymbol and
+            not IEventSymbol ||
             symbol.ContainingType is not { } type)
         {
             return;
         }
         var isStatic = symbol.IsStatic;
-        var constructor = (isStatic
+        var constructors = (isStatic
                 ? type.StaticConstructors
                 : type.InstanceConstructors)
             .OrderBy(static candidate => candidate.DeclaringSyntaxReferences
+                .FirstOrDefault()?.SyntaxTree.FilePath, StringComparer.Ordinal)
+            .ThenBy(static candidate => candidate.DeclaringSyntaxReferences
                 .FirstOrDefault()?.Span.Start ?? int.MaxValue)
-            .FirstOrDefault();
+            .Where(candidate =>
+                !AnalyzerGeneratedCodePolicy.IsGenerated(
+                    candidate,
+                    candidate.DeclaringSyntaxReferences.FirstOrDefault()?.SyntaxTree ??
+                        initializer.SyntaxTree,
+                    context.Compilation,
+                    context.CancellationToken))
+            .ToArray();
         var root = context.SemanticModel.GetOperation(
             initializer.Value, context.CancellationToken);
-        if (constructor == null || root == null)
+        if (constructors.Length == 0 || root == null ||
+            AnalyzerGeneratedCodePolicy.IsGenerated(
+                symbol,
+                initializer.SyntaxTree,
+                context.Compilation,
+                context.CancellationToken))
         {
             return;
         }
-        var outcome = AnalyzerSemanticOutcome.NotApplicable;
-        foreach (var operation in root.DescendantsAndSelf())
+        IMethodSymbol? constructor = null;
+        foreach (var candidate in constructors)
         {
-            if (operation is not IInvocationOperation and not IObjectCreationOperation)
+            if (SharpProofControlAttributePolicy.ValidateAndShouldSuppress(
+                    candidate,
+                    session,
+                    context.ReportDiagnostic,
+                    context.CancellationToken))
             {
+                session.RecordSemanticOutcome(
+                    candidate,
+                    AnalyzerSemanticOutcome.Suppressed);
                 continue;
             }
+            constructor = candidate;
+            break;
+        }
+        if (constructor == null)
+        {
+            return;
+        }
+        var outcome = AnalyzerSemanticOutcome.NotApplicable;
+        var operationFacts = new DefiniteOperationFacts(
+            context.Compilation,
+            context.CancellationToken);
+        if (!CanReachMemberInitializer(
+                initializer,
+                isStatic,
+                context.SemanticModel,
+                operationFacts,
+                context.CancellationToken))
+        {
+            return;
+        }
+        foreach (var operation in RequiresCallSiteDiscovery
+                     .ExecutableUnflowedDescendantsAndSelf(
+                         root,
+                         operationFacts))
+        {
             outcome = AnalyzerSemanticOutcomes.Combine(
                 outcome,
                 RequiresCallSiteAnalyzer.AnalyzeInitializerCall(
@@ -466,6 +512,89 @@ initializer.Parent is not VariableDeclaratorSyntax and not PropertyDeclarationSy
         session.RecordSemanticOutcome(constructor, outcome);
     }
 
+    private static bool CanReachMemberInitializer(
+        EqualsValueClauseSyntax target,
+        bool isStatic,
+        SemanticModel semanticModel,
+        DefiniteOperationFacts operationFacts,
+        CancellationToken cancellationToken)
+    {
+        var containingType = target.FirstAncestorOrSelf<TypeDeclarationSyntax>();
+        var targetMember = target.FirstAncestorOrSelf<MemberDeclarationSyntax>();
+        if (containingType == null || targetMember == null)
+        {
+            return true;
+        }
+
+        foreach (var member in containingType.Members)
+        {
+            foreach (var initializer in GetMemberInitializers(member))
+            {
+                if (initializer.SyntaxTree == target.SyntaxTree &&
+                    initializer.Span == target.Span)
+                {
+                    return true;
+                }
+                if (!HasMatchingInitializationKind(
+                        initializer,
+                        isStatic,
+                        semanticModel,
+                        cancellationToken))
+                {
+                    continue;
+                }
+                var operation = semanticModel.GetOperation(
+                    initializer.Value,
+                    cancellationToken);
+                if (operation != null &&
+                    !operationFacts.MayCompleteNormally(operation))
+                {
+                    return false;
+                }
+            }
+            if (member.SyntaxTree == targetMember.SyntaxTree &&
+                member.Span == targetMember.Span)
+            {
+                return true;
+            }
+        }
+        return true;
+    }
+
+    private static IEnumerable<EqualsValueClauseSyntax> GetMemberInitializers(
+        MemberDeclarationSyntax member)
+    {
+        return member switch
+        {
+            BaseFieldDeclarationSyntax field => field.Declaration.Variables
+                .Select(static variable => variable.Initializer)
+                .OfType<EqualsValueClauseSyntax>(),
+            PropertyDeclarationSyntax { Initializer: { } initializer } =>
+                [initializer],
+            _ => []
+        };
+    }
+
+    private static bool HasMatchingInitializationKind(
+        EqualsValueClauseSyntax initializer,
+        bool isStatic,
+        SemanticModel semanticModel,
+        CancellationToken cancellationToken)
+    {
+        var symbol = initializer.Parent switch
+        {
+            VariableDeclaratorSyntax variable => semanticModel.GetDeclaredSymbol(
+                variable,
+                cancellationToken),
+            PropertyDeclarationSyntax property => semanticModel.GetDeclaredSymbol(
+                property,
+                cancellationToken),
+            _ => null
+        };
+        return symbol is IFieldSymbol or IPropertySymbol or IEventSymbol &&
+            symbol.IsStatic == isStatic;
+    }
+
     private static bool ValidateContractClauses(
         IMethodSymbol method,
         AnalyzerSession session,

SharpProof.Analyzer.Core/AnalyzerGeneratedCodePolicy.cs

@@ -18,6 +18,19 @@ internal static bool IsGenerated(
         SyntaxTree tree,
         Compilation compilation,
         CancellationToken cancellationToken)
+    {
+        return IsGenerated(
+            (ISymbol)method,
+            tree,
+            compilation,
+            cancellationToken);
+    }
+
+    internal static bool IsGenerated(
+        ISymbol symbol,
+        SyntaxTree tree,
+        Compilation compilation,
+        CancellationToken cancellationToken)
     {
         if (IsGenerated(tree, compilation, cancellationToken))
         {
@@ -27,7 +40,7 @@ internal static bool IsGenerated(
         var generated = compilation.Options.SyntaxTreeOptionsProvider?
             .IsGenerated(tree, cancellationToken) ?? GeneratedKind.Unknown;
         return generated != GeneratedKind.NotGenerated &&
-            HasGeneratedCodeAttribute(method, compilation);
+            HasGeneratedCodeAttribute(symbol, compilation);
     }
 
     internal static bool IsGenerated(
@@ -94,7 +107,7 @@ private static bool IsExactGeneratedHeader(string comment)
     }
 
     private static bool HasGeneratedCodeAttribute(
-        IMethodSymbol method,
+        ISymbol symbol,
         Compilation compilation)
     {
         var generatedCode = compilation.GetTypeByMetadataName(
@@ -104,21 +117,21 @@ private static bool HasGeneratedCodeAttribute(
             return false;
         }
 
-        var scopes = new List<ISymbol> { method };
-        if (method.AssociatedSymbol != null)
+        var scopes = new List<ISymbol> { symbol };
+        if (symbol is IMethodSymbol { AssociatedSymbol: { } associated })
         {
-            scopes.Add(method.AssociatedSymbol);
+            scopes.Add(associated);
         }
-        for (var type = method.ContainingType;
+        for (var type = symbol.ContainingType;
              type != null;
              type = type.ContainingType)
         {
             scopes.Add(type);
         }
 
-        foreach (var symbol in scopes)
+        foreach (var scope in scopes)
         {
-            if (symbol.GetAttributes().Any(attribute =>
+            if (scope.GetAttributes().Any(attribute =>
                     SymbolEqualityComparer.Default.Equals(
                         attribute.AttributeClass?.OriginalDefinition,
                         generatedCode.OriginalDefinition)))