wehub-resource-sync
26382a7ac6
CI / Clippy (push) Failing after 15m13s
CI / Test (ubuntu-latest) (push) Failing after 16m1s
CI / Test (macos-latest) (push) Has been cancelled
CI / Test (windows-latest) (push) Has been cancelled
CI / Build (no embeddings / no ORT) (push) Has been cancelled
CI / Format (push) Has been cancelled
CI / Cookbook (Node) (push) Has been cancelled
CI / Pi Extension (Node) (push) Has been cancelled
CI / Rust SDK (lean-ctx-client) (push) Has been cancelled
CI / Embed SDK (lean-ctx-sdk) (push) Has been cancelled
CI / Python SDK (leanctx) (push) Has been cancelled
CI / Hermes Plugin (Python) (push) Has been cancelled
CI / SDK Conformance Matrix (push) Has been cancelled
CI / Coverage (push) Has been cancelled
CI / cargo-deny (push) Has been cancelled
CI / Adversarial Safety (push) Has been cancelled
CI / Benchmarks (push) Has been cancelled
CI / Output-Quality Gate (eval A/B) (push) Has been cancelled
CI / Documentation (push) Has been cancelled
CI / CI Green (push) Has been cancelled
JetBrains Plugin / Actionlint (push) Has been cancelled
CodeQL / Analyze (actions) (push) Has been cancelled
CodeQL / Analyze (javascript-typescript) (push) Has been cancelled
CodeQL / Analyze (rust) (push) Has been cancelled
JetBrains Plugin / Validation (push) Has been cancelled
JetBrains Plugin / Build (push) Has been cancelled
JetBrains Plugin / Test (push) Has been cancelled
Security Check / Security Scan (push) Has been cancelled
76 lines
2.3 KiB
Lean4
76 lines
2.3 KiB
Lean4
/-
|
||
LeanCTX Formal Verification — PathJail Proofs
|
||
|
||
Mirrors: rust/src/core/pathjail.rs
|
||
-/
|
||
import LeanCtxProofs.Basic
|
||
|
||
namespace LeanCtxProofs.Policy.PathJail
|
||
|
||
abbrev Path := List String
|
||
|
||
structure JailConfig where
|
||
root : Path
|
||
allowPaths : List Path
|
||
deriving DecidableEq, Repr
|
||
|
||
def isUnderPfx (pfx candidate : Path) : Bool :=
|
||
match pfx, candidate with
|
||
| [], _ => true
|
||
| _ :: _, [] => false
|
||
| p :: ps, c :: cs => p == c && isUnderPfx ps cs
|
||
|
||
def jailPathAllowed (config : JailConfig) (candidate : Path) : Bool :=
|
||
isUnderPfx config.root candidate ||
|
||
config.allowPaths.any (isUnderPfx · candidate)
|
||
|
||
-- ============================================================================
|
||
-- Theorems
|
||
-- ============================================================================
|
||
|
||
theorem jail_path_sound (config : JailConfig) (candidate : Path) :
|
||
jailPathAllowed config candidate = true →
|
||
isUnderPfx config.root candidate = true ∨
|
||
∃ allowed ∈ config.allowPaths, isUnderPfx allowed candidate = true := by
|
||
intro h
|
||
unfold jailPathAllowed at h
|
||
simp [Bool.or_eq_true] at h
|
||
cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h =>
|
||
right
|
||
simp [List.any_eq_true] at h
|
||
exact h
|
||
|
||
theorem jail_no_escape (config : JailConfig) (candidate : Path)
|
||
(h_root : isUnderPfx config.root candidate = false)
|
||
(h_allow : ∀ p ∈ config.allowPaths, isUnderPfx p candidate = false) :
|
||
jailPathAllowed config candidate = false := by
|
||
unfold jailPathAllowed
|
||
simp [Bool.or_eq_true, h_root, List.any_eq_true]
|
||
intro p hp
|
||
exact h_allow p hp
|
||
|
||
theorem jail_empty_allow_list (root candidate : Path) :
|
||
jailPathAllowed ⟨root, []⟩ candidate = isUnderPfx root candidate := by
|
||
unfold jailPathAllowed
|
||
simp [List.any_eq_true]
|
||
|
||
theorem jail_allow_monotone (config : JailConfig) (newAllow : Path) (candidate : Path) :
|
||
jailPathAllowed config candidate = true →
|
||
jailPathAllowed { root := config.root, allowPaths := newAllow :: config.allowPaths } candidate = true := by
|
||
intro h
|
||
unfold jailPathAllowed at *
|
||
simp [Bool.or_eq_true, List.any_eq_true] at *
|
||
rcases h with h | ⟨p, hp, hpref⟩
|
||
· left; exact h
|
||
· right
|
||
exact Or.inr ⟨p, hp, hpref⟩
|
||
|
||
theorem isUnderPfx_refl (p : Path) : isUnderPfx p p = true := by
|
||
induction p with
|
||
| nil => simp [isUnderPfx]
|
||
| cons x xs ih => simp [isUnderPfx, ih]
|
||
|
||
end LeanCtxProofs.Policy.PathJail
|