Status: Proof sketch documented; no checked contextual Rocq module exists yet
Rocq target module: rocq/liblevenshtein/ContextualCompletion/Visibility.v
Date: 2025-01-21
Authors: Formal Verification Team
This theorem establishes that hierarchical context visibility correctly implements lexical scoping: child contexts can see symbols from parent contexts (outer scopes), but parent contexts cannot see symbols from child contexts (inner scopes).
User Impact: This is the scope isolation correctness theorem. Without it:
Dependencies: Built on:
let engine = DynamicContextualCompletionEngine::new();
// Create scope hierarchy: global → module → function
let global = engine.create_root_context(0);
let module = engine.create_child_context(1, global).unwrap();
let function = engine.create_child_context(2, module).unwrap();
// Define symbols at different scopes
engine.finalize_direct(global, "global_var").unwrap();
engine.finalize_direct(module, "module_var").unwrap();
engine.finalize_direct(function, "local_var").unwrap();
// Query from function (child) - should see ALL ancestors
let results = engine.complete_finalized(function, "var", 10);
assert!(results.iter().any(|c| c.term == "global_var")); // ✓ Sees global
assert!(results.iter().any(|c| c.term == "module_var")); // ✓ Sees module
assert!(results.iter().any(|c| c.term == "local_var")); // ✓ Sees self
// Query from global (parent) - should NOT see descendants
let results = engine.complete_finalized(global, "var", 10);
assert!(results.iter().any(|c| c.term == "global_var")); // ✓ Sees self
assert!(!results.iter().any(|c| c.term == "module_var")); // ✗ Does not see module
assert!(!results.iter().any(|c| c.term == "local_var")); // ✗ Does not see function
// VIOLATION EXAMPLE (if theorem was false):
// Without this theorem, "local_var" could leak to global scope!
// This would break encapsulation and create security issues.
(* Ancestor relationship (from Theorem 1) *)
Fixpoint is_ancestor (tree : ContextTree) (ancestor child : ContextId) : bool :=
match parent tree child with
| None => false (* child is root *)
| Some p => if p = ancestor then true (* direct parent *)
else is_ancestor tree ancestor p (* recursive check *)
end.
(* Descendant relationship (inverse of ancestor) *)
Definition is_descendant (tree : ContextTree) (descendant ancestor : ContextId) : bool :=
is_ancestor tree ancestor descendant.
(* Visibility predicate: ctx1 visible from ctx2 *)
Definition visible_from (tree : ContextTree) (ctx1 ctx2 : ContextId) : Prop :=
ctx1 = ctx2 \/ (* Same context *)
is_ancestor tree ctx1 ctx2 = true. (* ctx1 is ancestor of ctx2 *)
(* Invisible predicate: ctx1 NOT visible from ctx2 *)
Definition invisible_from (tree : ContextTree) (ctx1 ctx2 : ContextId) : Prop :=
ctx1 <> ctx2 /\
is_ancestor tree ctx1 ctx2 = false.
Theorem hierarchical_visibility_soundness :
forall (tree : ContextTree) (parent child sibling : ContextId),
well_formed tree ->
is_parent tree parent child ->
is_parent tree parent sibling ->
child <> sibling ->
(* Part 1: Children see parents (upward visibility) *)
visible_from tree parent child /\
(* Part 2: Parents don't see children (no downward visibility) *)
invisible_from tree child parent /\
(* Part 3: Siblings don't see each other (no lateral visibility) *)
invisible_from tree sibling child /\
(* Part 4: Visibility is transitive upward *)
(forall ancestor, is_ancestor tree ancestor child = true ->
visible_from tree ancestor child) /\
(* Part 5: Invisibility is transitive downward *)
(forall descendant, is_descendant tree descendant parent = true ->
descendant <> child ->
invisible_from tree descendant parent).
Strategy: Prove visibility properties by case analysis on context relationships.
Claim: If child is a child of parent, then parent is visible from child.
Proof:
is_parent tree parent child means parent(child) = Some(parent)visible_from: visible_from tree parent child iff parent = child OR is_ancestor tree parent child = truechild <> parent (well-formedness: no self-loops)is_ancestor tree parent child = trueis_ancestor:
is_ancestor tree parent child
= match parent(child) with
| Some p => if p = parent then true else ...
parent(child) = Some(parent), the if condition succeedsis_ancestor tree parent child = truevisible_from tree parent child ✓ $\blacksquare$Claim: If child is a child of parent, then child is NOT visible from parent.
Proof:
invisible_from tree child parent iff child <> parent AND is_ancestor tree child parent = falsechild = parent
child <> parent ✓is_ancestor tree child parent = false
is_ancestor tree child parent = trueparent → ... → child → ... → parent (cycle!)is_ancestor tree child parent = false ✓invisible_from tree child parent ✓ $\blacksquare$Claim: If sibling and child are distinct children of parent, then sibling is NOT visible from child.
Proof:
invisible_from tree sibling child iff sibling <> child AND is_ancestor tree sibling child = falsesibling <> child (by assumption) ✓is_ancestor tree sibling child = false
is_ancestor tree sibling child iff sibling is on the path from child to rootchild to root: child → parent → ... → rootsibling to root: sibling → parent → ... → rootparent (sibling is NOT on child's path)is_ancestor tree sibling child = false ✓invisible_from tree sibling child ✓ $\blacksquare$Claim: If ancestor is an ancestor of child, then ancestor is visible from child.
Proof:
is_ancestor tree ancestor child = truevisible_from: visible_from tree ancestor child iff ancestor = child OR is_ancestor tree ancestor child = trueis_ancestor tree ancestor child = true, the second disjunct holdsvisible_from tree ancestor child ✓ $\blacksquare$Claim: If descendant is a descendant of parent (but not equal to child), then descendant is NOT visible from parent.
Proof:
is_descendant tree descendant parent = true AND descendant <> childis_descendant tree descendant parent = is_ancestor tree parent descendantis_ancestor tree parent descendant = trueinvisible_from tree descendant parent
descendant <> parent (given by well-formedness: ancestors $\ne$ descendants)is_ancestor tree descendant parent = falseis_ancestor tree descendant parent = trueis_ancestor tree parent descendant = true AND is_ancestor tree descendant parent = trueparent → ... → descendant → ... → parentis_ancestor tree descendant parent = false ✓invisible_from tree descendant parent ✓ $\blacksquare$Lemma 1 (Acyclic Tree):
Lemma tree_acyclic :
forall (tree : ContextTree) (ctx : ContextId),
well_formed tree ->
is_ancestor tree ctx ctx = false.
Proof: By contradiction. If is_ancestor tree ctx ctx = true, then there exists a path ctx → ... → ctx, violating well-formedness.
Lemma 2 (Ancestor Asymmetry):
Lemma ancestor_asymmetry :
forall (tree : ContextTree) (ctx1 ctx2 : ContextId),
well_formed tree ->
is_ancestor tree ctx1 ctx2 = true ->
is_ancestor tree ctx2 ctx1 = false.
Proof: Follows from Lemma 1 (acyclic) + transitivity. If both were true, we'd have a cycle.
Lemma 3 (Path Divergence):
Lemma sibling_paths_diverge :
forall (tree : ContextTree) (parent child1 child2 : ContextId),
well_formed tree ->
is_parent tree parent child1 ->
is_parent tree parent child2 ->
child1 <> child2 ->
~(is_ancestor tree child1 child2) /\ ~(is_ancestor tree child2 child1).
Proof: Paths from siblings to root diverge at their common parent, so neither sibling is on the other's path.
Lemma 4 (Visible Contexts Monotonicity):
Lemma visible_contexts_subset :
forall (tree : ContextTree) (parent child : ContextId),
well_formed tree ->
is_parent tree parent child ->
exists (visible_child visible_parent : list ContextId),
visible_child = visible_contexts tree child /\
visible_parent = visible_contexts tree parent /\
(forall ctx, In ctx visible_parent -> In ctx visible_child).
Proof: Child's visible contexts = [child] ++ parent's visible contexts. Therefore parent's visible set is a strict subset.
Source: src/contextual/context_tree.rs:335-349, src/contextual/engine.rs:1782-1802
// src/contextual/context_tree.rs:335-349
pub fn is_descendant(&self, child_id: ContextId, ancestor_id: ContextId) -> bool {
if child_id == ancestor_id {
return false; // Strict descendant (not reflexive)
}
let mut current = self.parent(child_id);
while let Some(parent_id) = current {
if parent_id == ancestor_id {
return true; // Found ancestor in parent chain
}
current = self.parent(parent_id); // Continue up the tree
}
false // Reached root without finding ancestor
}
Correspondence:
child <> ancestor check (non-reflexive)child_id (upward traversal)is_ancestor recursion)false if ancestor not found (not in parent chain)// src/contextual/engine.rs (simplified from lines 1090-1120)
pub fn complete_finalized(&self, context: ContextId, query: &str, max_distance: usize)
-> Vec<Completion>
{
let mut results = Vec::new();
// Get visible contexts (self + ancestors)
let visible = self.context_tree.visible_contexts(context);
for ctx in visible {
// Query dictionary for terms finalized in this context
if let Some(terms) = self.finalized_symbols.get(&ctx) {
for term in terms {
let distance = Self::levenshtein_distance(query, term);
if distance <= max_distance {
results.push(Completion {
term: term.clone(),
distance,
source_context: ctx,
is_draft: false,
});
}
}
}
}
results
}
Correspondence:
visible_contexts(context) includes context + all ancestors (Part 1 + Part 4)visible_contexts(parent) does NOT include children (Part 2)visible_contexts (Part 3)// src/contextual/engine.rs:1782-1802
#[test]
fn test_complete_hierarchical_visibility() {
let engine = DynamicContextualCompletionEngine::new();
let global = engine.create_root_context(0);
let func = engine.create_child_context(1, global).unwrap();
// Global term
engine.finalize_direct(global, "global_var").unwrap();
// Local term
engine.finalize_direct(func, "local_var").unwrap();
// Query from func - should see both (PART 1: child sees parent)
let results = engine.complete_finalized(func, "var", 10);
assert!(results.iter().any(|c| c.term == "global_var")); // ✓
assert!(results.iter().any(|c| c.term == "local_var")); // ✓
// Query from global - should NOT see local_var (PART 2: parent doesn't see child)
let results = engine.complete_finalized(global, "var", 10);
assert!(results.iter().any(|c| c.term == "global_var")); // ✓
assert!(!results.iter().any(|c| c.term == "local_var")); // ✓ Invisible!
}
Correspondence:
Unit Tests: src/contextual/context_tree.rs:505-535 (#[cfg(test)])
#[test]
fn test_is_descendant() {
let mut tree = ContextTree::new();
let root = tree.create_root(1);
let child = tree.create_child(2, root).unwrap();
let grandchild = tree.create_child(3, child).unwrap();
// Descendant relationships
assert!(tree.is_descendant(child, root)); // Direct child
assert!(tree.is_descendant(grandchild, root)); // Transitive
assert!(tree.is_descendant(grandchild, child)); // Direct child
// NOT descendant (upward, lateral, or self)
assert!(!tree.is_descendant(root, child)); // Parent NOT descendant of child
assert!(!tree.is_descendant(child, grandchild)); // Parent NOT descendant of grandchild
assert!(!tree.is_descendant(child, child)); // NOT self-descendant
}
Integration Tests: src/contextual/engine.rs:1782-1802
See test above (test_complete_hierarchical_visibility).
Candidate Property-Based Tests:
Using proptest crate:
proptest! {
// Asymmetry: If A is ancestor of B, B is NOT ancestor of A
#[test]
fn prop_ancestor_asymmetry(tree: ContextTree, ctx1: ContextId, ctx2: ContextId) {
if tree.is_descendant(ctx1, ctx2) {
prop_assert!(!tree.is_descendant(ctx2, ctx1));
}
}
// Transitivity: If A is ancestor of B and B is ancestor of C, then A is ancestor of C
#[test]
fn prop_ancestor_transitivity(
tree: ContextTree,
ctx1: ContextId,
ctx2: ContextId,
ctx3: ContextId
) {
if tree.is_descendant(ctx2, ctx1) && tree.is_descendant(ctx3, ctx2) {
prop_assert!(tree.is_descendant(ctx3, ctx1));
}
}
// Visibility completeness: visible_contexts includes all ancestors
#[test]
fn prop_visible_includes_ancestors(tree: ContextTree, ctx: ContextId) {
let visible = tree.visible_contexts(ctx);
for ancestor in tree.ancestors(ctx) {
prop_assert!(visible.contains(&ancestor));
}
}
// Visibility soundness: visible_contexts excludes all non-ancestors
#[test]
fn prop_visible_excludes_non_ancestors(tree: ContextTree, ctx: ContextId) {
let visible = tree.visible_contexts(ctx);
for other in tree.all_contexts() {
if !tree.is_descendant(ctx, other) && other != ctx {
prop_assert!(!visible.contains(&other));
}
}
}
}
Depends on:
visible_contexts() implementationRequired by:
Complements:
Scenario: User writing nested function in Rholang
contract outer(@x) = {
new temp in { // temp is local to outer
contract inner(@y) = {
new result in { // result is local to inner
// ... computation ...
}
}
}
}
// At module level, user types "re" and expects:
// - "rho" (builtin)
// - "receive" (builtin)
//
// WITHOUT Theorem 6, might also see:
// - "result" (leaked from inner!) ← PRIVACY VIOLATION
Consequences:
// At module level, "re" completes to:
completions = ["rho", "receive"] // ✓ Only global symbols
// Inside "inner", "re" completes to:
completions = ["result", "rho", "receive"] // ✓ Local + global
// Inside "outer" (but outside "inner"), "re" completes to:
completions = ["rho", "receive"] // ✓ "result" is invisible (from inner)
File: rocq/liblevenshtein/ContextualCompletion/Visibility.v
Proof Structure:
(* Imports *)
Require Import Coq.Lists.List.
Require Import ContextTree.
(* Main theorem *)
Theorem hierarchical_visibility_soundness : (* ... *).
Proof.
intros tree parent child sibling Hwf Hparent1 Hparent2 Hneq.
split. (* Part 1: Children see parents *)
- unfold visible_from. right. apply parent_is_ancestor. assumption.
split. (* Part 2: Parents don't see children *)
- apply descendant_not_ancestor_of_parent. assumption.
split. (* Part 3: Siblings don't see each other *)
- apply sibling_not_ancestor. assumption.
split. (* Part 4: Transitivity upward *)
- intros ancestor Hanc. unfold visible_from. right. assumption.
(* Part 5: Transitivity downward *)
- intros descendant Hdesc Hneq'. apply descendant_not_visible_from_ancestor.
+ assumption.
+ assumption.
Qed.
Current Implementation: $\mathcal{O}(\text{depth})$ for is_descendant check (follows parent chain)
Optimization candidate (if needed for large trees):
[left, right] interval during DFSctx1 is descendant of ctx2 iff left2 < left1 < right1 < right2\mathcal{O}(1)$ check vs $\mathcal{O}(\text{depth})$When to optimize:
is_descendant queries (currently rare)Last Updated: 2025-01-21 Review trigger: Reconcile this page when a checked contextual Rocq module is added.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |