Add PySpec to StrataCore translation pipeline#422
Draft
joehendrix wants to merge 3 commits intomainfrom
Draft
Conversation
joehendrix
commented
Feb 13, 2026
joehendrix
force-pushed
the
jhx/pyspec_to_core
branch
9 times, most recently
from
f67ee6c to
45e183f
Compare
Translate PySpec signatures (Python type specifications) to StrataCore programs, enabling verification of Python APIs. Details: - ToCore.lean: translates function signatures, class definitions, and type aliases to Core procedures, opaque types, and type synonyms - PySpecM.lean: monad infrastructure for error-tracked translation - Handles primitive types, Optional unions (Union[None, T]), TypedDict, string literal enums, and generic containers (List, Dict, Any, bytes) - SourceRange.format: moved from Specs.lean for reuse across modules - Eliminated sorry in DDM.lean (args.attach.foldl with membership proof) - Removed debug #eval from CorePrelude.lean - Moved Core.getProgram from Verifier.lean to Translate.lean - Enabled #strata_gen Core in Parse.lean - Added pySpecToCore CLI command in StrataMain.lean Testing: - ToCoreTest.lean: end-to-end #guard_msgs tests covering all type mappings (primitives, complex types, literals, TypedDict, optional patterns, kwonly args), error messages for unsupported types, and class/type definition translation By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…module support Parse.lean is now a Lean 4 module with public imports and a public section for #strata_gen. The mkScopedIdent function in Gen.lean is updated to handle module files by using mkPrivateName for the pre-resolution hint when not in a public section. Removed duplicate scopedIdent/currScopedIdent/arrayLit definitions from Util/Lean.lean. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add support for Union[None, float], Union[None, Literal[int]], all-int-literal unions, and all-TypedDict unions. Eliminates 3,406 translation warnings across 409 AWS services (3,354 TypedDict dedup, 48 float, 4 int literal). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
joehendrix
force-pushed
the
jhx/pyspec_to_core
branch
from
45e183f to
23c50e9
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
1 participant
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
Union[None, T]→StrOrNone/IntOrNone/BoolOrNone), TypedDict →DictStrAny, class declarations → opaque types with method procedures, function signatures → abstract proceduresNew Files
Strata/Languages/Python/Specs/ToCore.lean— Main translation logicStrata/Languages/Python/Specs/PySpecM.lean— Monad infrastructure for error trackingTesting
StrataTest/Languages/Python/ToCoreTest.lean— End-to-end tests covering primitive types, complex types (Any, List, Dict, bytes), literal types, optional/union patterns, class and type definitions, keyword-only args, and error cases. All tests use#guard_msgsfor exact output matching.🤖 Generated with Claude Code
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.