proofs(lean4) + tests: A-12 path-traversal containment (closes frontier A-12) by hyperpolymath · Pull Request #132 · hyperpolymath/valence-shell

hyperpolymath · 2026-06-02T22:37:45Z

Summary

Closes frontier item A-12 from `docs/PROOF-OPEN-FRONTIER.adoc`: prove that `ShellState::resolve_path` always returns a `PathBuf` within the sandbox root, regardless of `..` / `.` / normal components in the input.

Regression-guard for the 2026-02-12 CVE-class audit fix (`resolve_path("../../etc/passwd")` previously escaped the sandbox).

Changes

Lean 4 — `proofs/lean4/PathTraversal.lean`

Models the Rust resolve_path loop as `Component → applyComponent`.
Proves `applyComponent_preserves_root_prefix` per component (with sub-lemmas `isPrefix_append_right` and `isPrefix_dropLast`).
Lifts to `normalizeRaw_within_root` via the foldl invariant.
Headline: `path_traversal_containment` — `root <+: normalizePath root raw` for all `root`, `raw`.
Corollary: `normalizePath_eq_normalizeRaw` (the final clamp never fires — the foldl invariant alone suffices).
Wired into `lakefile.lean` as `lean_lib PathTraversal`.
Verified locally: `lean PathTraversal.lean` exit 0.

Rust — `impl/rust-cli/tests/security_tests.rs`

`property_resolve_path_stays_within_sandbox` — proptest with mixed `..` / `.` / normal components, optional leading slash (256 random cases per the proptest default).
`property_resolve_path_parent_dir_heavy_stays_within_sandbox` — 10:1 weighted toward `..` to specifically target the audit failure mode.
Both new tests + all 15 existing security tests pass (17 total).

Test plan

`lean PathTraversal.lean` — exit 0
`cargo test --test security_tests` — 17 passed, 0 failed
CI `lean-verification.yml` green
CI `rust-cli.yml` security_tests job green

References

