sorting specs TODO

docs/specs/bytecode/ISA_CORE.md

@@ -29,7 +29,7 @@ This document defines the minimal, stable Core ISA surface for the Prometeu Virt
 
 - Stack manipulation:
   - `PUSH_CONST u32` — load constant by index → _pushes `[value]`.
-  - `PUSH_I64 i64`, `PUSH_F64 f64`, `PUSH_BOOL u8`, `PUSH_I32 i32`, `PUSH_BOUNDED u32(<=0xFFFF)` — push literals.
+  - `PUSH_I64 i64`, `PUSH_F64 f64`, `PUSH_BOOL u8`, `PUSH_I32 i32` — push literals.
   - `POP` — pops 1.
   - `POP_N u32` — pops N.
   - `DUP` — `[x] -> [x, x]`.
@@ -38,8 +38,6 @@ This document defines the minimal, stable Core ISA surface for the Prometeu Virt
 - Arithmetic:
   - `ADD`, `SUB`, `MUL`, `DIV`, `MOD` — binary numeric ops.
   - `NEG` — unary numeric negation.
-  - `BOUND_TO_INT` — `[bounded] -> [int64]`.
-  - `INT_TO_BOUND_CHECKED` — `[int] -> [bounded]` (traps on overflow 0..65535).
 
 - Comparison and logic:
   - `EQ`, `NEQ`, `LT`, `LTE`, `GT`, `GTE` — comparisons → `[bool]`.

docs/specs/pbs/3. Core Syntax Specification.md

@@ -101,7 +101,6 @@ Numeric literals:
 
 - `IntLit`: decimal integer (`0`, `42`, `1000`)
 - `FloatLit`: decimal float with dot (`3.14`, `0.5`)
-- `BoundedLit`: decimal integer with `b` suffix (`0b`, `255b`)
 
 String literals:
 
@@ -256,6 +255,7 @@ Rules:
 - Struct methods have an implicit `this` receiver and do not declare `this: Self` explicitly.
 - `ctor` declares a named factory for the enclosing struct type.
 - A named `ctor` constructs its enclosing struct by initializing the fields of an implicit under-construction `this`.
+- Multiple `ctor` declarations with the same name are allowed only when their parameter signatures differ.
 - Struct values are constructed only through `new Type(...)`.
 - `declare contract` bodies contain only function signatures.
 - A contract declaration introduces a nominal runtime-dispatchable method surface.
@@ -351,15 +351,16 @@ Rules:
 
 - Top-level constants MUST use `declare const`.
 - `declare const` is a declaration and may be exported through `mod.barrel`.
+- A `declare const` initializer MUST be a constant expression as defined by static semantics.
+- `declare const` values are compile-time constants, not runtime-initialized module storage.
 
 ## 8. Type syntax
 
 ```ebnf
 TypeRef ::= OptionalType | TypePrimary
-TypePrimary ::= SelfType | SimpleType | GenericType | NamedTupleType | GroupType | UnitType
+TypePrimary ::= SelfType | SimpleType | NamedTupleType | GroupType | UnitType
 SelfType ::= 'Self'
 SimpleType ::= Identifier
-GenericType ::= Identifier '<' TypeRef (',' TypeRef)* '>'
 NamedTupleType ::= '(' NamedTupleField (',' NamedTupleField){0,5} ')'
 NamedTupleField ::= Identifier ':' TypeRef
 GroupType ::= '(' TypeRef ')'
@@ -372,6 +373,7 @@ Rules:
 - Named tuple arity is 1..6 in v1 core syntax.
 - Tuple types in PBS core are always named.
 - Single-slot tuple types are allowed only in type/signature surface, not as tuple literals.
+- General user-defined generics are not part of PBS core v1.
 - `optional T` is the canonical optional-type syntax in all type positions.
 - `optional void` and `optional ()` are invalid.
 - `Self` is valid only inside struct method and `ctor` declarations and refers to the enclosing struct type.
@@ -412,7 +414,7 @@ BreakStmt ::= 'break' ';'
 ContinueStmt ::= 'continue' ';'
 
 LValue ::= Identifier LValueSuffix*
-LValueSuffix ::= '.' Identifier | '[' Expr ']'
+LValueSuffix ::= '.' Identifier
 ```
 
 Rules:
@@ -428,6 +430,7 @@ Rules:
 - `for name: T from start until end step s { ... }` uses explicit step `s`.
 - `while` is the general-purpose loop form in v1 core.
 - `break` and `continue` are valid only inside loop contexts (`for`, `while`).
+- General indexing syntax (`expr[index]`) is not part of PBS core v1.
 - `LValue` MUST NOT include function call segments.
 - Compound assignment is syntax sugar over read/compute/write.
 
@@ -465,15 +468,14 @@ MulExpr ::= UnaryExpr (('*' | '/' | '%') UnaryExpr)*
 UnaryExpr ::= UnaryOp UnaryExpr | PostfixExpr
 UnaryOp ::= '!' | '-' | 'not'
 PostfixExpr ::= PrimaryExpr PostfixSuffix*
-PostfixSuffix ::= CallSugarSuffix | MemberSuffix | IndexSuffix | PropagateSuffix
+PostfixSuffix ::= CallSugarSuffix | MemberSuffix | PropagateSuffix
 CallSugarSuffix ::= '(' ArgList? ')'
 MemberSuffix ::= '.' Identifier
-IndexSuffix ::= '[' Expr ']'
 PropagateSuffix ::= '!'
 
 ArgList ::= Expr (',' Expr)*
 
-Literal ::= IntLit | FloatLit | BoundedLit | StringLit | BoolLit
+Literal ::= IntLit | FloatLit | StringLit | BoolLit
 BoolLit ::= 'true' | 'false'
 PrimaryExpr ::= Literal | Identifier | ThisExpr | NewExpr | BindExpr | SomeExpr | NoneExpr | UnitExpr | TupleExpr | GroupExpr | Block
 ThisExpr ::= 'this'
@@ -509,6 +511,7 @@ Rules:
 - `new Type.ctorName(args...)` is the canonical named-constructor surface.
 - Struct construction arguments are positional and follow the declared struct field order.
 - `as` is reserved in expressions for explicit contract-view conversion only; it does not denote a general cast surface in v1 core.
+- The right operand of expression-form `as` is a simple contract identifier already visible in scope, never a qualified module path.
 - `this` is an implicit receiver name available only inside struct method and `ctor` bodies.
 - `apply` is right-associative: `f1 apply f2 apply x` parses as `f1 apply (f2 apply x)`.
 - `f1 apply f2 apply f3 apply params` parses as `f1 apply (f2 apply (f3 apply params))`.
@@ -588,6 +591,7 @@ At minimum, deterministic diagnostics are required for:
 - invalid assignment targets (`LValue` violations),
 - top-level executable statements,
 - `const` used outside `declare const` or `let const`,
+- non-constant `declare const` initializer,
 - duplicate declaration names in the same namespace/scope (as defined by semantic phase),
 - use of reserved syntax words as active constructs.
 
@@ -616,6 +620,7 @@ Design goals:
 ### 13.2 Type Definition
 
 `optional` is a built-in prefix type constructor.
+It is a special core-language form, not evidence of general generic-type support in v1.
 
 Rules:
 
@@ -717,6 +722,7 @@ Design goals:
 
 `result<Error>` is not part of general `TypeRef`.
 It may appear only in a function return annotation.
+It is a special core-language return form, not evidence of general generic-type support in v1.
 
 Rules:
 
@@ -724,7 +730,7 @@ Rules:
 - The payload may be omitted; omitted payload is equivalent to `void`.
 - If present, the payload must be a valid return payload shape written after `result<E>`.
 - A single-slot payload is internally modeled as a one-field tuple payload.
-- `result<Error>` cannot be used for local variable annotations, parameter annotations, field types, or generic type arguments.
+- `result<Error>` cannot be used for local variable annotations, parameter annotations, or field types.
 - In function return surface, `result<Error>` is the only effect wrapper in use for that declaration.
 
 ### 14.3 Construction Surface
@@ -797,6 +803,19 @@ Rules:
 
 ## 15. Canonical examples
 
+This section is the canonical reference example set for PBS v1 syntax.
+
+It consolidates the primary surface forms used by tooling and conformance for:
+
+- `apply` and call sugar,
+- `bind` and nominal callbacks,
+- overloads that differ by return shape,
+- `optional`,
+- `result<Error>`,
+- `switch`.
+
+Examples in this section are intended to stay mutually consistent with the syntax and static-semantics documents.
+
 ### 15.1 Host function declaration
 
 ```pbs

docs/specs/pbs/4. Static Semantics Specification.md

@@ -135,8 +135,45 @@ Rules:
 - Any return surface that combines `optional` and `result` is statically invalid.
 - Any payload-less `optional` type surface is statically invalid.
 - Any `optional void` type surface is statically invalid.
+- A `declare const` declaration must include an explicit type annotation.
+- A `declare const` initializer must be a constant expression.
+- `declare const` dependency resolution is module-wide and must not depend on source-file processing order.
+- `declare const` dependencies must form an acyclic graph.
 
-### 3.4 Enum declarations and values
+### 3.4 Constant expressions
+
+PBS core v1 restricts top-level constant evaluation to a deterministic compile-time subset.
+
+Rules:
+
+- A `declare const` initializer is evaluated at compile time.
+- A `declare const` may depend only on previously resolved visible `declare const` declarations and enum case values.
+- Cross-file constant resolution within a module is defined by dependency analysis, not source-file order.
+- Constant evaluation fails if the dependency graph contains a cycle.
+- The allowed constant-expression forms in v1 core are:
+  - scalar literals: `IntLit`, `FloatLit`, `StringLit`, `BoolLit`,
+  - enum case paths `EnumName.caseName`,
+  - a reference to another visible `declare const`,
+  - unary `-` applied to an integer or float constant expression,
+  - unary `not` or `!` applied to a boolean constant expression,
+  - binary arithmetic operators over numeric constant expressions,
+  - binary comparison operators over compatible constant expressions,
+  - binary boolean operators over boolean constant expressions.
+- A `declare const` initializer must not use:
+  - callable application or call sugar,
+  - `host fn`,
+  - `new`,
+  - `bind(...)`,
+  - `some(...)` or `none`,
+  - tuple expressions,
+  - block expressions,
+  - `if`, `switch`, `handle`, `else` extraction, or `!` result propagation,
+  - method calls or member access except enum case paths.
+- The initializer type must be compatible with the declared `const` type.
+- A `pub const` may be imported from another module only through ordinary module import rules.
+- A `declare const` does not introduce mutable runtime storage; implementations may inline, fold, or materialize it as an immutable constant as long as observable semantics remain unchanged.
+
+### 3.5 Enum declarations and values
 
 Rules:
 
@@ -148,7 +185,7 @@ Rules:
 - The static type of `Name.case` is the enum type `Name`.
 - Error labels are not enum cases and must not be used where enum case values are required.
 
-### 3.5 Structs, methods, and contracts
+### 3.6 Structs, methods, and contracts
 
 Rules:
 
@@ -166,6 +203,7 @@ Rules:
 - A `ctor` has no declared return annotation and is not a `fn`.
 - A `ctor` completes by falling off the end of its body after initializing the enclosing struct instance.
 - Every field of the enclosing struct must be definitely assigned on every completing `ctor` path.
+- Named constructors participate in overload resolution by name plus parameter signature.
 - `return;` and `return expr;` are both invalid inside `ctor` bodies.
 - Methods declared in a struct body belong to the direct method namespace of that concrete struct type.
 - `receiver.method(...)` on a concrete struct receiver resolves only against methods declared directly in that struct body.
@@ -178,6 +216,7 @@ Rules:
 - A struct value may be coerced to a contract value when exactly one visible `implements Contract for Struct ...` applies.
 - Contract coercion may happen by explicit `expr as ContractType` or by contextual typing in assignments, parameter passing, and returns.
 - `as` in expression position is reserved for explicit contract coercion only; no other cast semantics exist in v1 core.
+- The contract name in `expr as ContractName` must be a simple visible identifier resolved through ordinary scope and import rules.
 - A contract value carries the underlying struct reference together with the selected contract implementation for runtime dispatch.
 - Calling `contractValue.method(...)` uses dynamic dispatch through the contract value.
 - Calling `structValue.contractMethod(...)` is not valid unless that method is also declared directly on the struct.
@@ -219,7 +258,7 @@ fn demo() -> int {
 }
 ```
 
-### 3.6 Nominal callbacks
+### 3.7 Nominal callbacks
 
 Rules:
 
@@ -246,7 +285,10 @@ declare callback TickCb(dt: int) -> void;
 fn on_tick(dt: int) -> void {
 }
 
-let cb: TickCb = on_tick;
+fn install_tick() -> void {
+  let cb: TickCb = on_tick;
+  let _ = cb;
+}
 ```
 
 Bound example:
@@ -259,7 +301,10 @@ declare struct Enemy(hp: int);
 fn update_enemy(self: Enemy, dt: int) -> void {
 }
 
-let cb: UpdateCb = bind(enemy, update_enemy);
+fn install_update(enemy: Enemy) -> void {
+  let cb: UpdateCb = bind(enemy, update_enemy);
+  let _ = cb;
+}
 ```
 
 Ambiguous overload example:
@@ -273,10 +318,12 @@ fn tick(dt: int) -> void {
 fn tick(time: int) -> void {
 }
 
-let cb: TickCb = tick; // error: ambiguous overloaded fn assignment
+fn install_tick() -> void {
+  let cb: TickCb = tick; // error: ambiguous overloaded fn assignment
+}
 ```
 
-### 3.7 Canonical application
+### 3.8 Canonical application
 
 The canonical surface form for function application is:
 
@@ -301,7 +348,7 @@ Rules:
 - Chained `apply` is nested ordinary application, not callable composition as a first-class value.
 - Callback values, `host fn`, service methods, struct methods, and contract-method targets use the same `apply` rules as top-level `fn`.
 
-### 3.8 Call sugar
+### 3.9 Call sugar
 
 The surface form:
 
@@ -321,7 +368,7 @@ Rules:
 - When `(arg1, ..., argN)` is used as positional tuple sugar, the callee input tuple shape supplies the effective labels.
 - All overload resolution, diagnostics, and type checking are defined on the canonical `apply` form.
 
-### 3.9 Result type of application
+### 3.10 Result type of application
 
 Rules:
 
@@ -339,10 +386,14 @@ fn func(a: int, b: int) -> (c: int, d: float) {
   return (c: a + b, d: 2.0);
 }
 
-let params: (a: int, b: int) = (1, 2);
-let r = func apply params;
-let c = r.c;
-let d = r.d;
+fn demo_apply() -> int {
+  let params: (a: int, b: int) = (1, 2);
+  let r = func apply params;
+  let c = r.c;
+  let d = r.d;
+  let _ = d;
+  return c;
+}
 ```
 
 In the example above:
@@ -360,8 +411,11 @@ fn plus_one(x: int) -> int {
   return x + 1;
 }
 
-let r = plus_one apply 1;
-if r == 2 { }
+fn demo_single() -> void {
+  let r = plus_one apply 1;
+  if r == 2 {
+  }
+}
 ```
 
 In the example above:
@@ -372,7 +426,7 @@ In the example above:
 - the value produced by `plus_one apply 1` has carrier type `int`,
 - `r.value` is not required and should not be used.
 
-### 3.10 Overload resolution
+### 3.11 Overload resolution
 
 Rules:
 
@@ -386,7 +440,7 @@ Rules:
 - Overloads that differ only by labels are duplicates and are forbidden.
 - Overloads that differ only by output positional types are permitted, but uncontextualized `apply` sites may become ambiguous.
 
-### 3.11 Member access and projection
+### 3.12 Member access and projection
 
 Rules:
 
@@ -413,7 +467,7 @@ Rules:
 - Access to a missing contract method is a compile-time error.
 - Member projection is not defined for single-slot collapsed carrier values.
 
-### 3.12 Block expressions and function fallthrough
+### 3.13 Block expressions and function fallthrough
 
 Rules:
 
@@ -426,7 +480,7 @@ Rules:
 - Reaching the end of an `optional P` function yields `none`.
 - Reaching the end of a `result<E>` function is a compile-time error.
 
-### 3.13 Loop forms
+### 3.14 Loop forms
 
 Rules:
 
@@ -442,7 +496,7 @@ Rules:
 - `continue` inside `for` transfers control to the step update and then to the next bound check.
 - `break` exits the nearest enclosing loop.
 
-### 3.14 `if` and `switch` conditional expressions
+### 3.15 `if` and `switch` conditional expressions
 
 Rules:
 
@@ -464,7 +518,7 @@ Rules:
 - A `switch` used as an `ExprStmt` is valid when the selected arm blocks evaluate to unit.
 - A `switch` expression used in a value-required position must be exhaustive, either by a wildcard arm or by another statically proven exhaustive case set.
 
-### 3.15 `optional` construction and extraction
+### 3.16 `optional` construction and extraction
 
 Rules:
 
@@ -476,7 +530,7 @@ Rules:
 - The static result type of `opt else fallback` is the carrier value type for single-slot payloads and the named tuple payload shape for multi-slot payloads.
 - `opt else fallback` does not introduce implicit mutation or unwrapping side effects beyond normal expression evaluation.
 
-### 3.16 `result<E>` return flow and handling
+### 3.17 `result<E>` return flow and handling
 
 Rules:
 
@@ -496,7 +550,7 @@ Rules:
 - The static result type of `handle expr { ... }` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot.
 - On error, `handle` performs an immediate enclosing-function return with the mapped `err(...)`.
 
-### 3.17 Required static diagnostics
+### 3.18 Required static diagnostics
 
 At minimum, deterministic static diagnostics are required for:
 
@@ -521,6 +575,8 @@ At minimum, deterministic static diagnostics are required for:
 - invalid enum case path,
 - invalid enum intrinsic member call,
 - invalid named constructor target,
+- unresolved named constructor overload,
+- ambiguous named constructor overload,
 - incompatible top-level `fn` assignment to callback type,
 - ambiguous overloaded top-level `fn` assignment to callback type,
 - attempted assignment of service method to callback type,
@@ -550,6 +606,11 @@ At minimum, deterministic static diagnostics are required for:
 - invalid mixed `optional`/`result` return surface,
 - invalid payload-less `optional` type surface,
 - invalid `optional void` type surface,
+- missing explicit type annotation on `declare const`,
+- non-constant `declare const` initializer,
+- incompatible `declare const` initializer type,
+- cyclic dependency among `declare const` declarations,
+- unresolved referenced `declare const` in constant evaluation,
 - invalid `none` usage without expected optional type,
 - invalid `else` extraction over non-optional operand,
 - fallback type mismatch in `else` extraction,

docs/specs/pbs/TODO.md

@@ -0,0 +1,47 @@
+# PBS Spec Approval TODO
+
+Status: Draft  
+Purpose: checklist curto para decidir se a spec da PBS pode ser aprovada para seguir agora
+
+## Blockers
+
+- [ ] Fechar o gate de prontidao para implementacao definido no charter.
+  Hoje o charter exige specs adicionais antes de iniciar implementacao: dynamic semantics, memory and lifetime, host ABI binding, module/package, diagnostics, IR/lowering e conformance.
+  Referencia: `1. Language Charter.md`, secao "Required Spec Set Before Implementation".
+
+- [ ] Definir a identidade normativa de `host fn`.
+  A governanca exige versionamento por `(module, name, version)`, mas a sintaxe e a semantica atual tratam `host fn` apenas por nome e assinatura.
+  Isso precisa de contrato claro de binding, capability gating e linking.
+  Referencias: `2. Governance and Versioning.md`, `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`.
+
+- [ ] Fechar o modelo semantico de `service` ou remover `service` do core v1.
+  A gramatica aceita `service Identifier (':' Identifier)?`, mas a spec nao define o significado do `: Identifier`, o ciclo de vida do servico, como ele e resolvido nem como participa do runtime.
+  Referencias: `3. Core Syntax Specification.md`, secao de `ServiceDecl`; `4. Static Semantics Specification.md`, callable categories.
+
+- [X] Remover do core v1 ou especificar completamente as superficies que ja existem na gramatica mas ainda nao tem contrato suficiente.
+  Itens visiveis hoje: `BoundedLit`, `GenericType`, `IndexSuffix` (`[]`) e `declare const` top-level.
+  Se permanecerem no v1, precisam de semantica estatica/dinamica e diagnosticos claros.
+  Referencia: `3. Core Syntax Specification.md`.
+
+## Non-Blockers
+
+- [x] Corrigir exemplos invalidos ou inconsistentes na spec estatica.
+  Ha exemplos com `let` em escopo top-level para callbacks, mas top-level `let` e proibido pela sintaxe.
+  Isso nao bloqueia a direcao da linguagem, mas deve ser corrigido para evitar ambiguidade.
+  Referencias: `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`.
+
+- [x] Consolidar exemplos canonicos para overload por retorno, `optional`, `result`, `bind`, `apply` e `switch`.
+  A base conceitual esta boa; o ajuste aqui e editorial e de conformance, nao arquitetural.
+
+- [ ] Decidir se a implementacao pode comecar em modo faseado.
+  Recomendacao: permitir apenas parser/AST/binding inicial enquanto os blockers acima nao forem fechados.
+  Nao liberar ainda lowering, linker, host integration ou runtime behavior final.
+
+## Decision Rule
+
+Pode aprovar a PBS para seguir agora somente se a aprovacao significar:
+
+- seguir com parser/frontend parcial, ou
+- seguir com fechamento das specs faltantes antes de runtime/lowering/linking.
+
+Nao aprovar como spec fechada para implementacao completa enquanto houver blockers abertos.