# Define the MVP semantic core

Type: grilling
Status: resolved
Parent: [Find the ASPL MVP specification](../map.md)

## Question

What exact static types, expressions, variable and mutability rules, function semantics, control flow, string-literal behavior, source-file structure, and explicitly unsafe operations belong to the tiny MVP language core, and which acceptance programs prove that this core is internally coherent?

## Answer

The MVP semantic core is a small, statically typed language with checked integer arithmetic, deterministic evaluation, immutable-by-default lexical bindings, typed top-level functions, literal-only strings, and an operation-local unsafe boundary for C calls. This ticket fixes behavior, not source spelling, VM representation, or the C adapter catalog.

### Types and checking

- Storable values have exactly five types: `bool`, `i64`, `f64`, immutable UTF-8 `string`, and opaque nullable `c_ptr`.
- `unit` is a result type, not a storable value. A `unit` function may end naturally or use a bare `return`. A call returning `unit` is valid only as a statement. Programs cannot create, store, pass, or compare `unit` values.
- Exact C ABI types exist only in foreign declarations. The dynamic C interoperability decision must define their explicit boundary conversions without adding implicit conversions to ordinary ASPL code.
- Types never convert implicitly. Local inference selects the initializer's exact type. An explicit annotation must match after any written conversion, and a mutable local keeps one type for its lifetime.

### Programs and names

- A program is one source file containing ASPL function definitions and foreign declarations. File scope permits no variables or executable statements.
- Exactly one defined ASPL function is named `ابدأ_الرئيسية` or `start_main`. It takes no parameters, returns `i64`, cannot be foreign, and cannot be called by ASPL source.
- An entry-function result from 0 through 255 becomes the process status. Any other result traps instead of being truncated.
- ASPL functions, foreign declarations, and the release-fixed builtin catalog share one top-level callable namespace. Duplicate names and overloads are errors, and source cannot replace a builtin alias.
- A local or parameter cannot reuse any currently visible local, parameter, ASPL function, foreign name, or builtin alias. A local name may be reused after its previous scope ends.

### Bindings and scopes

- Function bodies and nested control-flow blocks introduce lexical scopes.
- Every local has an initializer. The declared name becomes visible only after the checker has checked that initializer.
- Bindings and parameters are immutable by default. A local declaration may explicitly opt into mutation; parameters cannot.
- Assignment is a statement that targets one mutable local. It evaluates the entire right side before changing the target and produces no value.
- The MVP has no globals and no shadowing of a visible name.

### Functions

- Functions appear only at file scope and require parameter and result types. There are no nested functions, closures, methods, default arguments, variadic ASPL functions, or function values.
- Source order does not affect resolution. Direct recursion, mutual recursion, and calls to later definitions are valid.
- ASPL and builtin calls pass arguments by value, require exact arity, and require exact argument types after explicit conversions. Foreign calls use their separately specified boundary conversions.
- Every reachable path through a non-`unit` function must return a value of its declared type. A structural `if` proves a return only when both branches return. A `while` never proves a containing function returns, even when its condition is a literal true value.
- The checker rejects code that the same structural analysis proves unreachable. It does not use constant folding or theorem proving for reachability.

### Expressions and statements

- Expressions are literals, local or parameter references, ASPL calls, safe builtin calls, explicitly unsafe foreign calls, explicit numeric conversions, grouping, and the specified unary and binary operations.
- Functions are not values. Assignment, conditionals, increments, decrements, and implicit calls are not expressions. There is no general cast expression beyond the specified conversions and later explicit C boundary conversions.
- Statements are initialized local declarations, assignment, calls, `if`, `while`, and `return`.
- A non-`unit` call may be used as a statement and discard its result. No other value-producing expression may stand alone as a statement.

### Numeric behavior

- Integer literals have type `i64`; floating literals have type `f64`. An out-of-range literal is a checking error.
- The source form `-9223372036854775808` is accepted as the minimum `i64` value even though its magnitude does not fit as a positive `i64` literal. Negating that value at runtime traps.
- `i64` supports unary negation, `+`, `-`, `*`, `/`, `%`, equality, and ordered comparisons. Integer overflow traps.
- Signed division truncates toward zero. Remainder has the dividend's sign or is zero, and satisfies `a matches (a / b) * b + (a % b)`.
- Integer division and remainder trap for a zero divisor and for `i64` minimum with `-1`.
- `f64` supports unary negation, `+`, `-`, `*`, `/`, equality, and ordered comparisons. It follows IEEE 754 binary64 behavior, including infinities, signed zero, and NaN.
- Explicit `i64` to `f64` conversion uses IEEE 754 rounding. Explicit `f64` to `i64` conversion truncates toward zero and traps for NaN, infinity, or an out-of-range result.
- Bitwise operations and shifts are not in the MVP.

### Booleans and equality

- Only `bool` is valid as an `if` or `while` condition. There are no truthiness conversions.
- Boolean `and` and `or` short-circuit. Boolean `not` is unary.
- Equality requires operands of the same type. Booleans and integers compare by value, floating equality follows IEEE 754 behavior, strings compare exact UTF-8 contents, and pointers compare identity including null. `unit` has no equality operation.

### Strings

- A string is an immutable UTF-8 value created only from a literal. String contents receive no runtime normalization.
- Strings may be stored, passed, returned, discarded, and compared. They may contain an embedded NUL.
- The core has no concatenation, indexing, slicing, interpolation, mutation, or runtime string construction. C-string conversion and lifetime rules belong to dynamic C interoperability.

### Pointers and unsafe operations

- `c_ptr` has a null literal. Ordinary code may store, pass, return, discard, and compare a pointer.
- Ordinary code cannot dereference a pointer, perform pointer arithmetic, inspect its address, or convert between pointers and integers or strings.
- Only an unsafe foreign call may introduce a non-null pointer from outside ASPL or send one back across the foreign boundary. ASPL functions may relay the opaque value without inspecting it.
- Every foreign declaration and every foreign call is explicitly unsafe at its own use site. The MVP has no general unsafe block.

### Control flow, evaluation, and traps

- `if` with an optional `else` and `while` are statements with lexical block bodies. `break` and `continue` are not in the MVP.
- `return` is the only early-exit statement.
- Operands, call arguments, and initializers evaluate left to right. Assignment evaluates its complete right side before changing the target. Boolean short-circuiting preserves this order.
- A runtime trap immediately and uncatchably terminates the whole ASPL program. Nothing after the failing operation runs. Later diagnostics and CLI decisions must assign messages and exit codes without changing which operations trap.

### Acceptance programs

The notation decision must render these as equivalent Arabic-keyword and English-keyword source fixtures. Each rejection and trap is a separate program so an earlier failure cannot hide another.

Programs that succeed:

- `sum_loop` uses a mutable local and `while` to sum 1 through 10, then returns 55.
- `recursive_factorial` computes factorial of 5 and returns 120.
- `mutual_recursion` defines even and odd checks in reverse dependency order and proves that mutual recursion resolves independently of source order.
- `short_circuit` places integer division by zero in Boolean branches that must not execute.
- `string_identity` passes and returns an Arabic string containing an embedded NUL, then compares it with the original.
- `float_round_trip` explicitly converts 42 from `i64` to `f64` and back.
- `unit_call` calls a `unit` helper as a statement.
- `builtin_output` calls the safe `(string) -> unit` output builtin as a statement and writes the exact literal bytes without an added newline.
- `null_round_trip` passes null through a `c_ptr` identity function and compares the result with null.
- `maximum_status` returns process status 255 successfully.

Programs rejected during checking cover each of these independently:

- Wrong-type arithmetic, comparison, condition, assignment, return, argument, or equality operands.
- An attempted implicit conversion or an out-of-range numeric literal.
- A local without an initializer, assignment to an immutable binding, or assignment of a different type.
- Shadowing of a local, parameter, ASPL function, foreign declaration, or builtin alias.
- A global binding or executable top-level statement.
- A duplicate or overloaded callable, missing or invalid entry function, or source call to the entry function.
- Wrong call arity, a missing return path, or structurally unreachable code.
- Any attempt to create, store, pass, or compare `unit`.
- Pointer arithmetic, dereference, address inspection, or pointer conversion.
- An unmarked foreign declaration or foreign call.
- Any excluded expression or statement form.

Programs that trap at runtime cover each of these independently:

- Checked integer overflow, including negation of `i64` minimum.
- Integer division or remainder by zero.
- `i64` minimum divided or remaindered by `-1`.
- NaN, infinity, and out-of-range `f64` to `i64` conversions.
- The entry function returning below 0 or above 255.

The runtime value model must preserve these semantics in bytecode execution. Dynamic C interoperability must add a concrete foreign-call fixture. Diagnostics, CLI, playground, and final conformance decisions must preserve the same checking and trap outcomes in every environment where the relevant operation is supported.