Independent of PR proofs(coq): close admit triumvirate (#56 / #57 / #58) — Coq layer at zero Admitted #128 (the Coq admit triumvirate) — these can land in either order.
Frontier doc: `docs/PROOF-OPEN-FRONTIER.adoc` §A-12
Origin bug: 2026-02-12 Opus audit session (path_traversal in `What Was Fixed` § `CLAUDE.md`)

🤖 Generated with Claude Code

Closes frontier item A-12 from docs/PROOF-OPEN-FRONTIER.adoc: prove that ShellState::resolve_path always returns a PathBuf within the sandbox root, regardless of `..` / `.` / normal components in the input. Regression-guard for the 2026-02-12 CVE-class audit fix (resolve_path("../../etc/passwd") previously escaped the sandbox). Lean 4 — proofs/lean4/PathTraversal.lean * Models the Rust resolve_path loop as Component → applyComponent. * Proves applyComponent_preserves_root_prefix per component. * Lifts to normalizeRaw_within_root via foldl invariant. * Headline: path_traversal_containment. * Corollary: normalizePath_eq_normalizeRaw (final clamp never fires). * Wired into lakefile.lean as lean_lib PathTraversal. * Verified: lean PathTraversal.lean exit 0. Rust — impl/rust-cli/tests/security_tests.rs * property_resolve_path_stays_within_sandbox — proptest with mixed ../ + ./ + normal components, optional leading /. * property_resolve_path_parent_dir_heavy_stays_within_sandbox — 10:1 weighted toward `..` to specifically target the audit failure mode. Each runs 256 random cases (proptest default). * All 17 security tests pass (existing 15 + 2 new). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-02T22:38:44Z

🔍 Hypatia Security Scan

Findings: 149 issues detected

Severity	Count
🔴 Critical	8
🟠 High	34
🟡 Medium	107

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-04T00:43:59Z

🔍 Hypatia Security Scan

Findings: 149 issues detected

Severity	Count
🔴 Critical	8
🟠 High	34
🟡 Medium	107

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-04T02:51:29Z

🔍 Hypatia Security Scan

Findings: 148 issues detected

Severity	Count
🔴 Critical	8
🟠 High	34
🟡 Medium	106

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-04T02:53:15Z

🔍 Hypatia Security Scan

Findings: 148 issues detected

Severity	Count
🔴 Critical	8
🟠 High	34
🟡 Medium	106

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-04T03:00:28Z

🔍 Hypatia Security Scan

Findings: 148 issues detected

Severity	Count
🔴 Critical	8
🟠 High	34
🟡 Medium	106

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-05T02:44:35Z

🔍 Hypatia Security Scan

Findings: 151 issues detected

Severity	Count
🔴 Critical	8
🟠 High	38
🟡 Medium	105

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in bridge-forbidden-phrases.yml",
    "type": "missing_timeout_minutes",
    "file": "bridge-forbidden-phrases.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

## Summary Pilot for **Q1 closure-path-C** (\`believe_me\` axioms with CI allow-list). Lands the smallest possible footprint to demonstrate the unlock and gates further use behind a registry + CI check. **Closes 1 of 16 Idris2 holes** (\`equivReflProof\`) and provides the infrastructure to close more in follow-ups, subject to owner sign-off on Q4 policy. ## What's in this PR ### New module — \`proofs/idris2/src/Filesystem/Axioms.idr\` | Identifier | Type | Justification | |---|---|---| | \`axStringEqRefl\` | \`(s : String) -> (s == s) = True\` | Every Idris2 backend evaluates \`prim__strEq s s\` to True for any \`s\`; type-checker cannot see through the primitive on opaque values. Same epistemic status as Agda \`postulate funext\` or Coq \`Axiom is_empty_dir_dec\` (both already accepted). | | \`axBits8EqRefl\` | \`(b : Bits8) -> (b == b) = True\` | Same shape for the byte-level primitive. | | \`fileContentEqRefl\` | \`(xs : List Bits8) -> (xs == xs) = True\` | Derived (not an axiom) — structural induction over the list using \`axBits8EqRefl\` at the leaf. | ### \`Model.idr\` — \`equivRefl\` closed * \`pathEqRefl\` (structural induction over \`Path\`) * \`fsEntryEqRefl\` (case-split on \`Dir\` / \`File c\`) * \`entryEqRefl\` (tuple combinator) * \`equivRefl\` derives via \`allElemSelf\` (every entry is \`elem\` of its own list). Subtle bit: Idris2 0.8.0's \`elem\` is \`Foldable.any (==)\` which desugars to a foldl form, not the textbook \`(x==y) || elem x ys\` recursion. The proof threads through \`foldlOrTrueIdempotent\` — once the accumulator hits True, the foldl stays True regardless of the tail. Hole inventory: **16 → 15**. ### CI guard — \`.github/scripts/check-idris2-believe-me.sh\` * Rejects any \`believe_me\` in \`proofs/idris2/**/*.idr\` that is NOT in \`Filesystem.Axioms\`. * Sanity-check: registered-axiom count matches \`believe_me\` count in the allowed file. * Wired into \`idris-verification.yml\` as a pre-build gate. ### Registry — \`.machine_readable/IDRIS2_AXIOMS.a2ml\` Single source of truth for the \`believe_me\` allow-list. Each entry carries: type signature, operational justification, morally-equivalent existing axioms, downstream consumers. ## Test plan - [x] \`idris2 --build valence-shell.ipkg\` — exit 0 - [x] Guard pass: 2 occurrences in \`Axioms.idr\` / 2 axioms in registry - [x] Guard rejection test: added test \`believe_me\` in \`Model.idr\` — correctly flagged + exit 1 - [ ] CI \`idris-verification.yml\` green - [ ] Reviewer confirms Q4 policy (accept soft \`believe_me\` with named + gated axioms) ## Q4 policy implication This commit takes **Q4 option B** (soft policy with named + gated axioms). If you subsequently prefer **Q4 option A** (hard \"never believe_me\"), revert this PR and accept the **Q1-B** (Nat-interned \`Path\`) migration as the only path forward — substantially bigger work but no \`believe_me\` at all. ## Unblocks (follow-up work, not in this PR) With the axioms available, the following holes become tractable in subsequent per-PR closures: * \`equivTransProof\` (Model.idr:353) — needs \`elem\` transitivity on top of reflexivity * \`cnoWriteSameContentProof\` (Operations.idr:254) — uses the same \`equiv\`-membership chain * 4 \`?XXXPrfAfter\` sub-holes in Operations.idr (postcondition equalities) The 7 reversibility theorems in Operations.idr + 4 Composition.idr theorems need both this axiom infrastructure AND the Cat-A theorem-shape redesigns from #129/#130/#131. ## References * Builds on the discussion in #128 and #132 * Issue #119 (Idris2 hole inventory + closure plan audit) * Companion PRs (independent): #128 (Coq admit triumvirate), #132 (A-12 path-traversal containment) 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath mentioned this pull request Jun 2, 2026

proofs(idris2): Q1-C primitive-eq axiom pilot + equivRefl closure #133

Merged

5 tasks

hyperpolymath enabled auto-merge (squash) June 3, 2026 06:26

Merge branch 'main' into proofs/a12-path-traversal-containment

1c61a48

ci: realign validation matrix with current support

de12777

ci: build lean wrapper without make

ca461e7

ci: provide rust sources for fuzz builds

afed375

Merge branch 'main' into proofs/a12-path-traversal-containment

a0b96c4

hyperpolymath disabled auto-merge June 5, 2026 02:43

hyperpolymath merged commit cd2592d into main Jun 5, 2026
37 of 51 checks passed

hyperpolymath deleted the proofs/a12-path-traversal-containment branch June 5, 2026 02:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

proofs(lean4) + tests: A-12 path-traversal containment (closes frontier A-12)#132

proofs(lean4) + tests: A-12 path-traversal containment (closes frontier A-12)#132
hyperpolymath merged 6 commits into
mainfrom
proofs/a12-path-traversal-containment

hyperpolymath commented Jun 2, 2026

Uh oh!

github-actions Bot commented Jun 2, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented Jun 2, 2026

Summary

Changes

Test plan

References

Uh oh!

github-actions Bot commented Jun 2, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented Jun 5, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant