Repository navigation
Verify semantic invariants at the raw UBCM boundary - #18
Draft
Papishushi wants to merge 1 commit into
Draft
Papishushi wants to merge 1 commit into
Papishushi wants to merge 1 commit into
Conversation
Up to standards ✅🟢 Issues
|
| Metric | Results |
|---|---|
| Complexity | 84 |
| Duplication | 7 |
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
changed the base branch from
feat/semantic-source-frontend-v0
to
main
October 14, 2026 17:03
Papishushi
force-pushed
the
feat/semantic-binary-verifier-v0
branch
2 times, most recently
from
October 15, 2026 01:56
d781cef to
eba12f9
Compare
Papishushi
changed the base branch from
main
to
feat/semantic-source-frontend-v0
October 15, 2026 12:22
Papishushi
added this pull request to stack #13
October 15, 2026 12:36
Papishushi
force-pushed
the
feat/semantic-binary-verifier-v0
branch
from
October 15, 2026 21:42
8bdce2a to
57dd1ee
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the next trust boundary in the portable pipeline, stacked on #17.
The source frontend is no longer trusted to be the only producer of executable UBCM.
PortableBinaryVerifiernow derives semantic safety directly from the indexed tables and raw code bytes, without callingFunctionStackValidator,PortableBinaryCodec.Decode, orIndexedExecutableFormat.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,ROLLand operand-free stack operationsLOADandSTOREFNADDRandCALLICALL, using the target Function table argument count and return typeCALL, including Value vs LoanRead/LoanWrite cell counts plusbudget_msandresult_addressRETURN, requiring a result cell for non-void functionsTRAPreachability andCLEARstack resetA reachable non-void fallthrough is rejected.
Frame and binding invariants
The verifier independently reconstructs binding properties from Function/Type tables and rejects:
STORE BindingIndextargetingReadOnlyorConstVARtargeting an argumentVARinitializationVARinitializationThis also prevents crafted
VARinstructions from becoming a back door around readonly enforcement.Independence
This is intentionally a second semantic implementation. It does not reuse
FunctionStackValidatoror sourceCompilationScopes; 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:
Consumeis now fail-fast and transactional: a scope/source mismatch throws immediately and never advances the caller cursorParseFunc,ParseAction,ParseClass,ParseStruct,ParseRecord,ParseInterface,ParseEnumorParseFieldTryConsumeDeclarationPrefixand typed-declaration probes leave the cursor untouched when a production does not applylocal/globalcontext blocks are distinguished fromlocal/globaldeclaration modifiers by the following block productionstruct,interfaceandenumdeclaration keywords consistently, recognizes nullable/array typed names, removes the catch-all argument classification, and resolves overlapping operators/punctuation longest-firstDedicated 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 { ... }versusglobal 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:
LOAD->STOREagainst a readonly bindingRETURNremoval / reachable fallthroughRETURNunderflowVARretargeting from a local binding to an argumentNext
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.