Add scan_bug_history.py top-20 GitHub repo scanning and fix_from_bug_history.py Copilot calibration

- scan_bug_history.py: auto-fetch top N Python repos from GitHub Search API,
  shallow-clone each, scan 1000 commits per repo, produce combined JSON+MD report
- fix_from_bug_history.py: parse bug_history.md, verify each BUG_INTRODUCED/
  BUG_FIXED event via GitHub Models API (gh auth token), compute per-bug-type
  precision, generate and optionally apply patches to a3_python/unsafe/ checkers
- results/a3_calibration.md: initial calibration run (41% overall precision;
  NAME_ERROR 100%, TYPE_CONFUSION 40%, BOUNDS/DIV_ZERO 0%)

Author: GitHub Copilot

.github/workflows/agential-ci.yml

@@ -0,0 +1,48 @@
+name: Agential Demo CI
+
+on:
+  push:
+    branches: [ main, master ]
+  pull_request:
+    branches: [ main, master ]
+
+jobs:
+  demo:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Setup Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.11'
+      - name: Run demo
+        run: |
+          python3 agential_demo/demo.py 2>&1 | tee demo.log
+      - name: Upload demo log
+        uses: actions/upload-artifact@v4
+        with:
+          name: demo-log
+          path: demo.log
+
+  build_slides:
+    needs: demo
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install Rust toolchain (for tectonic)
+        uses: actions-rs/toolchain@v1
+        with:
+          toolchain: stable
+          profile: minimal
+          override: true
+      - name: Install tectonic
+        run: cargo install tectonic --locked
+      - name: Build slides PDF
+        run: |
+          cd agential_demo
+          tectonic slides.tex
+      - name: Upload slides PDF
+        uses: actions/upload-artifact@v4
+        with:
+          name: slides-pdf
+          path: agential_demo/slides.pdf

BugsInPy

@@ -0,0 +1 @@
+Subproject commit 11c5f1eea954a42132cfd06bf257766a7963e0fd

README.md

@@ -52,6 +52,16 @@ a3 scan . --triage github                # uses GITHUB_TOKEN, free in CI
 a3 scan . --triage anthropic              # uses ANTHROPIC_API_KEY
 ```
 
+#### Using GitHub Models locally (free, no API key needed)
+
+If you have the [GitHub CLI](https://cli.github.com/) installed and authenticated (`gh auth login`), you can use GitHub Models for triage locally — no API key signup required:
+
+```bash
+export GITHUB_TOKEN=$(gh auth token) && a3 scan . --triage github --verbose
+```
+
+This exports your existing GitHub CLI token and uses it to access GitHub Models for agentic triage. In CI (GitHub Actions), `GITHUB_TOKEN` is already available automatically.
+
 Or run scan and triage as separate steps:
 
 ```bash
@@ -199,6 +209,70 @@ a3 baseline diff --sarif results.sarif
 a3 baseline accept --sarif results.sarif
 ```
 
+### Two Usage Patterns
+
+#### Scenario A: Whole-Repo Scan
+
+Scan every Python file in one pass. Best for first-time adoption, weekly audits, or establishing a baseline.
+
+```bash
+# Scan the entire repository
+a3 scan . --interprocedural --dse-verify --output-sarif results.sarif
+
+# Agentic triage (optional — filters remaining false positives)
+a3 triage --sarif results.sarif --provider github --agentic \
+  --output-sarif triaged.sarif
+
+# Lock current findings as the baseline (ratchet start)
+a3 baseline accept --sarif triaged.sarif
+git add .a3-baseline.json && git commit -m "ci: establish a3 baseline" && git push
+```
+
+The scheduled workflow (`a3-scheduled-scan.yml`) repeats this automatically every week.
+
+#### Scenario B: Incremental — Auto-Invoke on Every Python File Change
+
+After `a3 init . --copilot`, **no manual step is needed**. The generated `a3-pr-scan.yml` triggers whenever a `.py` file is added or modified:
+
+```yaml
+on:
+  push:
+    branches: [main]
+    paths: ["**.py"]          # triggers ONLY when .py files change
+  pull_request:
+    branches: [main]
+    paths: ["**.py"]
+```
+
+**Example — adding a new file:**
+
+```bash
+cat > src/payments.py << 'EOF'
+def charge(amount, discount):
+    return amount / discount   # DIV_ZERO: discount could be 0
+
+def refund(amount, count):
+    if count > 0:
+        return amount / count  # SAFE: guarded by count > 0
+    return 0.0
+EOF
+
+git add src/payments.py
+git commit -m "feat: add payment processing"
+git push   # <-- CI auto-triggers, scans only src/payments.py
+```
+
+What happens automatically:
+
+1. Push triggers `a3-pr-scan.yml` (path filter matches `**.py`)
+2. Workflow detects changed files via `git diff --name-only`
+3. a3 scans only `src/payments.py` — finds DIV_ZERO in `charge()`, proves `refund()` safe
+4. Baseline diff: new bug not in baseline → **CI fails** until the bug is fixed or accepted
+
+Non-Python changes (docs, configs, images) do not trigger the workflow at all.
+
+---
+
 ### Using a different LLM provider (optional)
 
 If you prefer Claude or GPT-5 via your own API key instead of GitHub Models:
@@ -291,7 +365,7 @@ a3 <target> [options]           # legacy syntax, same behavior
 | `--output-sarif PATH` | Write SARIF 2.1.0 JSON |
 | `--triage [PROVIDER]` | Run agentic triage after scan (auto-detects API key, or specify: `openai`, `anthropic`, `github`) |
 | `--triage-model MODEL` | LLM model for integrated triage (default: provider-appropriate) |
-| `--save-results PATH` | Write results as pickle (default: `results/<name>_results.pkl`) |
+| `--save-results PATH` | Write results as JSON (default: `results/<name>_results.json`) |
 | `--verbose` | Detailed step-by-step output |
 | `--config PATH` | Path to `.a3.yml` |
 
@@ -578,16 +652,6 @@ a3 baseline diff --sarif triaged.sarif --auto-issue
 
 ---
 
-## Docker
-
-```bash
-docker build -t a3 .
-docker run --rm -v $(pwd)/my_project:/target a3 /target
-docker run --rm -v $(pwd):/code a3 /code/myfile.py --functions
-```
-
----
-
 ## Architecture
 
 ```

a3_python/__init__.py

@@ -11,4 +11,9 @@
 No heuristics. Grounded in Python→Z3 heap/transition/barrier model.
 """
 
-__version__ = "0.1.10"
+from importlib.metadata import version as _pkg_version, PackageNotFoundError
+
+try:
+    __version__: str = _pkg_version("a3-python")
+except PackageNotFoundError:
+    __version__ = "0.0.0+dev"

a3_python/__main__.py

@@ -1,11 +1,11 @@
 """
-Allow running pyfromscratch as a module:
+Allow running a3_python as a module:
 
-    python3.11 -m pyfromscratch <target> [options]
+    python3 -m a3_python <target> [options]
 
-Delegates to pyfromscratch.cli:main().
+Delegates to a3_python.cli:main().
 """
 import sys
-from .cli import main
+from .cli import _main_wrapper
 
-sys.exit(main())
+sys.exit(_main_wrapper())

a3_python/barriers/context_aware_verification.py

@@ -160,15 +160,24 @@ def verify_bug_with_full_context(
         # =====================================================================
         # LAYER 2: Synthesize barriers from preconditions
         # =====================================================================
+        # CRITICAL FIX: Only mark safe if there is EVIDENCE that the barrier
+        # condition holds (e.g., validated params, guard facts for this bug type).
+        # Simply creating a barrier template is not proof — we need evidence
+        # that the precondition (x != 0, len(x) > 0, x is not None) is enforced.
         if bug_variable:
-            synthesized = self._synthesize_barrier_for_bug(
-                bug_type, bug_variable, crash_summary
+            # Check if there's evidence the precondition is satisfied
+            has_evidence = self._has_precondition_evidence(
+                bug_type, bug_variable, crash_summary, call_chain_summaries
             )
-            if synthesized:
-                result.synthesized_barriers.append(synthesized)
-                result.is_safe = True
-                result.verification_time_ms = (time.time() - start_time) * 1000
-                return result
+            if has_evidence:
+                synthesized = self._synthesize_barrier_for_bug(
+                    bug_type, bug_variable, crash_summary
+                )
+                if synthesized:
+                    result.synthesized_barriers.append(synthesized)
+                    result.is_safe = True
+                    result.verification_time_ms = (time.time() - start_time) * 1000
+                    return result
 
         # =====================================================================
         # LAYER 3: Learn invariants from codebase
@@ -187,7 +196,8 @@ def verify_bug_with_full_context(
         # LAYER 4: Interprocedural barrier propagation
         # =====================================================================
         interprocedural = self._propagate_barriers_interprocedurally(
-            bug_type, bug_variable, call_chain_summaries
+            bug_type, bug_variable, call_chain_summaries,
+            crash_summary=crash_summary
         )
         if interprocedural:
             result.synthesized_barriers.extend(interprocedural)
@@ -432,6 +442,66 @@ def _check_learned_protection(
         # For now, conservative: return False
         return False
 
+    # =========================================================================
+    # LAYER 2 SUPPORT: Precondition Evidence Check
+    # =========================================================================
+    
+    def _has_precondition_evidence(
+        self,
+        bug_type: str,
+        bug_variable: Optional[str],
+        crash_summary: CrashSummary,
+        call_chain_summaries: List[CrashSummary],
+    ) -> bool:
+        """
+        Check if there is concrete evidence that the barrier precondition holds.
+        
+        A synthesized barrier is only trustworthy if there is evidence the code
+        actually enforces the precondition. Without evidence, synthesizing a 
+        barrier template is meaningless — the code may not protect against the bug.
+        
+        Evidence sources:
+        - Guard facts that match the bug type (e.g., non-zero check for DIV_ZERO)
+        - Validated params (caller checks value before passing)
+        - Return guarantees from callees
+        
+        Returns:
+            True if there is concrete evidence the precondition is enforced
+        """
+        from .guard_to_barrier import get_protected_bugs
+        from ..semantics.interprocedural_guards import BUG_TYPE_TO_GUARD_TYPES
+        
+        # 1. Check if crash summary has guard facts for this bug type
+        relevant_guard_types = BUG_TYPE_TO_GUARD_TYPES.get(bug_type, set())
+        
+        for block_id, guard_facts in crash_summary.intra_guard_facts.items():
+            for guard_type, variable, extra in guard_facts:
+                if guard_type in relevant_guard_types:
+                    # Found a guard for the right bug type
+                    # Check if it protects the right variable
+                    if bug_variable is None or variable is None:
+                        return True
+                    if bug_variable in str(variable) or str(variable) in bug_variable:
+                        return True
+        
+        # 2. Check if the bug type is in guarded_bugs
+        if bug_type in crash_summary.guarded_bugs:
+            return True
+        
+        # 3. Check validated params from call chain
+        for summary in call_chain_summaries:
+            for param_idx, validations in summary.validated_params.items():
+                if validations and bug_variable and f'param_{param_idx}' == bug_variable:
+                    return True
+        
+        # 4. Check return guarantees from callees
+        for summary in call_chain_summaries:
+            if bug_type in summary.guarded_bugs:
+                return True
+        
+        # No evidence found — the barrier can't be trusted
+        return False
+    
     # =========================================================================
     # LAYER 4: Interprocedural Propagation
     # =========================================================================
@@ -440,18 +510,27 @@ def _propagate_barriers_interprocedurally(
         self,
         bug_type: str,
         bug_variable: Optional[str],
-        call_chain_summaries: List[CrashSummary]
+        call_chain_summaries: List[CrashSummary],
+        crash_summary: Optional[CrashSummary] = None
     ) -> List[BarrierCertificate]:
         """
         Propagate barriers from callers to callees.
         
         If caller validates parameter x, and callee uses x in a crash,
         the validation barrier protects the callee.
