Error reference
Every error Velaris can give, from the error table in the compiler source, which the test suite holds against every code the compiler can raise, so this page cannot go stale. In the message templates, braces are filled with your program’s names and values; every error also arrives with numbered fixes, and as JSON with --json.
| Code | What it means | Message template |
|---|---|---|
| E000 | a character the lexer cannot read, or a run that stopped without a Velaris error to report | unexpected character {source[pos]!r} |
| E001 | the program's file cannot be found | cannot find file '{path}' |
| E002 | an unknown escape sequence in a text literal | unknown escape '\\{e}' in text |
| E100 | the parser expected something else here | expected '{want}' but found '{t.text or 'end of file'}' |
| E101 | a token that cannot start an expression here | unexpected '{t.text}' |
| E102 | an expression that nests, or chains operators, too deeply, or blocks nested too deeply | blocks nest more than {BLOCK_NEST_LIMIT} deep here (an 'if', 'while', 'for' or 'else if' inside another) |
| E200 | an unknown function, or an import with no such function | '{ns}' has no function called '{fname}' |
| E204 | a function named like a built-in, which would shadow it | '{n}' is the name of a built-in, so a function called '{n}' would shadow it; through 7.x the built-in silently won and this function was never reached |
| E300 | an effect used but not declared in 'uses', or a name in 'uses' that is not an effect | function '{fn.name}' declares '{unknown[0]}', which is not an effect; the effects are {', '.join(ALL_EFFECTS)} |
| E310 | an effect outside the run's budget (while running); or a promise that calls a function with effects or uses 'try' | the '{where}' promise of '{fn.name}' calls '{node.name}' which has effects ({', '.join(sorted(eff))}); promises must be pure |
| E311 | a Python module outside the run's ffi: grants was reached | '{what}' reaches {described}, whose owning Python module cannot be determined; this run allows ffi:{granted} and refuses what it cannot place |
| E313 | a path outside the run's fs grants | '{what}' reaches '{path}' (resolved: {real}), which this run's fs grants do not cover |
| E314 | a host or port outside the run's net grants | '{what}' reaches host '{host}', which this run does not allow: {why} |
| E315 | the run's fs or net operation count was reached | '{what}' is the {_state.OP_COUNTS[kind]}{_ordinal(_state.OP_COUNTS[kind])} {kind} operation, and this run allows {limit} |
| E316 | a file larger than the read ceiling (raise it with --max-read) | '{args[0]}' is {size} bytes, over the read ceiling of {_state.MAX_READ_BYTES} bytes - a file is read whole, into memory, so a large one is capped |
| E317 | a network request whose socket peer is a proxy the run's net grants do not cover (an ambient HTTP_PROXY / HTTPS_PROXY) | an ambient proxy ({proxy}) would carry this request, and its host {peer}:{port} is outside this run's net grants: a net grant bounds the URL's host, and from 8.0 also the socket's peer |
| E318 | read_file on a documented credential location; read a secret with read_file_secret, or grant its exact path | '{what}' reaches '{path}' (resolved: {real}), a documented credential location the fs grants do not name explicitly; a broad grant does not include it |
| E400 | there is no 'main' function | there is no 'main' - a program needs somewhere to start |
| E401 | the wrong number of arguments, or parameters on 'main' | '{node.name}' expects {len(ptypes)} argument(s) but got {len(node.args)} |
| E402 | an unknown variable, or break or continue, which the language does not have | unknown variable '{node.name}': it is not defined where this function value is written, nor in it |
| E403 | division or remainder by zero while running | percent_of with a denominator of zero |
| E405 | random(n) with n less than 1 | random(n) needs n greater than 0 |
| E406 | the placeholders in a format text and the values given do not match | this text has {holes} placeholder(s) but got {given} value(s) |
| E407 | a whole number grew past 64 bits | this whole number has {len(t.text)} digits (whole numbers go from -9223372036854775808 to 9223372036854775807) |
| E408 | an exit code outside 0 to 255 | an exit code must be between 0 and 255, not {code} |
| E500 | an unknown type | |
| E501 | types do not match | '{node.name}' here is the builtin, which needs {want} for argument {i}; the function '{node.name}' of this program is hidden by it |
| E502 | a value is needed from a function that returns nothing | argument {i} of '{node.name}' is a call to a function that returns nothing |
| E503 | a return does not match the declared return type | '{fn.name}' promises to return {declared_ret} but this return gives nothing |
| E504 | an 'if' or 'while' condition that is not a Bool | 'while' needs a yes/no condition (Bool), but this is {c} |
| E505 | a requires, ensures or invariant that is not a Bool | 'invariant' must be a yes/no promise (Bool) |
| E506 | an empty list or map with no type to say what it holds | cannot tell what an empty list holds |
| E507 | a record defined twice, a field given twice in a record, or one name used for a record and a function | '{r.name}' is used for both a record and a function |
| E508 | an unknown record | unknown record '{node.name}' |
| E509 | a record value with a missing, unknown or repeated field, or a map with a repeated key | record '{node.name}' is missing field(s): {', '.join(missing)} |
| E510 | a field that the value does not have | record '{t}' has no field '{node.field}' |
| E511 | a record changed in place | records cannot be changed in place |
| E512 | an imported file cannot be found | cannot import '{path}': it is not UTF-8 text, so it is not Velaris source |
| E513 | a function or record defined in two files | function '{f.name}' is defined {where} |
| E514 | a variable named like an import | '{name}' is the name of an import, so it cannot also be a variable |
| E515 | an import from outside the directory a program is served from, or of a file there that is not a .vel file | cannot import '{path}': {why} |
| E520 | a failure that is ignored: a call that can fail, not handled with check or passed up with try | 'get' on a map can fail - the key may be missing, and that cannot be ignored |
| E521 | 'try' in a function that cannot fail, or a failure that escaped the program while running | 'try' passes failure up, but '{fn.name}' cannot fail |
| E522 | 'try' or 'check' on a call that cannot fail | '{shown_name(node.subject.name)}' cannot fail - call it directly, no check needed |
| E523 | 'fail' in a function that does not declare 'or fail' | 'fail' is used, but '{fn.name}' does not declare it can fail |
| E524 | 'main' declared 'or fail' | 'main' cannot be 'or fail' - there is no one above it to handle the failure |
| E525 | a check's ok arm names the result of a call that returns nothing, or leaves a returned value unnamed | '{node.subject.name}' returns nothing - write 'ok {{ ... }}' with no name |
| E530 | a function passed as a value that has effects or can fail | '{f2.name}' uses effects ({', '.join(sorted(f2.effects))}) - only pure functions can be passed as values |
| E540 | a type variable that appears only in the return type | type variable '{tv}' must appear in at least one parameter (a {tv} only in the return type cannot be inferred) |
| E541 | a type variable named like a real type | type variable '{tv}' shadows a real type |
| E542 | an argument that does not fit the shape a generic function's type variables took | '{node.name}' argument {i} should look like {want}, but this is {got} |
| E543 | a generic function passed as a value | '{f2.name}' is generic - generic functions cannot be passed as values yet |
| E550 | amounts in two different currencies added, compared, or one given where the other is needed | |
| E551 | a currency that is not in velaris.CURRENCIES, or one not written as text in the call | the currency must be written in the call, as text |
| E552 | a rounding mode other than "half_up", "half_even" or "down", or one not written as text in the call | the rounding mode must be written in the call: |
| E553 | an amount divided with '/' or '%', which would round without saying how | '{op}' on an amount would round without saying how |
| E560 | a Secret given to something that emits it: a builtin with an effect, a generic function with an effect, or a 'fail' reason | {what} is {t}, and {where} - a Secret cannot be printed, written, sent or passed to Python. It came from {origin} |
| E561 | declassify without a reason written as text in the call, or given something that is not a Secret | the reason given to '{said}' must be written as text in the call |
| E562 | a Secret of a Secret | a Secret of a Secret is the same secret; write {inner} |
| E563 | an 'if' or 'while' branching on a value derived from a Secret | '{kind}' would branch on {t}, which came from {origin} - a program does not choose what to do by looking at a secret. A comparison over one gives a Secret of Bool exactly so that this is refused: in a loop it would read the secret out a character at a time |
| E600 | a 'requires' broke while running | broken promise: {nice_name(name)} requires {expr_str(expr)} ({vals(expr)}) |
| E601 | an 'ensures' broke while running | broken promise: {nice_name(name)} ensures {expr_str(expr)} ({vals(expr, (retval,))}) |
| E602 | a position outside a list or text while running | position {i} is outside the text (it has {len(t)} character(s)) |
| E607 | a text grew too large to build, or there was no input to read | this text grew too large to build |
| E608 | a file could not be written | could not write '{str(args[0]).replace(chr(0), chr(92) + '0')}': a path cannot hold a NUL character |
| E609 | recursion too deep, a value nested too deeply, or split by empty text | '{name}' called itself {DEPTH_LIMIT} deep - this looks like recursion that never stops |
| E610 | the run's time limit was reached and the program stopped | the program ran longer than {self.timeout} second(s) and was stopped |
| E611 | the run's memory cap was reached and the program stopped | the program used more than {self.max_memory_mb} MB and was stopped |
| E612 | a loop whose end cannot be shown (check --strict only) | |
| E613 | a check or audit ran past its time ceiling and was stopped | the {what} did not finish within {self.timeout:g} second(s) and was stopped; the source may be crafted to stall the checker |
| E614 | a check or audit grew past its memory ceiling and was stopped | the {what} used more than {self.max_memory_mb} MB and was stopped; the source may be crafted to bloat the checker |
| E700 | a promise that is provably false, with the input that breaks it | promise cannot be kept: {nice_name(fn.name)} ensures {expr_str(ens_expr)} - proven without running the program: {vals} gives result = {rv} |
| E701 | a call that can break the called function's 'requires', with the input that does | this call can break a promise: '{fnB.name}' requires {expr_str(r_expr)}, but '{ctx.caller}' can call it with {vals} - proven without running the program |
| E703 | a loop invariant the prover cannot show holds | cannot prove the loop keeps 'invariant {expr_str(inv_expr)}' {where} in '{ctx.caller}' - the promises allow: {vals} |
| E704 | a loop invariant broke while running | loop broke its promise: invariant {expr_str(inv_expr)} ({vals}) |
| E705 | a list read the prover shows can go past the end | this 'get' can reach position {m.eval(idx, model_completion=True)}, but the list has {m.eval(length, model_completion=True)} item(s) - proven without running the program |
| E706 | a divisor the prover shows can be zero | this can {word} zero |
| E999 | the self-test in 'velaris doctor' failed | self-test failed |
Findings that are not compile errors
What velaris check --sarif, proofs --sarif, audit --sarif and capabilities check --sarif report besides the codes above, at the level SARIF reports each at.
| Rule | Level | What it means |
|---|---|---|
| unproven-promise | warning | a requires or ensures that is checked while the program runs, not proven before it runs |
| contract-coverage | note | a function that takes or returns data and promises nothing about it |
| loop-not-shown-to-end | note | a loop the termination rule cannot show to end; check --strict refuses it as E612 |
| ffi-native | note | a granted Python module ships native code (a compiled extension: .so/.pyd/.dylib), found on disk without importing it; there is no source to read and a budget does not contain what it does |
| secret-source | note | a builtin that hands the program a Secret (env, read_file_secret); the compiler will not let its result be printed, written or sent |
| secret-declassified | warning | a declassify call turns a Secret into an ordinary value, with a stated reason; an error under check --strict unless the reason is listed in --allow-declassify-reasons |
| uses-io | note | a function that may perform io: the console |
| uses-env | note | a function that may perform env: environment variables |
| uses-fs | note | a function that may perform fs: files |
| uses-net | note | a function that may perform net: the network |
| uses-clock | note | a function that may perform clock: the time |
| uses-rand | note | a function that may perform rand: randomness |
| uses-ffi | note | a function that may perform ffi: Python, and so anything Python can do |
| uses-declassify | note | a function that may perform declassify: turning a Secret into an ordinary value, which anything may then emit |
| capability-widened | error | code that needs a grant velaris.capabilities does not give: an effect, a Python module, a path outside the recorded ones, a host, a scoped grant made unscoped, or more fs or net operations in a run than recorded (capabilities check) |
| capability-effect-gained | error | a function velaris.capabilities records now declares an effect it did not declare there (capabilities check) |
| capability-narrowed | note | velaris.capabilities gives more than the code needs now; capabilities init --force records the narrower surface |
| dependency-capability-widened | error | an upgraded Velaris dependency needs a grant its previous version did not: an effect, a Python module, a path, a host, or more fs or net operations in a run (deps-diff) |
| dependency-effect-gained | error | a function of an upgraded Velaris dependency declares an effect it did not declare in the previous version (deps-diff) |
| dependency-install-script | error | an upgraded dependency runs an install-time script its previous version did not, or a different one; what the script does is not derived (deps-diff) |
| dependency-surface-unknown | note | an upgraded dependency holds code other than Velaris, or could not be read, so what it can do was not derived; unknown is not safe (deps-diff) |
| dependency-added | note | a dependency the upgraded version declares that the previous one did not; its own surface was not examined (deps-diff) |
| dependency-narrowed | note | an upgraded Velaris dependency needs less than its previous version did (deps-diff) |
Removed codes
None. A code that stops being given is listed here, and is never given again for anything else (STABILITY.md).