Skip to content

Verify semantic invariants at the raw UBCM boundary - #18

Draft
Papishushi wants to merge 1 commit into
feat/semantic-source-frontend-v0from
feat/semantic-binary-verifier-v0
Draft

Papishushi wants to merge 1 commit into
feat/semantic-source-frontend-v0from
feat/semantic-binary-verifier-v0

Conversation

@Papishushi

@Papishushi Papishushi commented Oct 14, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Closes the next trust boundary in the portable pipeline, stacked on #17.

source
  -> semantic frontend
  -> canonical UBCM
  -> independent semantic binary verifier
  -> typed decoder
  -> x64

The source frontend is no longer trusted to be the only producer of executable UBCM. PortableBinaryVerifier now derives semantic safety directly from the indexed tables and raw code bytes, without calling FunctionStackValidator, PortableBinaryCodec.Decode, or IndexedExecutableFormat.Verify.

Semantic stack verification

For every FunctionIndex, the raw verifier now tracks reachable evaluation-stack depth and enforces the portable v0 stack effects for:

  • PUSH, DROP, PICK, ROLL and operand-free stack operations
  • integer ALU, bitwise and comparison opcodes
  • named/raw LOAD and STORE
  • FNADDR and CALLI
  • local CALL, using the target Function table argument count and return type
  • import CALL, including Value vs LoanRead/LoanWrite cell counts plus budget_ms and result_address
  • the existing legacy four-UInt64 import ABI special case
  • RETURN, requiring a result cell for non-void functions
  • TRAP reachability and CLEAR stack reset

A reachable non-void fallthrough is rejected.

Frame and binding invariants

The verifier independently reconstructs binding properties from Function/Type tables and rejects:

  • function results outside the portable scalar-cell ABI
  • argument/local bindings outside the scalar-cell ABI
  • STORE BindingIndex targeting ReadOnly or Const
  • VAR targeting an argument
  • duplicate local VAR initialization
  • locals with no canonical VAR initialization

This also prevents crafted VAR instructions from becoming a back door around readonly enforcement.

Independence

This is intentionally a second semantic implementation. It does not reuse FunctionStackValidator or source CompilationScopes; all decisions come from canonical UBCM tables and bytes.

Frontend lexical/parser contract hardening

Strict verification exposed declaration-parser bugs that had previously been masked by permissive token consumption. This PR therefore also hardens the source frontend contract rather than suppressing those failures:

  • Consume is now fail-fast and transactional: a scope/source mismatch throws immediately and never advances the caller cursor
  • declaration dispatch consumes modifiers plus the declaration keyword before entering ParseFunc, ParseAction, ParseClass, ParseStruct, ParseRecord, ParseInterface, ParseEnum or ParseField
  • TryConsumeDeclarationPrefix and typed-declaration probes leave the cursor untouched when a production does not apply
  • local/global context blocks are distinguished from local/global declaration modifiers by the following block production
  • the bundled TextMate grammar now classifies struct, interface and enum declaration keywords consistently, recognizes nullable/array typed names, removes the catch-all argument classification, and resolves overlapping operators/punctuation longest-first
  • comments are treated as parser trivia and enum-member consumption no longer abuses the exact-source argument as a diagnostic label

Dedicated regressions cover declaration dispatch across scopes, modifier preservation, malformed declarations failing at the first required token, every supported nullable-array field-name shape, and global { ... } versus global func ....

Adversarial tests

Tests start from valid frontend-produced UBCM and then mutate the binary directly, proving that the raw verifier rejects malicious bytes after the frontend is completely out of the picture. Mutations cover:

  • ALU stack underflow
  • local-call arity underflow
  • import Value -> LoanRead mutation changing required cells
  • LOAD -> STORE against a readonly binding
  • non-void RETURN removal / reachable fallthrough
  • return-signature mutation causing RETURN underflow
  • function binding type mutation to a non-cell type
  • VAR retargeting from a local binding to an argument

Next

Once this is green, the next architectural PR is to make the portable x64 path the canonical/default CLI route and begin retiring direct source -> x64 as legacy compatibility.

@codacy-production

codacy-production Bot commented Oct 14, 2026 •

Copy link
Copy Markdown

Up to standards ✅

🟢 Issues 0 issues

Results:
0 new issues

View in Codacy

🟢 Metrics 84 complexity · 7 duplication

Metric Results
Complexity 84
Duplication 7

View in Codacy

NEW Get contextual insights on your PRs based on Codacy's metrics, along with PR and Jira context, without leaving GitHub. Enable AI reviewer
TIP This summary will be updated as you push new changes.

@Papishushi
Papishushi changed the base branch from feat/semantic-source-frontend-v0 to main October 14, 2026 17:03
Comment thread Ubytec/CommandLineDriver.cs Fixed
Comment thread Ubytec/CommandLineDriver.cs Fixed
@Papishushi
Papishushi force-pushed the feat/semantic-binary-verifier-v0 branch 2 times, most recently from d781cef to eba12f9 Compare October 15, 2026 01:56
@Papishushi
Papishushi changed the base branch from main to feat/semantic-source-frontend-v0 October 15, 2026 12:22
@Papishushi
Papishushi added this pull request to stack #13 October 15, 2026 12:36
@Papishushi Papishushi self-assigned this Oct 15, 2026
@Papishushi
Papishushi force-pushed the feat/semantic-binary-verifier-v0 branch from 8bdce2a to 57dd1ee Compare October 15, 2026 21:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants