Vyper CLI vs test export: source_id discrepancy for main module

[lukaszcz]

Version Information

• vyper Version (output of vyper --version): 0.4.4+commit.24c51cda
• OS: osx (doesn't matter)
• Python Version (output of python --version): Python 3.14.3

Summary

The Vyper CLI (vyper -f annotated_ast) and the Vyper test framework
(compile_code) assign different source_id values to the main module.
This causes the HOL formalization to break when processing CLI-generated JSON.

The discrepancy

Generation method	Main module source_id	self.x variable_reads source_id
vyper foo.vy -f annotated_ast (CLI)	0	0
compile_code(src, ...) (Python API)	-1	-1
pytest --export (test framework)	-1	-1

Root cause

The CLI uses FilesystemInputBundle which assigns source_ids sequentially
starting from 0:

# vyper/compiler/input_bundle.py:100,113-120
self._source_id_counter = 0

def _generate_source_id(self, resolved_path):
    if resolved_path not in self._source_ids:
        self._source_ids[resolved_path] = self._source_id_counter
        self._source_id_counter += 1
    return self._source_ids[resolved_path]

The compile_code function creates a FileInput with source_id=-1:

# vyper/compiler/__init__.py:157-174
def compile_code(source_code, ..., source_id: int = -1, ...):
    file_input = FileInput(source_id=source_id, ...)

The test framework uses compile_code (via _compile in base_env.py), so
all test exports get source_id=-1 for the main module.

Impact on HOL formalization

The HOL formalization maps source_ids to num option:

(* frontend/jsonToVyperScript.sml:19-22 *)
source_id_to_nsid (src_id:int) =
  if src_id = -1 then NONE
  else SOME (Num (src_id + &builtin_source_id_offset))   (* offset = 2 *)

And stores the main module under NONE in cx.sources:

(* frontend/jsonToVyperScript.sml:1372 *)
let sources = (NONE, translate_module main) :: MAP translate_imported_module imports

With CLI-generated JSON (source_id=0):

• source_id_to_nsid 0 = SOME 2
• self.x becomes TopLevelName (SOME 2, "x")
• lookup_global cx (SOME 2) ... calls get_module_code cx (SOME 2)
• ALOOKUP mods (SOME 2) fails — main module is stored under NONE

With test-generated JSON (source_id=-1):

• source_id_to_nsid (-1) = NONE
• self.x becomes TopLevelName (NONE, "x")
• lookup_global cx NONE ... calls get_module_code cx NONE
• ALOOKUP mods NONE succeeds

Potential fixes

Make the CLI also use source_id=-1 for the main module, matching compile_code. This is arguably a Vyper bug since the two APIs produce semantically different output.

[charles-cooper]

I don't think hol should care about the exact values of the source id..?

[lukaszcz]

Currently, there is a distinction between the main module (self) and the other modules. Maybe this should be a HOL formalization issues - remove the option from src_id_opt and make self a normal module. I'm not sure though if the reason for the current state isn't that sometimes self needs special treatment. Currently, self is indicated by NONE and other modules by SOME source_id.

In any case, the JSON Vyper produces for generated tests is different from the JSON it produces for the same files via the CLI. IMO, there shouldn't be such a discrepancy - the output should be the same in both cases.

[charles-cooper]

we can have the exporter use source_id=0 or something

but actually idk when src_id_opt can be NONE? like i don't think vyper ever produces none, it must be something in the translation

[lukaszcz]

we can have the exporter use source_id=0 or something

but actually idk when src_id_opt can be NONE? like i don't think vyper ever produces none, it must be something in the translation

Yes, the translation just converts -1 to NONE. So it currently requires the main module to have source id -1.

[charles-cooper]

that's.. so weird, i consider this a bug in the translator. self (the compilation target) is just the toplevel module, it should be identified during parsing the json