From fd9b4f2291b88b4722c4e953b1d86b6e0ceeb9ec Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Wed, 12 Aug 2026 10:33:55 +0200 Subject: [PATCH] Fix the check_porting bug when there are name collisions --- Iris/Iris/HeapLang/Lib/SpinLock.lean | 22 ++--- Iris/Iris/Std/RocqPorting.lean | 10 +++ scripts/README.md | 5 ++ scripts/check_porting.py | 116 +++++++++++++++++++++++---- 4 files changed, 125 insertions(+), 28 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean index fe09e668a..d22cdc944 100644 --- a/Iris/Iris/HeapLang/Lib/SpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean @@ -20,19 +20,19 @@ open BI Iris ProgramLogic namespace SpinLock -@[rocq_alias heap_lang.newlock] +@[rocq_alias heap_lang.spin_lock.newlock] def newlock : Val := hl_val( λ _, ref(#false)) @[rocq_alias heap_lang.try_acquire] def tryAcquire : Val := hl_val( λ l, snd(cmpXchg(l, #false, #true))) -@[rocq_alias heap_lang.acquire] +@[rocq_alias heap_lang.spin_lock.acquire] def acquire : Val := hl_val( rec acquire l := if (&tryAcquire l) then #() else acquire l) -@[rocq_alias heap_lang.release] +@[rocq_alias heap_lang.spin_lock.release] def release : Val := hl_val( λ l, l ← #false) @@ -48,14 +48,14 @@ section Predicates variable [HeapLangGS hlc GF] [SpinLockG GF] -@[rocq_alias heap_lang.locked] +@[rocq_alias heap_lang.spin_lock.locked] def locked (γ : GName) : IProp GF := token γ -@[rocq_alias heap_lang.lock_inv] +@[rocq_alias heap_lang.spin_lock.lock_inv] def lockInv (γ : GName) (l : Loc) (R : IProp GF) : IProp GF := iprop% ∃ b : Bool, (l ↦ some hl_val(#b)) ∗ (if b then True else locked γ ∗ R) -@[rocq_alias heap_lang.is_lock] +@[rocq_alias heap_lang.spin_lock.is_lock] def isLock (γ : GName) (lk : Val) (R : IProp GF) : IProp GF := iprop% ∃ l : Loc, ⌜lk = Val.lit (.loc l)⌝ ∧ inv spinlockN (lockInv γ l R) @@ -65,11 +65,11 @@ instance instIsLockPersistent (γ : GName) (lk : Val) (R : IProp GF) : Persisten instance instLockedTimeless (γ : GName) : Timeless (locked (GF := GF) γ) := by unfold locked; infer_instance -@[rocq_alias heap_lang.locked_exclusive] +@[rocq_alias heap_lang.spin_lock.locked_exclusive] theorem instLockedExclusive (γ : GName) : locked γ ∗ locked γ ⊢@{IProp GF} False := token_exclusive γ -@[rocq_alias heap_lang.is_lock_iff] +@[rocq_alias heap_lang.spin_lock.is_lock_iff] theorem is_lock_iff (γ : GName) (lk : Val) (R₁ R₂ : IProp GF) : isLock γ lk R₁ ⊢ (▷ □ (R₁ ∗-∗ R₂)) -∗ isLock γ lk R₂ := by unfold isLock lockInv @@ -96,7 +96,7 @@ section Specs variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [SpinLockG GF] -@[rocq_alias heap_lang.newlock_spec_delay_init] +@[rocq_alias heap_lang.spin_lock.newlock_spec_delay_init] theorem newlock_spec : ⊢ □ ∀ (Φ : Val → IProp GF), (∀ (v : Val) (γ : GName), (∀ R E, R ={E}=∗ isLock γ v R) -∗ Φ v) -∗ @@ -162,7 +162,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : simp only [Bool.false_eq_true, ↓reduceIte] itrivial -@[rocq_alias heap_lang.acquire_spec] +@[rocq_alias heap_lang.spin_lock.acquire_spec] theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : ⊢ □ ∀ (Φ : Val → IProp GF), isLock γ lk R -∗ @@ -184,7 +184,7 @@ theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : simp only [if_pos] iframe -@[rocq_alias heap_lang.release_spec] +@[rocq_alias heap_lang.spin_lock.release_spec] theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) : ⊢ □ ∀ (Φ : Val → IProp GF), isLock γ lk R ∗ (locked γ ∗ R) -∗ diff --git a/Iris/Iris/Std/RocqPorting.lean b/Iris/Iris/Std/RocqPorting.lean index 741416df8..db35566f2 100644 --- a/Iris/Iris/Std/RocqPorting.lean +++ b/Iris/Iris/Std/RocqPorting.lean @@ -63,6 +63,16 @@ For the heap_lang package (`iris_heap_lang/` upstream) write: ``` @[rocq_alias heap_lang.pointsto] ``` + +File-local declarations normally follow the same convention. If a local name +occurs in multiple tracked Rocq files, include the source filename to make the +aliases distinct. For example, both +`iris_heap_lang/lib/spin_lock.v` and `iris_heap_lang/lib/ticket_lock.v` contain a +local `lock_inv`, so their aliases are: +``` +@[rocq_alias heap_lang.spin_lock.lock_inv] +@[rocq_alias heap_lang.ticket_lock.lock_inv] +``` -/ open Lean Elab Command diff --git a/scripts/README.md b/scripts/README.md index ef9a09929..121b57bbf 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -68,6 +68,11 @@ directory argument of `#rocq_ignore_file` / `#rocq_concept`: #rocq_ignore_file heap_lang.lib "diverge.v" "Not needed" ``` +File-local declarations use the short convention unless the same name occurs +in multiple tracked files. Ambiguous locals include their source filename, so +the two local `lock_inv` declarations in the spin and ticket locks are +`heap_lang.spin_lock.lock_inv` and `heap_lang.ticket_lock.lock_inv`. + ## Configuration Files - **`scripts/ROCQ_REVISION`** -- The Iris-Rocq commit SHA to track against. diff --git a/scripts/check_porting.py b/scripts/check_porting.py index 408a9ce31..f93b36401 100755 --- a/scripts/check_porting.py +++ b/scripts/check_porting.py @@ -170,14 +170,35 @@ def qualify(name: str, rel_path: str) -> str: return (pkg.prefix if pkg else "") + name +def qualify_local(name: str, rel_path: str) -> str: + """Qualify a file-local name with its Rocq source filename. + + This is used only when the short name is ambiguous across source files. + + >>> qualify_local("lock_inv", "iris_heap_lang/lib/spin_lock.v") + 'heap_lang.spin_lock.lock_inv' + >>> qualify_local("helper", "iris/algebra/ofe.v") + 'ofe.helper' + """ + pkg = package_of(rel_path) + stem = rel_path.rsplit("/", 1)[-1].removesuffix(".v") + return f"{pkg.prefix if pkg else ''}{stem}.{name}" + + def unqualify(name: str, rel_path: str) -> str: """Strip that prefix again for display; the section already shows it. >>> unqualify("heap_lang.pointsto", "iris_heap_lang/primitive_laws.v") 'pointsto' + >>> unqualify("heap_lang.spin_lock.lock_inv", "iris_heap_lang/lib/spin_lock.v") + 'lock_inv' """ pkg = package_of(rel_path) - return name.removeprefix(pkg.prefix) if pkg else name + short = name.removeprefix(pkg.prefix) if pkg else name + if pkg: + source_prefix = rel_path.rsplit("/", 1)[-1].removesuffix(".v") + "." + short = short.removeprefix(source_prefix) + return short def split_path(rel_path: str) -> tuple[str, str, str]: @@ -230,13 +251,13 @@ def folder_path(folder: str, file: str) -> str: r"Fact|Remark|Example|Canonical\s+Structure" ) -# Matches a named definition line. Captures the identifier (group 1). +# Matches a named definition line. Captures the modifiers and identifier. # Handles optional prefixes like "Global", "Local", "Program", "#[export]". # Identifiers may contain apostrophes (e.g., csum_updateP'_l). _DEF_RE = re.compile( - rf"^\s*(?:(?:Global|Local|Program|#\[(?:export|global)\])\s+)*" + rf"^\s*(?P(?:(?:Global|Local|Program|#\[(?:export|global|local)\])\s+)*)" rf"(?:{_DEF_KEYWORDS})\s+" - rf"(\w[\w']*)", + rf"(?P\w[\w']*)", re.MULTILINE, ) @@ -292,30 +313,43 @@ def _strip_comments(text: str) -> str: return "".join(out) -def parse_rocq_file(text: str) -> list[str]: - """Extract fully-qualified definition names from a Rocq .v file. +@dataclass(frozen=True) +class ParsedDefinition: + name: str + is_local: bool = False + + +def parse_rocq_file(text: str) -> list[ParsedDefinition]: + """Extract definitions and their locality from a Rocq .v file. Module prefixes are included; Section prefixes are not. A mutual block declares one name per `with` clause: >>> parse_rocq_file("Inductive expr :=\\n | Val (v : val)\\nwith val :=\\n | LitV.") - ['expr', 'val'] + [ParsedDefinition(name='expr', is_local=False), ParsedDefinition(name='val', is_local=False)] Only at column 0, so an indented `with` -- a mutual helper local to another definition's body -- contributes no name: >>> parse_rocq_file("Fixpoint f x := 0\\n with g y := 1.") - ['f'] + [ParsedDefinition(name='f', is_local=False)] + + `Local` and `#[local]` declarations retain that information so collisions + between private names in separate libraries can be disambiguated later: + + >>> parse_rocq_file("Local Definition helper := 0.\\n#[local] Instance instFoo : Foo := {}.") + [ParsedDefinition(name='helper', is_local=True), ParsedDefinition(name='instFoo', is_local=True)] """ text = _strip_comments(text) # A mutual `with` sometimes sits alone on its line, the name following on the # next. Join the two so the line-based matching below sees one head. text = re.sub(r"^with[ \t]*\n[ \t]*", "with ", text, flags=re.MULTILINE) - names: list[str] = [] + definitions: list[ParsedDefinition] = [] module_stack: list[str] = [] # current Module nesting, used for name qualification section_names: set[str] = set() # track Section names so End can distinguish them + mutual_is_local = False # `with` clauses inherit the head declaration's locality for line in text.split("\n"): # Track Module open (but not Module Type, which is a signature) @@ -344,12 +378,56 @@ def parse_rocq_file(text: str) -> list[str]: # Extract definition name and qualify with Module prefix. A mutual # block's `with` clauses declare names too, so they count as well. - if m := _DEF_RE.match(line) or _WITH_DEF_RE.match(line): + if m := _DEF_RE.match(line): + ident = m.group("identifier") + modifiers = m.group("modifiers") + mutual_is_local = "Local" in modifiers.split() or "#[local]" in modifiers.split() + qualified = ".".join([*module_stack, ident]) if module_stack else ident + definitions.append(ParsedDefinition(qualified, mutual_is_local)) + elif m := _WITH_DEF_RE.match(line): ident = m.group(1) qualified = ".".join([*module_stack, ident]) if module_stack else ident - names.append(qualified) + definitions.append(ParsedDefinition(qualified, mutual_is_local)) - return names + return definitions + + +def qualify_definitions( + parsed: dict[str, list[ParsedDefinition]], +) -> dict[str, list[str]]: + """Apply package prefixes and disambiguate file-local name collisions. + + Unique local names retain the existing short alias convention. If the same + qualified short name occurs in multiple files, local occurrences gain their + source filename so every declaration has a distinct key. + + >>> qualified = qualify_definitions({ + ... "iris_heap_lang/lib/spin_lock.v": [ParsedDefinition("lock_inv", True)], + ... "iris_heap_lang/lib/ticket_lock.v": [ParsedDefinition("lock_inv", True)], + ... }) + >>> qualified["iris_heap_lang/lib/spin_lock.v"] + ['heap_lang.spin_lock.lock_inv'] + >>> qualified["iris_heap_lang/lib/ticket_lock.v"] + ['heap_lang.ticket_lock.lock_inv'] + """ + base_names = { + path: [qualify(definition.name, path) for definition in definitions] + for path, definitions in parsed.items() + } + files_by_name: dict[str, set[str]] = defaultdict(set) + for path, names in base_names.items(): + for name in names: + files_by_name[name].add(path) + ambiguous = {name for name, files in files_by_name.items() if len(files) > 1} + + return { + path: [ + qualify_local(definition.name, path) + if definition.is_local and base_name in ambiguous else base_name + for definition, base_name in zip(definitions, base_names[path], strict=True) + ] + for path, definitions in parsed.items() + } # ============================================================================ @@ -424,7 +502,7 @@ def download_iris_rocq(commit: str, cache_dir: Path) -> tuple[dict[str, list[str log(f"Downloaded {len(tarball_data) / 1024:.0f} KB, parsing...") # Parse every .v file under the tracked source roots. - definitions: dict[str, list[str]] = {} + parsed: dict[str, list[ParsedDefinition]] = {} with tarfile.open(fileobj=io.BytesIO(tarball_data), mode="r:gz") as tf: for member in tf.getmembers(): if not member.isfile() or not member.name.endswith(".v"): @@ -439,10 +517,13 @@ def download_iris_rocq(commit: str, cache_dir: Path) -> tuple[dict[str, list[str fobj = tf.extractfile(member) if fobj is None: continue - names = parse_rocq_file(fobj.read().decode("utf-8", errors="replace")) - defs = [qualify(n, rel_path) for n in names] - if defs: - definitions[rel_path] = defs + parsed_definitions = parse_rocq_file( + fobj.read().decode("utf-8", errors="replace") + ) + if parsed_definitions: + parsed[rel_path] = parsed_definitions + + definitions = qualify_definitions(parsed) # Cache the parsed definitions so we don't re-download next time. cache_file.parent.mkdir(parents=True, exist_ok=True) @@ -575,6 +656,7 @@ def compute_report( Names arrive already qualified by their package prefix, so `pointsto` from `iris` and `heap_lang.pointsto` from `iris_heap_lang` are distinct keys. + Ambiguous file-local names also carry their source filename. """ report = Report(rocq_commit=rocq_commit, lean_rev=lean_rev, concepts=concepts)