Skip to content

hy-check(buildable): rust/sha3 pinned crate call-arity + spread rejection (Row 13 BUILDABLE) - #4355

Open
gorky117-cell wants to merge 2 commits into
limitlessprojects:mainfrom
gorky117-cell:fix/sha3-pinned-crate-call-arity-soundness
Open

gorky117-cell wants to merge 2 commits into
limitlessprojects:mainfrom
gorky117-cell:fix/sha3-pinned-crate-call-arity-soundness

Conversation

@gorky117-cell

Copy link
Copy Markdown
Contributor

Soundness & Specification Context (Row 13 BUILDABLE)

Under GUARANTEES.md Row 13 (BUILDABLE):

Any program accepted by hyb check with verdict Accept must compile cleanly under standard Go's toolchain (go build).

In compiler/crates/hy-check/src/buildable.rs, foreign calls to the M5/M6 curated pinned Rust crate rust/sha3 (sha3) completely bypassed call arity validation and spread argument constraints.

Calls with missing or extra arguments:

  • sha3.digest256() (expects 1 argument data, accepts 0 or 2+)
  • sha3.stream_checksum() (expects 2 arguments iters, seed, accepts 0, 1, or 3+)
    passed hyb check with zero diagnostics (Verdict::Accept), only to fail downstream at emission/compilation time with:
error [emit]: emitter (MVP-0): not yet supported: rust/sha3.digest256: missing arguments (params: data)
error [emit]: emitter (MVP-0): not yet supported: rust/sha3.digest256: too many arguments (descriptor has 1)
error [emit]: emitter (MVP-0): not yet supported: rust/sha3.stream_checksum: missing arguments (params: iters, seed)

Technical Solution

  1. Foreign Package Call Dispatch (buildable.rs line 8370):

    • Dispatched (pkg == "sha3" || pkg == "rust/sha3") && self.lookup_kind(pkg).is_none() to check_sha3_package_call.
    • Local shadowing is strictly preserved so user-declared identifiers named sha3 retain their local semantics.
    • Zero modifications to foreign.rs: strictly matches the Spec M6 pinned Rust surface.
  2. Exact Arity Enforcement:

    • sha3.digest256: exactly 1 argument (data).
    • sha3.stream_checksum: exactly 2 arguments (iters, seed).
    • Rejects underflow and overflow fail-closed with HYB-E1002, providing actionable error messages naming expected count and actual argument count.
    • Rejects variadic spread ... on non-variadic calls with HYB-E1002.
  3. Hermetic Regression Test Battery (tests/sha3_member_arity_buildable_soundness.rs):

    • 6 test functions verifying exact arity acceptance (both bare sha3 and rust/sha3 imports), arity underflow rejection, arity overflow rejection, spread rejection, local shadowing preservation, and actionable error messages.

Verification & Repository Hygiene

  • python tools/check_conflict_markers.py: none
  • python tools/check_test_registration.py: OK (40 test file(s), 36 discovery pattern(s))
  • python tools/check_guarantees.py: OK (table, registry, corpus and doc agree)
  • python tools/check_corpus_census.py: OK (all 7 corpus census surfaces agree)
  • Rebased directly on Session 183 upstream main (7cf29833), 0 behind, single atomic commit.

Bounty Settlement Coordinates

  • Contributor: @gorky117-cell / gauravatwork117 <gauravatwork117@gmail.com>
  • Settlement Rail: Requested PayPal (USD) via Discussion #295 (Comment #19441036)
  • Standby PayPal Address: kumarsinghgaurav@gmail.com

… (Row 13 BUILDABLE)

Both members of \
ust/sha3\ blessed in foreign.rs are now arity-checked at
hyb check time against the pinned Rust crate descriptors:
- \sha3.digest256(data)\: exactly 1 argument
- \sha3.stream_checksum(iters, seed)\: exactly 2 arguments
Invocations with missing or excessive arguments fail-closed with HYB-E1002
instead of escaping to emitter / build errors (Row 13 BUILDABLE). Spread calls
(\...\) on non-variadic members are strictly guarded from day one.
Dedicated regression test suite covers exact arity acceptance, underflow/overflow
rejection, spread rejection, local shadowing, and actionable error messages.

Signed-off-by: Gaurav Kumar Singh <gauravatwork117@gmail.com>
@github-actions github-actions Bot added the bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify()) label Nov 11, 2026
…into fix/sha3-pinned-crate-call-arity-soundness

Signed-off-by: gauravatwork117 <gauravatwork117@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify())

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants