Skip to content

AGENT.soundiness.md

Latest commit

 

History

History
321 lines (236 loc) · 11 KB

AGENT.soundiness.md

File metadata and controls

321 lines (236 loc) · 11 KB
Raw

Soundiness Info Window - Design Document

Overview

This document describes the design and implementation for a Soundiness Info Window in KeY, as implemented on July 3, 2026.

What is Soundiness?

Soundiness refers to the practical trade-offs made in formal verification tools between complete soundness and usability. Unlike binary soundness (sound/unsound), soundiness acknowledges a spectrum of assumptions and simplifications that affect verification validity.

See: Soundiness - Communications of the ACM

In KeY's context, soundiness encompasses:

  • Taclet options that disable certain checks for usability
  • Platform limitations (memory, timeouts)
  • Incomplete source code analysis
  • Proof techniques that rely on unproved lemmas or assumptions

User Requirements

Goal

Provide non-expert KeY users with a comprehensive, understandable report explaining what assumptions and limitations affect their verification results.

Key Design Decisions

Question Decision Rationale
Q1: Aggregate risk score? ❌ No aggregate level Users should see individual warnings without oversimplification
Q2: Detail level? ✅ Full detail in HTML format Simple, readable format that works in Swing
Q3: Proof tree analysis depth? ✅ Full traversal Users need to find where assumptions are used
Q4: Batch analysis? ❌ Not for v1 Focus on single-proof experience first
Q5: Report persistence? ❌ Compute fresh each time Settings may change; always show current state
Q6: Memory warning thresholds? ✅ Yes (<1GB critical, <2GB warning) Concrete thresholds help users understand limits

Four Compartments

The soundiness report is organized into four distinct compartments:

Compartment 1: General KeY Settings

"Platform and tool limitations that affect verification"

Data Sources:

  • Runtime.getRuntime().maxMemory() - JVM memory limits
  • ChoiceSettings.getChoice("initialisation") - Static initialization setting
  • StrategySettings.getMaxSteps() - Proof search limits
  • GeneralSettings.isUseJML() - JML enabled/disabled
  • GeneralSettings.isEnsureSourceConsistency() - Source caching

Warning Examples:

Category Condition User Message
Memory < 1GB available "Very limited memory available"
Memory < 2GB available "Limited memory available"
Static Initialization disableStaticInitialisation "Static constructors are not analyzed"
JML Disabled isUseJML() == false "JML specifications are ignored"
Source Caching isEnsureSourceConsistency() == false "Source file changes may not be detected"

Compartment 2: Taclet Options

"Semantic simplifications in the logical calculus"

Current KeY Classification:

// UNSOUND choices (TacletOptionsSettings.isUnsound())
- runtimeExceptions:ignore
- initialisation:disableStaticInitialisation  
- intRules:arithmeticSemanticsIgnoringOF

// INCOMPLETE choices (isIncomplete())
- runtimeExceptions:ban
- Strings:off
- intRules:arithmeticSemanticsCheckingOF
- integerSimplificationRules:minimal
- programRules:None

// CONDITIONAL (getInformation())
- JavaCard:on/off (sound only for respective platform)
- assertions:on/off (depends on JVM startup flags)

Enhanced Presentation:

Choice Plain English Impact Severity
runtimeExceptions:ignore "Assumes no null pointer, divide-by-zero, or array bounds errors occur" 🔴 High
intRules:arithmeticSemanticsIgnoringOF "Integer overflow is ignored; arithmetic wraps around like in Java" 🔴 High
initialisation:disableStaticInitialisation "Static field initializers and static blocks are skipped" 🔴 High
Strings:off "String operations are not analyzed" 🟡 Medium
programRules:None "Java language constructs are not processed" 🔴 High
runtimeExceptions:ban "Any implicit runtime exception is treated as program failure" 🟢 Low

Compartment 3: Source Analysis

"What was actually loaded and parsed"

Information Displayed:

  • Count of loaded .java and .key files
  • Parse warnings and errors
  • Missing class dependencies
  • JML contract coverage (% of methods with specifications)
  • Unsupported Java features (lambdas, streams, etc.)

Note: Currently returns empty data; full implementation requires integration with KeYFile/InitConfig.

Compartment 4: Proof Tree Analysis

"What happened during this specific proof"

Analysis Components:

  1. Goal Statistics

    • Total goals, closed goals, open goals
    • Cached goals (from proof cache)

  2. User-Defined Lemmas

    • Scan for taclets with "lemma" in name
    • Track usage count
    • Flag unproved lemmas

  3. Assumptions

    • Count of assume commands used
    • Location and formula for each assumption

  4. Rule Application Statistics

    • Most frequently used rules (top 5)
    • Interactive vs. automated steps ratio

Technical Architecture

Implementation Approach

The implementation uses a single HTML generation approach rather than separate data models and UI components:

Location: /opencode/key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessAnalyzer.java

public final class SoundinessAnalyzer {
    
    /**
     * Generates an HTML soundiness report for the given proof.
     * 
     * @param proof the proof to analyze
     * @return HTML string containing the complete report
     */
    public static String generateHTMLReport(Proof proof);
}

Internal Data Records (encapsulated within analyzer):

  • GeneralKeYWarning - Warning with level, category, message, recommendation
  • TacletOptionEntry - Taclet choice with impact description
  • SourceStats - Source file statistics
  • ProofStats - Proof tree statistics
  • LemmaUsage - Lemma usage tracking
  • AssumptionUsage - Assumption tracking

Dialog UI

Location: /opencode/key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessDialog.java

Simple modal JDialog with:

  • HTML pane displaying the generated report
  • Scroll pane with wheel scrolling enabled
  • Copy HTML button
  • Close button

UI Layout:

┌─────────────────────────────────────────────────────┐
│  Soundiness Report: [Proof Name]                    │
├─────────────────────────────────────────────────────┤
│                                                     │
│  [Scrollable HTML Report]                           │
│  - 1. General KeY Settings                          │
│  - 2. Taclet Options                                │
│  - 3. Source Analysis                               │
│  - 4. Proof Tree Analysis                           │
│                                                     │
│        [Copy HTML]  [Close]                         │
└─────────────────────────────────────────────────────┘

Integration Points

1. TaskTree Icon Enhancement

File: TaskTree.java:TaskTreeIconCellRenderer.getTreeCellRendererComponent()

Add overlay icon when proof has unsound choices or assumptions:

  • Icon: Use existing IconFactory.WARNING_UNSOUND
  • Tooltip: Brief summary like "2 unsound choices, 1 assumption used"

2. Proof Statistics Dialog

File: ShowProofStatistics.java:Window.init()

Add button after line ~338:

JButton soundinessButton = new JButton("Show Soundiness Report");
soundinessButton.setIcon(IconFactory.WARNING_UNSOUND.get());
soundinessButton.addActionListener(e -> {
    de.uka.ilkd.key.gui.soundiness.SoundinessDialog dialog = 
        new de.uka.ilkd.key.gui.soundiness.SoundinessDialog(mainWindow, proof);
    dialog.setVisible(true);
});
buttonPane2.add(soundinessButton);

3. Context Menu Extension

File: ShowSoundinessAction.java

Register via KeY extension mechanism to add "Show Soundiness Report" to proof list right-click menu.

4. Proof Finished Notification

File: ProofClosedJTextPaneDisplay.java:execute()

After showing statistics, optionally add link: "⚠ This proof used unsound options. [View Details]"

Code Conventions

Naming

  • Use Soundiness prefix consistently (not Soundness)
  • Private constructors for utility classes
  • Internal records use descriptive names

Documentation

  • Javadoc for public APIs
  • Include @since 2.13 tag
  • Link to this document in package-info.java

Error Handling

  • Never fail silently - log warnings to SLF4J
  • Handle null proofs gracefully
  • Catch exceptions during analysis and show partial results

Testing Strategy

Manual Testing Scenarios

  1. Proof with all 3 unsound choices enabled
  2. Proof using \lemma taclets without side proofs
  3. Proof with multiple assume commands
  4. Minimal proof (single goal, few steps)
  5. Proof closed via cache
  6. Large proof (>1000 nodes) - verify performance acceptable (<2s analysis)

Performance Considerations

Current Implementation

  • Single-pass analysis for all compartments
  • HTML generated on-demand
  • No caching (report computed fresh each time)

Future Optimization

For very large proofs, consider:

  • Background thread analysis
  • Lazy loading of compartments
  • Caching with invalidation on proof structure changes

Risks and Mitigations

Risk Impact Mitigation
Proof tree traversal too slow Poor UX for large proofs Profile and optimize if needed
Too many false positives Users ignore warnings Careful calibration, user feedback loop
Technical jargon in messages Confuses non-experts Iterate on wording based on feedback
Integration conflicts with extensions Broken functionality Test with popular extensions

Future Enhancements (Post-v1)

  • Batch analysis ("Analyze All Loaded Proofs")
  • Persistent soundiness metadata in proof bundles
  • Aggregate statistics across proof corpus
  • Automatic recommendations ("Consider enabling X for more complete verification")
  • Integration with SMT solver trust levels
  • Historical tracking (how soundiness changed during proof development)
  • Enhanced source analysis with real KeYFile data
  • Proper lemma detection via \lemma annotation parsing

References

  • Soundiness - CACM Paper
  • TacletOptionsSettings.java - existing taclet option handling
  • ShowProofStatistics.java - similar dialog pattern
  • TaskTree.java - proof list rendering

Contact

For questions about this implementation, contact the KeY development team.

Document Version: 2.0
Created: 2026-07-03
Updated: 2026-07-03 (Simplified HTML generation approach)
Status: ✅ Implemented