+        
+        NOTE: A function's own return guarantees do NOT protect against its
+        own internal bugs. E.g., if f() has return_guarantees={'nonnull'},
+        that means f's *return value* is non-None, not that f is internally
+        safe from NULL_PTR. Skip the crash function's own summary.
         """
         propagated = []
 
-        # Check return guarantees from callees
+        # Check return guarantees from callees (excluding crash function itself)
         for summary in call_chain_summaries:
+            # A function's own return guarantee does not protect its internal ops
+            if crash_summary is not None and summary is crash_summary:
+                continue
             for guarantee_type in summary.return_guarantees:
                 # Create barrier from guarantee
                 if guarantee_type == 'nonempty' and bug_type == 'BOUNDS':

a3_python/barriers/dsos_sdsos.py

@@ -1198,7 +1198,7 @@ class DSOSIntegrationConfig:
 
 class DSOSSDSOSIntegration:
     """
-    Main integration class for DSOS/SDSOS in PythonFromScratch.
+    Main integration class for DSOS/SDSOS in a3-python.
     
     Provides:
     1. Problem analysis and method selection

a3_python/barriers/hscc2004.py

@@ -5,7 +5,7 @@
   S. Prajna, A. Jadbabaie, G. J. Pappas.
   "Safety verification of hybrid systems using barrier certificates." HSCC 2004.
 
-In PythonFromScratch, we use the same *barrier proof obligations* (Init/Unsafe/Step)
+In a3-python, we use the same *barrier proof obligations* (Init/Unsafe/Step)
 but apply them to discrete transition systems extracted from Python bytecode.
 
 This module provides a first practical, sound "hybrid-style" integration:

a3_python/barriers/lasserre_hierarchy.py

@@ -1110,7 +1110,7 @@ def get_cached_counterexamples(self) -> List[List[float]]:
 
 class LasserreIntegration:
     """
-    Main integration class for Lasserre hierarchy in PythonFromScratch.
+    Main integration class for Lasserre hierarchy in a3-python.
     
     Provides the interface for the kitchen-sink orchestrator to use
     Lasserre-based barrier synthesis with systematic degree lifting.

a3_python/barriers/parrilo_sos_sdp.py

@@ -1181,7 +1181,7 @@ class SOSBarrierSynthesizer:
     """
     Synthesizes barrier certificates using SOS-SDP.
     
-    This is the main integration point with the PythonFromScratch framework.
+    This is the main integration point with the a3-python framework.
     It extracts polynomial models from program semantics and finds certificates
     using Positivstellensatz-based reasoning.
     """
@@ -1596,7 +1596,7 @@ def operand_to_poly(operand) -> Optional[Polynomial]:
 
 class ParriloSOSIntegration:
     """
-    Main integration class for Parrilo SOS-SDP in PythonFromScratch.
+    Main integration class for Parrilo SOS-SDP in a3-python.
     
     This class provides the interface for the kitchen-sink orchestrator
     to invoke SOS-based barrier synthesis and certification.