feat(csharp): add C# language lifter with RPC protocol and menagerie signature#590
Merged
Conversation
|
Warning Rate limit exceeded
You’ve run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
WalkthroughThis PR implements a Roslyn-based C# lifter that emits JSON contracts, a JSON-IR→C# compiler, a JSON-RPC stdin/stdout server, xUnit tests and fixtures, project/manifest wiring, registers "csharp" in the CLI surfaces, and adds Menagerie C# language-signature specs. ChangesC# Lifter Implementation
C# Language Signature Specifications
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
✨ Finishing Touches🧪 Generate unit tests (beta)
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c979466f12
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| _ => "csharp:binop", | ||
| }; | ||
| var precond = DivByZeroPrecondition(op, rhs); | ||
| return Ctor(op, lhs, rhs, precond); |
There was a problem hiding this comment.
Every binary expression currently emits Ctor(op, lhs, rhs, precond), but the C# language-signature algorithms for ops like csharp:add, csharp:sub, csharp:eq, etc. are defined with arity 2, so this produces malformed IR for any binary expression and can break downstream mint/prove flows that expect signature-conformant terms.
Useful? React with 👍 / 👎.
Comment on lines
+119
to
+120
| foreach (var v in forStmt.Declaration?.Variables ?? new SeparatedSyntaxList<VariableDeclaratorSyntax>()) | ||
| { |
There was a problem hiding this comment.
for initializers
The for lifting path only reads forStmt.Declaration?.Variables, so common loops like for (i = 0; i < n; i++) lose their initializer entirely in lifted IR. This changes program semantics and yields incorrect contracts for a widely used loop form.
Useful? React with 👍 / 👎.
| ["formalSorts"] = JsonSerializer.SerializeToNode(formalSorts), | ||
| ["returnSort"] = PrimSort("Int"), | ||
| ["pre"] = TrueFormula(), | ||
| ["post"] = EqFormula(VarTerm("return_value"), stmtTerm), |
There was a problem hiding this comment.
The contract postcondition equates return_value with stmtTerm, but stmtTerm is produced by EmitStatement (e.g., csharp:return, csharp:seq) and represents statement structure rather than the method’s returned expression. This makes generated function-contract semantics invalid for normal methods and can invalidate downstream reasoning.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 15
🧹 Nitpick comments (14)
menagerie/csharp-language-signature/specs/op_bitxor.spec.json (1)
1-1: 💤 Low valueConsider formatting the JSON for readability.
Like
op_gt.spec.json, this spec would benefit from multi-line formatting for easier maintenance and review.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/op_bitxor.spec.json` at line 1, The JSON spec for the algorithm "csharp:bitxor" is currently single-line and hard to read; reformat menagerie/csharp-language-signature/specs/op_bitxor.spec.json into a multi-line, pretty-printed layout (like op_gt.spec.json) so each key (kind, fn_name, formals, formal_sorts, return_sort, pre, post, effects, locus) and nested objects/arrays are on their own lines for easier review and maintenance while preserving all field values (ensure "post" still contains the operation-contract with operator "bitxor" and wp "lhs ^ rhs (bitwise XOR)").menagerie/csharp-language-signature/specs/op_gt.spec.json (1)
1-1: 💤 Low valueConsider formatting the JSON for readability.
This spec is currently on a single line. Formatting it with indentation (like
op_seq.spec.json) would improve maintainability and diff clarity.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/op_gt.spec.json` at line 1, The JSON spec for the operation is all on one line which harms readability; open the op_gt.spec.json and pretty-print / reformat the JSON payload (the object with "kind":"algorithm", "fn_name":"csharp:gt", etc.) using standard indentation (like op_seq.spec.json) so keys like "formals", "formal_sorts", "post" and "effects" are each on their own lines and nested structures are indented for clarity; keep the same content and values (fn_name "csharp:gt", return_sort "Bool", post operator "gt") but change only whitespace/formatting.menagerie/csharp-language-signature/specs/op_index.spec.json (1)
1-1: 💤 Low valueConsider adding
arity_shapefor consistency.Similar to
op_lt.spec.json, this binary operator could benefit from anarity_shapefield to align with the pattern used inop_and.spec.jsonandop_sub.spec.json.📝 Proposed enhancement
-{"kind": "algorithm", "fn_name": "csharp:index", "formals": ["base", "index"], "formal_sorts": [{"kind": "ctor", "name": "Expr", "args": []}, {"kind": "ctor", "name": "Int", "args": []}], "return_sort": {"kind": "ctor", "name": "Expr", "args": []}, "pre": {"kind": "atomic", "name": "true", "args": []}, "post": {"kind": "operation-contract", "operator": "index", "arity": ["Expr", "Int"], "result": "Expr", "wp": "base[index]"}, "effects": {"effects": []}, "locus": "menagerie/csharp-language-signature/README.md"} +{"kind": "algorithm", "fn_name": "csharp:index", "formals": ["base", "index"], "formal_sorts": [{"kind": "ctor", "name": "Expr", "args": []}, {"kind": "ctor", "name": "Int", "args": []}], "return_sort": {"kind": "ctor", "name": "Expr", "args": []}, "pre": {"kind": "atomic", "name": "true", "args": []}, "post": {"kind": "operation-contract", "operator": "index", "arity": ["Expr", "Int"], "result": "Expr", "wp": "base[index]", "arity_shape": {"kind": "named", "slots": [{"name": "base"}, {"name": "index"}]}}, "effects": {"effects": []}, "locus": "menagerie/csharp-language-signature/README.md"}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/op_index.spec.json` at line 1, The spec for the algorithm "csharp:index" is missing an arity_shape field for the binary operator; add an "arity_shape" entry matching the pattern used by other binary operator specs (e.g., op_lt/op_and/op_sub) so the operator's arity is explicit—update the object describing the algorithm (fn_name "csharp:index") to include an arity_shape that corresponds to two arguments (Expr, Int) consistent with the other binary operator specs.menagerie/csharp-language-signature/specs/op_lt.spec.json (1)
1-1: 💤 Low valueConsider adding
arity_shapefor consistency.While the spec is functionally correct, some other binary operators in this signature (e.g.,
op_and.spec.json,op_sub.spec.json) include anarity_shapefield with named slots. Adding it here would improve consistency and documentation clarity.📝 Proposed enhancement
-{"kind": "algorithm", "fn_name": "csharp:lt", "formals": ["lhs", "rhs"], "formal_sorts": [{"kind": "ctor", "name": "Int", "args": []}, {"kind": "ctor", "name": "Int", "args": []}], "return_sort": {"kind": "ctor", "name": "Bool", "args": []}, "pre": {"kind": "atomic", "name": "true", "args": []}, "post": {"kind": "operation-contract", "operator": "lt", "arity": ["Int", "Int"], "result": "Bool", "wp": "lhs < rhs"}, "effects": {"effects": []}, "locus": "menagerie/csharp-language-signature/README.md"} +{"kind": "algorithm", "fn_name": "csharp:lt", "formals": ["lhs", "rhs"], "formal_sorts": [{"kind": "ctor", "name": "Int", "args": []}, {"kind": "ctor", "name": "Int", "args": []}], "return_sort": {"kind": "ctor", "name": "Bool", "args": []}, "pre": {"kind": "atomic", "name": "true", "args": []}, "post": {"kind": "operation-contract", "operator": "lt", "arity": ["Int", "Int"], "result": "Bool", "wp": "lhs < rhs", "arity_shape": {"kind": "named", "slots": [{"name": "lhs"}, {"name": "rhs"}]}}, "effects": {"effects": []}, "locus": "menagerie/csharp-language-signature/README.md"}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/op_lt.spec.json` at line 1, The JSON spec for the algorithm "csharp:lt" is missing an arity_shape field for the binary operator "lt"; add an "arity_shape" entry mirroring the formal parameter names (e.g., "arity_shape": ["lhs", "rhs"]) to the top-level object so it matches other binary operator specs (like op_and and op_sub) and improves documentation/consistency for the operator "lt".implementations/csharp/Provekit.Lift.Csharp/Program.cs (2)
15-16: ⚡ Quick winReplace
Environment.Exit(1)with proper async exit code handling.Calling
Environment.Exit(1)prevents graceful async cleanup. In asyncMainmethods, return the exit code fromInvokeAsyncinstead.♻️ Proposed refactor
rootCommand.SetHandler((bool rpc) => { if (rpc) { RpcServer.Run(); - return; } - Console.Error.WriteLine("usage: provekit-lift-csharp --rpc"); - Environment.Exit(1); + else + { + Console.Error.WriteLine("usage: provekit-lift-csharp --rpc"); + Environment.ExitCode = 1; + } }, rpcOption); -await rootCommand.InvokeAsync(args); +return await rootCommand.InvokeAsync(args);🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/Program.cs` around lines 15 - 16, The code currently calls Environment.Exit(1) which aborts async cleanup; instead modify the async Main/entry path to return and propagate an exit code from the invoked async routine (use the result of InvokeAsync or await the async handler) so the runtime can perform graceful async cleanup—locate the Program.Main/InvokeAsync call in Program.cs and replace the Environment.Exit(1) path with returning the integer exit code (or await InvokeAsync and return its int) and ensure any cleanup tasks are awaited before returning.
2-2: ⚡ Quick winRemove unused import.
The
System.Text.Jsonnamespace is imported but never used in this file.🧹 Proposed fix
using System.CommandLine; -using System.Text.Json; using Provekit.Lift.Csharp;🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/Program.cs` at line 2, Remove the unused using directive "using System.Text.Json;" from Program.cs to clean up imports; locate the top of the file where using directives are declared in the Program class and delete that specific line so the unused namespace is no longer imported.implementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.cs (1)
100-106: ⚡ Quick winAdd defensive structure validation before array indexing.
Line 104 indexes
post?["args"]?[1]without verifying the structure. If the contract format changes, this could fail with a confusing error.🛡️ Proposed improvement
var contract = result.Declarations[0]; var post = contract["post"]; +Assert.NotNull(post); +var args = post["args"]; +Assert.NotNull(args); +Assert.True(args.AsArray().Count >= 2, "Expected at least 2 args in post condition"); var compiler = new CsharpCompiler(); -var compiled = compiler.CompileBody(post?["args"]?[1]); +var compiled = compiler.CompileBody(args[1]); Assert.NotNull(compiled);🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.cs` around lines 100 - 106, The test indexes post?["args"]?[1] without validating structure; before calling CsharpCompiler.CompileBody, assert that result.Declarations has at least one item, that contract (result.Declarations[0]) contains a non-null "post" dictionary/object, that post contains an "args" array/list with Count/Length > 1, and then pass post["args"][1] to CompileBody; add clear Assert.NotNull/Assert.True checks (using variables result, contract, post, and the CsharpCompiler instance) so the failure message indicates which part of the structure was missing instead of throwing an indexing exception.menagerie/csharp-language-signature/specs/op_new.spec.json (1)
1-1: ⚡ Quick winConsider formatting JSON for readability.
The entire spec is on a single line, making it difficult to read, diff, and maintain. Multi-line JSON formatting would improve clarity.
📝 Proposed formatting
-{"kind": "algorithm", "fn_name": "csharp:new", "formals": ["type_name", "args"], "formal_sorts": [{"kind": "ctor", "name": "String", "args": []}, {"kind": "ctor", "name": "Expr", "args": []}], "return_sort": {"kind": "ctor", "name": "Expr", "args": []}, "pre": {"kind": "atomic", "name": "true", "args": []}, "post": {"kind": "operation-contract", "operator": "new", "arity": ["String"], "result": "Expr", "wp": "new object of type type_name constructed with args", "arity_shape": {"kind": "named", "slots": [{"name": "type_name"}, {"name": "args", "shape": {"kind": "set"}}]}}, "effects": {"effects": [{"kind": "effect-signature", "name": "Alloc"}]}, "locus": "menagerie/csharp-language-signature/README.md"} +{ + "kind": "algorithm", + "fn_name": "csharp:new", + "formals": ["type_name", "args"], + "formal_sorts": [ + {"kind": "ctor", "name": "String", "args": []}, + {"kind": "ctor", "name": "Expr", "args": []} + ], + "return_sort": {"kind": "ctor", "name": "Expr", "args": []}, + "pre": {"kind": "atomic", "name": "true", "args": []}, + "post": { + "kind": "operation-contract", + "operator": "new", + "arity": ["String"], + "result": "Expr", + "wp": "new object of type type_name constructed with args", + "arity_shape": { + "kind": "named", + "slots": [ + {"name": "type_name"}, + {"name": "args", "shape": {"kind": "set"}} + ] + } + }, + "effects": { + "effects": [{"kind": "effect-signature", "name": "Alloc"}] + }, + "locus": "menagerie/csharp-language-signature/README.md" +}🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/op_new.spec.json` at line 1, The JSON spec for the algorithm "csharp:new" is currently on one line; reformat it into pretty-printed, multi-line JSON to improve readability while preserving its exact content and semantics (keep keys like "fn_name", "formals", "formal_sorts", "return_sort", "pre", "post", "effects", "locus" and the "post" operation-contract details such as "operator":"new", "arity", "result", "wp", "arity_shape"). Ensure arrays (e.g. "formals", "formal_sorts", "effects") and nested objects are indented and placed on separate lines, validate the JSON after formatting, and do not change any string values or field names for the "csharp:new" spec.implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs (2)
381-385: 💤 Low valueTemporary variable generation may obscure expression semantics.
VarExprgenerates a fresh temporary variable for unhandled expressions. While this prevents crashes, it loses the connection between the temporary and the original expression, potentially making the contract less meaningful.Consider either handling more expression types explicitly or emitting a placeholder term that preserves structure (e.g.,
Ctor("csharp:unknown", StrConst(expr.ToString()))).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines 381 - 385, VarExpr currently returns a fresh temporary via VarTerm for any ExpressionSyntax, losing the original expression structure; update VarExpr to preserve semantics by either expanding handling for more ExpressionSyntax subclasses (e.g., LiteralExpressionSyntax, IdentifierNameSyntax, MemberAccessExpressionSyntax) and mapping them to meaningful terms, or emit a structured placeholder term instead of a blind temp (for example use a constructor-like term such as Ctor("csharp:unknown", StrConst(expr.ToString()))); ensure VarExpr still falls back to VarTerm only if no structured representation can be produced and keep references to VarExpr and VarTerm consistent.
85-85: 💤 Low valueConsider warning when local variable declarations lack initializers.
In valid C# code, local variables must be initialized before use, so
LocalDeclarationStatementSyntaxvariables should never haveInitializer == null. However, if the tool processes incomplete or malformed code, silently defaulting toIntConst(0)could mask issues. Consider emitting a warning or error when encountering such cases to improve robustness.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` at line 85, In ContractEmitter (around the local declaration handling where the code uses v.Initializer to build init: var init = v.Initializer is not null ? EmitExpression(v.Initializer.Value) : IntConst(0)), add a diagnostic/warning when v.Initializer is null instead of silently defaulting; emit a warning that the LocalDeclaration (VariableDeclaratorSyntax v / LocalDeclarationStatementSyntax) has no initializer, include the variable identifier (v.Identifier.Text) and source location if available, then keep the fallback to IntConst(0) to preserve current behavior so malformed/incomplete input is traceable without breaking emission.menagerie/csharp-language-signature/specs/eff_loop.spec.json (1)
1-1: 💤 Low valueConsider formatting for readability.
Like
eff_call.spec.json, this spec is minified. For consistency and maintainability, consider formatting with indentation to match the multi-line style of other specs.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/eff_loop.spec.json` at line 1, The JSON spec for the algorithm "csharp:effect:loop" is minified and should be pretty-printed for readability and consistency with other specs; reformat the contents of menagerie/csharp-language-signature/specs/eff_loop.spec.json into a multi-line, indented JSON layout (preserving keys like "kind", "fn_name": "csharp:effect:loop", "formals", "return_sort", "pre", "post", "effects", and "locus") so it matches the style used by eff_call.spec.json and other spec files.menagerie/csharp-language-signature/specs/eff_call.spec.json (1)
1-1: 💤 Low valueConsider formatting for readability.
The spec is valid but minified on a single line. For maintainability and easier review, consider formatting with indentation to match the style used in other spec files like
op_foreach.spec.json.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/csharp-language-signature/specs/eff_call.spec.json` at line 1, The spec file is minified and hard to read; reformat the JSON in menagerie/csharp-language-signature/specs/eff_call.spec.json by pretty-printing it (e.g., JSON.stringify(obj, null, 2)) so keys like "kind", "fn_name" (csharp:effect:call), "formals", "return_sort", "pre", "post" (operator: call-effect), and "effects" (name: Call) are each on their own indented lines matching the style of other spec files (like op_foreach.spec.json); ensure the file remains valid JSON and commit the formatted version.implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs (1)
107-123: 💤 Low valueIf statement always emits
elsebranch.Lines 107-123 always emit both
ifandelseblocks, even when the original code had noelse. While this preserves semantics (the else would contain a skip/empty statement), it adds visual clutter to the generated code.Consider checking if the else branch is empty/skip and omitting the
elseblock in that case:_indent--; _lines.Add($"{Indent()}}}"); if (!IsSkipStmt(args[2])) { _lines.Add($"{Indent()}else"); _lines.Add($"{Indent()}{{"); _indent++; EmitStmt(args[2]); _indent--; _lines.Add($"{Indent()}}}"); }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs` around lines 107 - 123, The EmitIf method currently always emits an else block even when the else branch is a no-op; modify EmitIf to detect an empty/skip else by calling IsSkipStmt on args[2] (after verifying args length) and only emit the "else" lines and the nested EmitStmt(args[2]) when IsSkipStmt(args[2]) is false; keep existing indentation handling (_indent, Indent()) and _lines.Add calls but wrap the else-block emission in that conditional so generated code omits empty else blocks.implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs (1)
48-51: ⚡ Quick winCache metadata references instead of rebuilding per file
References()is recomputed for every file, including a full TPA scan each time. Caching once per process should significantly reduce lift latency on larger inputs.Also applies to: 89-99
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs` around lines 48 - 51, Cache the result of the expensive References() call instead of recomputing it per file: add a process-wide static (or Lazy<ImmutableArray<MetadataReference>>) field on the CsharpLifter class, populate it once (thread-safely) by calling References() during initialization, and then replace all per-file calls to References() (the ones used when creating CSharpCompilation in the CsharpLifter logic, including the other occurrences around the block at lines ~89-99) with the cached field so each compilation reuses the same metadata reference set.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/csharp/.provekit/lift/csharp/manifest.toml`:
- Around line 4-5: The manifest's working_dir and command paths are inconsistent
causing dotnet to fail; update the manifest.toml so paths resolve from the
manifest location by either setting the working_dir key to
"implementations/csharp" or changing the command value to a path relative to the
manifest (e.g., adjust the "--project" argument to point to
../../Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj); modify the keys named
working_dir and command in
implementations/csharp/.provekit/lift/csharp/manifest.toml accordingly so dotnet
run can locate Provekit.Lift.Csharp.csproj.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs`:
- Line 35: The code in ContractEmitter.cs currently maps every parameter to
PrimSort("Int") via the formalSorts assignment, losing real C# types; replace
this by using the semantic model to derive each parameter's sort (e.g., call
_model.GetTypeInfo(p.Type).Type and map that to a sort via a helper like
GetSortFromType) so formalSorts reflects actual parameter types (handle
primitives like bool/string and reference/nullable types accordingly); update or
add a GetSortFromType method used by the parameters.Select(...) call and ensure
ContractEmitter uses it to build formalSorts instead of PrimSort("Int").
- Around line 180-181: The pattern in ContractEmitter that maps both null and
all unknown literals to IntConst(0) loses semantics; update the literal-to-term
mapping so the null case emits a distinct null term (e.g., emit NullConst() in
the null match arm of the method that handles literals in ContractEmitter) and
change the wildcard/default arm from IntConst(0) to either throw an exception or
log a warning and fail fast for unrecognized literal types; ensure you only use
IntConst(0) for actual integer literals and keep the change localized to the
literal mapping logic (the match expression handling literals in
ContractEmitter).
- Line 46: The return sort in ContractEmitter.cs is hardcoded to Int which
misrepresents actual method return types; update the ["returnSort"] assignment
in the contract emission for _method to derive the sort from the semantic model
by calling GetSortFromType on the declared symbol's ReturnType (use
_model.GetDeclaredSymbol(_method)?.ReturnType) so that boolean, string, void and
reference types are emitted correctly; ensure null-checking of the symbol and
that GetSortFromType handles void and nullable/reference cases, replacing the
literal PrimSort("Int") with the computed sort.
- Around line 278-283: The current assignment handling in the method returns
only rhs when assign.Left is not an IdentifierNameSyntax, which drops
assignments to complex lvalues; update the branch that handles assign.Left so it
recognizes and emits assignments for MemberAccessExpressionSyntax (obj.field),
ElementAccessExpressionSyntax (arr[index]), and other complex lvalues by
constructing an appropriate csharp:assign term via Ctor("csharp:assign",
<target-term>, rhs) and calling AddEffect("write", <target-name-or-path>); add a
small helper (e.g., ExtractWriteTarget or GetWriteTarget) that takes the
left-hand SyntaxNode and returns both a term usable by Ctor (similar to VarTerm
for identifiers) and a string/representation for AddEffect, then use that helper
in place of the IdentifierNameSyntax-only logic so all written targets are
tracked and assignments are emitted.
- Line 387: DivByZeroPrecondition currently returns a constant zero stub;
replace it with logic that, for division or modulo operators (e.g., "/" and
"%"), returns a JsonObject representing the precondition "rhs != 0" built using
the existing IntConst(0) and the library's binary-inequality expression
constructor; keep returning a neutral/no-op precondition for non-divide
operators. Update the DivByZeroPrecondition method so it checks the op string
and constructs the inequality JsonObject (rhs != IntConst(0)) using the same
expression-building helpers used elsewhere in ContractEmitter (e.g., the
binary-expression/inequality helper used by the binary-expression emission code
that calls DivByZeroPrecondition).
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs`:
- Around line 350-355: WrapFunction currently hardcodes the signature to "static
int F(int x0, int x1)" which breaks round-trip for methods with different
parameter counts/types and return types; modify WrapFunction to accept the IR
metadata (formals, formalSorts, returnSort) and use that to generate the
function signature (parameter types and names from formals/formalSorts and
return type from returnSort) instead of the two-int assumption, and ensure the
generated parameter list uses the actual names and types and the method return
type reflects returnSort so the lifted body compiles against the original
signature.
- Line 182: The emission currently hardcodes variable declarations as "int
{name} = {expr}" in CsharpCompiler (the _lines.Add call emitting declarations),
which prevents preserving original types; change the emitter to read the
variable term's sort/type annotation from the IR node (the variable declaration
site) and map that sort to a C# type name (e.g., via a new helper like
MapSortToCSharpType or GetCSharpTypeName) and use that type instead of "int"
when building the declaration string; ensure the emitter handles primitive sorts
(Int, Bool, String) and reference types consistently and falls back to a safe
default (e.g., object) if the sort is missing.
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs`:
- Around line 17-21: The code in CsharpLifter.cs currently calls
Directory.GetFiles(fullPath, "*.cs", SearchOption.AllDirectories) which can
throw and abort processing; change to a fault-tolerant enumeration that catches
exceptions per-directory so one bad folder doesn't stop the whole run. Replace
the single GetFiles call with a safe walker that processes files in fullPath,
then recursively EnumerateDirectories(fullPath) and for each child directory
call the same processing inside a try/catch (or catch exceptions around each
Directory.EnumerateFiles/EnumerateDirectories call), log or collect the error,
and continue calling LiftFile(file, result) for any discovered .cs files; keep
the existing LiftFile and result usage unchanged.
- Around line 16-25: The code in CsharpLifter.cs resolves source paths with
Path.GetFullPath(Path.Combine(workspaceRoot, sourcePath)) but does not verify
the resulting fullPath is contained within workspaceRoot, allowing traversal
outside the workspace; update the logic in the method that iterates source paths
(the block that calls LiftFile) to compute normalizedFullWorkspace =
Path.GetFullPath(workspaceRoot) and normalizedFullPath =
Path.GetFullPath(Path.Combine(workspaceRoot, sourcePath)) and then ensure
normalizedFullPath starts with normalizedFullWorkspace (use a
directory-separator-aware comparison, e.g., Path.GetRelativePath or string
prefix check with Path.DirectorySeparatorChar and OrdinalIgnoreCase) before
calling Directory.GetFiles or LiftFile; if the check fails, skip the path or
log/throw an error to prevent accessing files outside the workspace.
In `@implementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj`:
- Around line 16-17: Update the PackageReference entries in the csproj for
Microsoft.CodeAnalysis.CSharp and System.CommandLine: bump
Microsoft.CodeAnalysis.CSharp to a stable release that explicitly supports
net10.0 (replace the current 4.13.0 with the latest stable net10-compatible
version) and replace System.CommandLine 2.0.0-beta4.22272.1 with a stable 2.0.x
release (e.g., 2.0.6 or 2.0.7). After updating the PackageReference versions in
Provekit.Lift.Csharp.csproj, run dotnet restore and build to verify
compatibility and fix any API changes reported by the compiler (check usages in
code that reference Roslyn APIs or System.CommandLine parsing/handler types).
In `@implementations/csharp/Provekit.Lift.Csharp/RpcServer.cs`:
- Around line 50-56: The code currently calls GetValue<string>() and uses casts
like request["params"] as JsonObject/AsArray() that can throw on malformed but
parseable JSON and crash the server; update the parsing to safely extract and
validate types (e.g. use pattern matching or JsonValue.TryGetValue<string>(out
var method) for request["method"], check request["params"] is JsonObject or
JsonArray before casting, or wrap conversions in small try/catch that converts
failures to a safe default) and then route to Initialize(id), LiftRpc(id, ...),
CompileRpc(id, ...) only with validated values; apply the same defensive parsing
to the other request-handling sites (around the blocks at the other call sites
mentioned) so malformed payloads do not escape the Run loop.
In `@menagerie/csharp-language-signature/specs/op_call.spec.json`:
- Around line 4-18: The operation-contract for the call in the post field
currently lists arity: ["String"] which drops the second formal (args) and makes
the contract unsound; update the operation-contract's "arity" to include both
formal sorts in the same order as "formals" (e.g., ["String","Expr"]) so the
call operator's arity matches "formals" and the "arity_shape" (callee then args
as a set) for the "operator": "call" entry.
In `@menagerie/csharp-language-signature/specs/op_le.spec.json`:
- Line 1: The weakest-precondition string for the algorithm "csharp:le" is
incorrect: the "wp" field currently reads "lhs <= le" but should reference the
second formal parameter; update the "wp" value to "lhs <= rhs" in the JSON for
the csharp:le entry so it matches the formals (lhs, rhs) and the operator "le".
In `@menagerie/csharp-language-signature/specs/op_postinc.spec.json`:
- Line 1: The spec for the csharp:postinc algorithm (operator "postinc",
function "csharp:postinc") is missing a write effect: since the operation
performs target++ (read then increment) you need to add a write effect for the
target in the "effects" array so the contract reflects mutation; update the
"effects" field to include an appropriate write/mutable effect entry referring
to the target (e.g., a write effect on the Int-typed "target") and keep the rest
of the postcondition and wp intact.
---
Nitpick comments:
In `@implementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.cs`:
- Around line 100-106: The test indexes post?["args"]?[1] without validating
structure; before calling CsharpCompiler.CompileBody, assert that
result.Declarations has at least one item, that contract
(result.Declarations[0]) contains a non-null "post" dictionary/object, that post
contains an "args" array/list with Count/Length > 1, and then pass
post["args"][1] to CompileBody; add clear Assert.NotNull/Assert.True checks
(using variables result, contract, post, and the CsharpCompiler instance) so the
failure message indicates which part of the structure was missing instead of
throwing an indexing exception.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs`:
- Around line 381-385: VarExpr currently returns a fresh temporary via VarTerm
for any ExpressionSyntax, losing the original expression structure; update
VarExpr to preserve semantics by either expanding handling for more
ExpressionSyntax subclasses (e.g., LiteralExpressionSyntax,
IdentifierNameSyntax, MemberAccessExpressionSyntax) and mapping them to
meaningful terms, or emit a structured placeholder term instead of a blind temp
(for example use a constructor-like term such as Ctor("csharp:unknown",
StrConst(expr.ToString()))); ensure VarExpr still falls back to VarTerm only if
no structured representation can be produced and keep references to VarExpr and
VarTerm consistent.
- Line 85: In ContractEmitter (around the local declaration handling where the
code uses v.Initializer to build init: var init = v.Initializer is not null ?
EmitExpression(v.Initializer.Value) : IntConst(0)), add a diagnostic/warning
when v.Initializer is null instead of silently defaulting; emit a warning that
the LocalDeclaration (VariableDeclaratorSyntax v /
LocalDeclarationStatementSyntax) has no initializer, include the variable
identifier (v.Identifier.Text) and source location if available, then keep the
fallback to IntConst(0) to preserve current behavior so malformed/incomplete
input is traceable without breaking emission.
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs`:
- Around line 107-123: The EmitIf method currently always emits an else block
even when the else branch is a no-op; modify EmitIf to detect an empty/skip else
by calling IsSkipStmt on args[2] (after verifying args length) and only emit the
"else" lines and the nested EmitStmt(args[2]) when IsSkipStmt(args[2]) is false;
keep existing indentation handling (_indent, Indent()) and _lines.Add calls but
wrap the else-block emission in that conditional so generated code omits empty
else blocks.
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs`:
- Around line 48-51: Cache the result of the expensive References() call instead
of recomputing it per file: add a process-wide static (or
Lazy<ImmutableArray<MetadataReference>>) field on the CsharpLifter class,
populate it once (thread-safely) by calling References() during initialization,
and then replace all per-file calls to References() (the ones used when creating
CSharpCompilation in the CsharpLifter logic, including the other occurrences
around the block at lines ~89-99) with the cached field so each compilation
reuses the same metadata reference set.
In `@implementations/csharp/Provekit.Lift.Csharp/Program.cs`:
- Around line 15-16: The code currently calls Environment.Exit(1) which aborts
async cleanup; instead modify the async Main/entry path to return and propagate
an exit code from the invoked async routine (use the result of InvokeAsync or
await the async handler) so the runtime can perform graceful async
cleanup—locate the Program.Main/InvokeAsync call in Program.cs and replace the
Environment.Exit(1) path with returning the integer exit code (or await
InvokeAsync and return its int) and ensure any cleanup tasks are awaited before
returning.
- Line 2: Remove the unused using directive "using System.Text.Json;" from
Program.cs to clean up imports; locate the top of the file where using
directives are declared in the Program class and delete that specific line so
the unused namespace is no longer imported.
In `@menagerie/csharp-language-signature/specs/eff_call.spec.json`:
- Line 1: The spec file is minified and hard to read; reformat the JSON in
menagerie/csharp-language-signature/specs/eff_call.spec.json by pretty-printing
it (e.g., JSON.stringify(obj, null, 2)) so keys like "kind", "fn_name"
(csharp:effect:call), "formals", "return_sort", "pre", "post" (operator:
call-effect), and "effects" (name: Call) are each on their own indented lines
matching the style of other spec files (like op_foreach.spec.json); ensure the
file remains valid JSON and commit the formatted version.
In `@menagerie/csharp-language-signature/specs/eff_loop.spec.json`:
- Line 1: The JSON spec for the algorithm "csharp:effect:loop" is minified and
should be pretty-printed for readability and consistency with other specs;
reformat the contents of
menagerie/csharp-language-signature/specs/eff_loop.spec.json into a multi-line,
indented JSON layout (preserving keys like "kind", "fn_name":
"csharp:effect:loop", "formals", "return_sort", "pre", "post", "effects", and
"locus") so it matches the style used by eff_call.spec.json and other spec
files.
In `@menagerie/csharp-language-signature/specs/op_bitxor.spec.json`:
- Line 1: The JSON spec for the algorithm "csharp:bitxor" is currently
single-line and hard to read; reformat
menagerie/csharp-language-signature/specs/op_bitxor.spec.json into a multi-line,
pretty-printed layout (like op_gt.spec.json) so each key (kind, fn_name,
formals, formal_sorts, return_sort, pre, post, effects, locus) and nested
objects/arrays are on their own lines for easier review and maintenance while
preserving all field values (ensure "post" still contains the operation-contract
with operator "bitxor" and wp "lhs ^ rhs (bitwise XOR)").
In `@menagerie/csharp-language-signature/specs/op_gt.spec.json`:
- Line 1: The JSON spec for the operation is all on one line which harms
readability; open the op_gt.spec.json and pretty-print / reformat the JSON
payload (the object with "kind":"algorithm", "fn_name":"csharp:gt", etc.) using
standard indentation (like op_seq.spec.json) so keys like "formals",
"formal_sorts", "post" and "effects" are each on their own lines and nested
structures are indented for clarity; keep the same content and values (fn_name
"csharp:gt", return_sort "Bool", post operator "gt") but change only
whitespace/formatting.
In `@menagerie/csharp-language-signature/specs/op_index.spec.json`:
- Line 1: The spec for the algorithm "csharp:index" is missing an arity_shape
field for the binary operator; add an "arity_shape" entry matching the pattern
used by other binary operator specs (e.g., op_lt/op_and/op_sub) so the
operator's arity is explicit—update the object describing the algorithm (fn_name
"csharp:index") to include an arity_shape that corresponds to two arguments
(Expr, Int) consistent with the other binary operator specs.
In `@menagerie/csharp-language-signature/specs/op_lt.spec.json`:
- Line 1: The JSON spec for the algorithm "csharp:lt" is missing an arity_shape
field for the binary operator "lt"; add an "arity_shape" entry mirroring the
formal parameter names (e.g., "arity_shape": ["lhs", "rhs"]) to the top-level
object so it matches other binary operator specs (like op_and and op_sub) and
improves documentation/consistency for the operator "lt".
In `@menagerie/csharp-language-signature/specs/op_new.spec.json`:
- Line 1: The JSON spec for the algorithm "csharp:new" is currently on one line;
reformat it into pretty-printed, multi-line JSON to improve readability while
preserving its exact content and semantics (keep keys like "fn_name", "formals",
"formal_sorts", "return_sort", "pre", "post", "effects", "locus" and the "post"
operation-contract details such as "operator":"new", "arity", "result", "wp",
"arity_shape"). Ensure arrays (e.g. "formals", "formal_sorts", "effects") and
nested objects are indented and placed on separate lines, validate the JSON
after formatting, and do not change any string values or field names for the
"csharp:new" spec.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 3a0c2195-09b8-4493-a7df-f82dea531b34
📒 Files selected for processing (74)
implementations/csharp/.provekit/lift/csharp/manifest.tomlimplementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.csimplementations/csharp/Provekit.Lift.Csharp.Tests/Provekit.Lift.Csharp.Tests.csprojimplementations/csharp/Provekit.Lift.Csharp.Tests/fixtures/sample.csimplementations/csharp/Provekit.Lift.Csharp/ContractEmitter.csimplementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.csimplementations/csharp/Provekit.Lift.Csharp/CsharpLifter.csimplementations/csharp/Provekit.Lift.Csharp/Program.csimplementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csprojimplementations/csharp/Provekit.Lift.Csharp/RpcServer.csimplementations/csharp/Provekit.slnimplementations/rust/provekit-cli/src/project_config.rsmenagerie/csharp-language-signature/specs/eff_alloc.spec.jsonmenagerie/csharp-language-signature/specs/eff_call.spec.jsonmenagerie/csharp-language-signature/specs/eff_loop.spec.jsonmenagerie/csharp-language-signature/specs/eff_read.spec.jsonmenagerie/csharp-language-signature/specs/eff_write.spec.jsonmenagerie/csharp-language-signature/specs/effsig_alloc.spec.jsonmenagerie/csharp-language-signature/specs/effsig_call.spec.jsonmenagerie/csharp-language-signature/specs/effsig_loop.spec.jsonmenagerie/csharp-language-signature/specs/effsig_read.spec.jsonmenagerie/csharp-language-signature/specs/effsig_write.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_assoc.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_skip_left.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_skip_right.spec.jsonmenagerie/csharp-language-signature/specs/language_signature_csharp.spec.jsonmenagerie/csharp-language-signature/specs/op_add.spec.jsonmenagerie/csharp-language-signature/specs/op_and.spec.jsonmenagerie/csharp-language-signature/specs/op_assign.spec.jsonmenagerie/csharp-language-signature/specs/op_bitand.spec.jsonmenagerie/csharp-language-signature/specs/op_bitnot.spec.jsonmenagerie/csharp-language-signature/specs/op_bitor.spec.jsonmenagerie/csharp-language-signature/specs/op_bitxor.spec.jsonmenagerie/csharp-language-signature/specs/op_break.spec.jsonmenagerie/csharp-language-signature/specs/op_call.spec.jsonmenagerie/csharp-language-signature/specs/op_cast.spec.jsonmenagerie/csharp-language-signature/specs/op_continue.spec.jsonmenagerie/csharp-language-signature/specs/op_decl.spec.jsonmenagerie/csharp-language-signature/specs/op_div.spec.jsonmenagerie/csharp-language-signature/specs/op_eq.spec.jsonmenagerie/csharp-language-signature/specs/op_for.spec.jsonmenagerie/csharp-language-signature/specs/op_foreach.spec.jsonmenagerie/csharp-language-signature/specs/op_ge.spec.jsonmenagerie/csharp-language-signature/specs/op_gt.spec.jsonmenagerie/csharp-language-signature/specs/op_if.spec.jsonmenagerie/csharp-language-signature/specs/op_index.spec.jsonmenagerie/csharp-language-signature/specs/op_ite.spec.jsonmenagerie/csharp-language-signature/specs/op_le.spec.jsonmenagerie/csharp-language-signature/specs/op_lt.spec.jsonmenagerie/csharp-language-signature/specs/op_member.spec.jsonmenagerie/csharp-language-signature/specs/op_mod.spec.jsonmenagerie/csharp-language-signature/specs/op_mul.spec.jsonmenagerie/csharp-language-signature/specs/op_ne.spec.jsonmenagerie/csharp-language-signature/specs/op_neg.spec.jsonmenagerie/csharp-language-signature/specs/op_new.spec.jsonmenagerie/csharp-language-signature/specs/op_not.spec.jsonmenagerie/csharp-language-signature/specs/op_or.spec.jsonmenagerie/csharp-language-signature/specs/op_postdec.spec.jsonmenagerie/csharp-language-signature/specs/op_postinc.spec.jsonmenagerie/csharp-language-signature/specs/op_predec.spec.jsonmenagerie/csharp-language-signature/specs/op_preinc.spec.jsonmenagerie/csharp-language-signature/specs/op_return.spec.jsonmenagerie/csharp-language-signature/specs/op_seq.spec.jsonmenagerie/csharp-language-signature/specs/op_shl.spec.jsonmenagerie/csharp-language-signature/specs/op_shr.spec.jsonmenagerie/csharp-language-signature/specs/op_skip.spec.jsonmenagerie/csharp-language-signature/specs/op_sub.spec.jsonmenagerie/csharp-language-signature/specs/op_while.spec.jsonmenagerie/csharp-language-signature/specs/sort_bool.spec.jsonmenagerie/csharp-language-signature/specs/sort_expr.spec.jsonmenagerie/csharp-language-signature/specs/sort_int.spec.jsonmenagerie/csharp-language-signature/specs/sort_stmt.spec.jsonmenagerie/csharp-language-signature/specs/sort_string.spec.jsonmenagerie/csharp-language-signature/specs/sort_unit.spec.json
|
|
||
| var parameters = _method.ParameterList.Parameters; | ||
| var formals = parameters.Select(p => p.Identifier.Text).ToList(); | ||
| var formalSorts = parameters.Select(_ => PrimSort("Int")).ToList(); |
There was a problem hiding this comment.
All parameter types hardcoded to Int sort.
Line 35 maps every parameter to PrimSort("Int") regardless of the actual C# parameter type. This loses type information for bool, string, reference types, etc., and may cause semantic mismatches when the contract is used for verification.
Consider extracting the actual parameter type from the semantic model:
var formalSorts = parameters.Select(p =>
GetSortFromType(_model.GetTypeInfo(p.Type).Type)).ToList();🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` at line 35,
The code in ContractEmitter.cs currently maps every parameter to PrimSort("Int")
via the formalSorts assignment, losing real C# types; replace this by using the
semantic model to derive each parameter's sort (e.g., call
_model.GetTypeInfo(p.Type).Type and map that to a sort via a helper like
GetSortFromType) so formalSorts reflects actual parameter types (handle
primitives like bool/string and reference/nullable types accordingly); update or
add a GetSortFromType method used by the parameters.Select(...) call and ensure
ContractEmitter uses it to build formalSorts instead of PrimSort("Int").
| ["fnName"] = _method.Identifier.Text, | ||
| ["formals"] = JsonSerializer.SerializeToNode(formals), | ||
| ["formalSorts"] = JsonSerializer.SerializeToNode(formalSorts), | ||
| ["returnSort"] = PrimSort("Int"), |
There was a problem hiding this comment.
Return type hardcoded to Int sort.
Similar to parameter types, the return sort is hardcoded to Int. Methods returning bool, string, void, or reference types will have incorrect contract signatures.
Consider using the semantic model to extract the actual return type:
["returnSort"] = GetSortFromType(_model.GetDeclaredSymbol(_method)?.ReturnType)🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` at line 46,
The return sort in ContractEmitter.cs is hardcoded to Int which misrepresents
actual method return types; update the ["returnSort"] assignment in the contract
emission for _method to derive the sort from the semantic model by calling
GetSortFromType on the declared symbol's ReturnType (use
_model.GetDeclaredSymbol(_method)?.ReturnType) so that boolean, string, void and
reference types are emitted correctly; ensure null-checking of the symbol and
that GetSortFromType handles void and nullable/reference cases, replacing the
literal PrimSort("Int") with the computed sort.
Comment on lines
+180
to
+181
| null => IntConst(0), | ||
| _ => IntConst(0), |
There was a problem hiding this comment.
Unknown and null literals default to 0.
Lines 180-181 map both null literals and unrecognized literal types to IntConst(0). This loses semantic information and may introduce incorrect semantics (e.g., null reference vs. zero value).
Consider either:
- Emitting a distinct term for
null(e.g.,NullConst()) - Logging a warning for unhandled literal types
- Throwing an exception to fail fast on unexpected cases
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines
180 - 181, The pattern in ContractEmitter that maps both null and all unknown
literals to IntConst(0) loses semantics; update the literal-to-term mapping so
the null case emits a distinct null term (e.g., emit NullConst() in the null
match arm of the method that handles literals in ContractEmitter) and change the
wildcard/default arm from IntConst(0) to either throw an exception or log a
warning and fail fast for unrecognized literal types; ensure you only use
IntConst(0) for actual integer literals and keep the change localized to the
literal mapping logic (the match expression handling literals in
ContractEmitter).
Comment on lines
+16
to
+17
| <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="4.13.0" /> | ||
| <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" /> |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check package versions on NuGet
echo "Checking Microsoft.CodeAnalysis.CSharp 4.13.0:"
curl -s "https://api.nuget.org/v3-flatcontainer/microsoft.codeanalysis.csharp/index.json" | jq '.versions[] | select(. == "4.13.0")'
echo -e "\nChecking System.CommandLine versions:"
curl -s "https://api.nuget.org/v3-flatcontainer/system.commandline/index.json" | jq '.versions[-5:]'Repository: TSavo/provekit
Length of output: 271
🏁 Script executed:
cat implementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj | head -30Repository: TSavo/provekit
Length of output: 649
🏁 Script executed:
# Check if the specific beta version of System.CommandLine exists on NuGet
curl -s "https://api.nuget.org/v3-flatcontainer/system.commandline/2.0.0-beta4.22272.1/system.commandline.2.0.0-beta4.22272.1.nupkg" -I | head -5Repository: TSavo/provekit
Length of output: 210
🏁 Script executed:
# Check Microsoft.CodeAnalysis.CSharp 4.13.0 framework support metadata
curl -s "https://api.nuget.org/v3/registration5-semver1/microsoft.codeanalysis.csharp/4.13.0.json" | jq '.data[0].catalogEntry | {frameworks: .frameworkAssemblyGroup, dependencies: .dependencyGroups}'Repository: TSavo/provekit
Length of output: 107
🏁 Script executed:
# Check System.CommandLine beta version metadata
curl -s "https://api.nuget.org/v3/registration5-semver1/system.commandline/2.0.0-beta4.22272.1.json" | jq '.data[0].catalogEntry | {frameworks: .frameworkAssemblyGroup, targetFrameworks: .targetFramework, dependencies: .dependencyGroups}'Repository: TSavo/provekit
Length of output: 115
🏁 Script executed:
# Try alternative metadata endpoint for Microsoft.CodeAnalysis.CSharp
curl -s "https://api.nuget.org/v3-flatcontainer/microsoft.codeanalysis.csharp/4.13.0/microsoft.codeanalysis.csharp.nuspec" | grep -E 'targetFramework|group|dependency' | head -20Repository: TSavo/provekit
Length of output: 1730
🏁 Script executed:
# Check System.CommandLine versions available (get full list to find the beta)
curl -s "https://api.nuget.org/v3-flatcontainer/system.commandline/index.json" | jq '.versions | map(select(startswith("2.0.0-beta")))'Repository: TSavo/provekit
Length of output: 742
Update package versions for .NET 10.0 compatibility and production readiness.
-
Microsoft.CodeAnalysis.CSharp4.13.0 explicitly supports only net8.0, net9.0, and .NETStandard2.0 — it lacks explicit net10.0 support. Consider upgrading to a newer version that targets net10.0. -
System.CommandLine2.0.0-beta4.22272.1 is an outdated beta version. Stable releases (2.0.6, 2.0.7) are available and should be used instead for production.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj`
around lines 16 - 17, Update the PackageReference entries in the csproj for
Microsoft.CodeAnalysis.CSharp and System.CommandLine: bump
Microsoft.CodeAnalysis.CSharp to a stable release that explicitly supports
net10.0 (replace the current 4.13.0 with the latest stable net10-compatible
version) and replace System.CommandLine 2.0.0-beta4.22272.1 with a stable 2.0.x
release (e.g., 2.0.6 or 2.0.7). After updating the PackageReference versions in
Provekit.Lift.Csharp.csproj, run dotnet restore and build to verify
compatibility and fix any API changes reported by the compiler (check usages in
code that reference Roslyn APIs or System.CommandLine parsing/handler types).
There was a problem hiding this comment.
Pull request overview
This PR introduces a new C# (“csharp” / “csharp-source”) lift plugin implemented in C# (Roslyn-based) with an NDJSON JSON-RPC interface, plus a new menagerie language signature for C# and the repo wiring to register the surface.
Changes:
- Add
Provekit.Lift.Csharplifter/“compiler” with JSON-RPC methods (initialize,lift,compile,shutdown) and a new xUnit test project. - Add
menagerie/csharp-language-signature/signature specs (sorts, operations, equations, effect signatures). - Register
"csharp"as a known surface and add the lifter manifest + solution entries.
Reviewed changes
Copilot reviewed 74 out of 74 changed files in this pull request and generated 21 comments.
Show a summary per file
| File | Description |
|---|---|
| menagerie/csharp-language-signature/specs/sort_unit.spec.json | Adds Unit sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/sort_string.spec.json | Adds String sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/sort_stmt.spec.json | Adds Stmt sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/sort_int.spec.json | Adds Int sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/sort_expr.spec.json | Adds Expr sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/sort_bool.spec.json | Adds Bool sort spec for C# signature. |
| menagerie/csharp-language-signature/specs/op_while.spec.json | Adds while operation spec. |
| menagerie/csharp-language-signature/specs/op_sub.spec.json | Adds subtraction operation spec. |
| menagerie/csharp-language-signature/specs/op_skip.spec.json | Adds skip/no-op statement operation spec. |
| menagerie/csharp-language-signature/specs/op_shr.spec.json | Adds right shift operation spec. |
| menagerie/csharp-language-signature/specs/op_shl.spec.json | Adds left shift operation spec. |
| menagerie/csharp-language-signature/specs/op_seq.spec.json | Adds sequencing operation spec. |
| menagerie/csharp-language-signature/specs/op_return.spec.json | Adds return statement operation spec. |
| menagerie/csharp-language-signature/specs/op_preinc.spec.json | Adds pre-increment operation spec. |
| menagerie/csharp-language-signature/specs/op_predec.spec.json | Adds pre-decrement operation spec. |
| menagerie/csharp-language-signature/specs/op_postinc.spec.json | Adds post-increment operation spec. |
| menagerie/csharp-language-signature/specs/op_postdec.spec.json | Adds post-decrement operation spec. |
| menagerie/csharp-language-signature/specs/op_or.spec.json | Adds logical-or operation spec. |
| menagerie/csharp-language-signature/specs/op_not.spec.json | Adds logical-not operation spec. |
| menagerie/csharp-language-signature/specs/op_new.spec.json | Adds object-creation operation spec. |
| menagerie/csharp-language-signature/specs/op_neg.spec.json | Adds arithmetic negation operation spec. |
| menagerie/csharp-language-signature/specs/op_ne.spec.json | Adds != operation spec. |
| menagerie/csharp-language-signature/specs/op_mul.spec.json | Adds multiplication operation spec. |
| menagerie/csharp-language-signature/specs/op_mod.spec.json | Adds modulo operation spec. |
| menagerie/csharp-language-signature/specs/op_member.spec.json | Adds member-access operation spec. |
| menagerie/csharp-language-signature/specs/op_lt.spec.json | Adds < operation spec. |
| menagerie/csharp-language-signature/specs/op_le.spec.json | Adds <= operation spec. |
| menagerie/csharp-language-signature/specs/op_ite.spec.json | Adds conditional expression (?:) operation spec. |
| menagerie/csharp-language-signature/specs/op_index.spec.json | Adds indexer operation spec. |
| menagerie/csharp-language-signature/specs/op_if.spec.json | Adds if-statement operation spec. |
| menagerie/csharp-language-signature/specs/op_gt.spec.json | Adds > operation spec. |
| menagerie/csharp-language-signature/specs/op_ge.spec.json | Adds >= operation spec. |
| menagerie/csharp-language-signature/specs/op_foreach.spec.json | Adds foreach loop operation spec. |
| menagerie/csharp-language-signature/specs/op_for.spec.json | Adds for loop operation spec. |
| menagerie/csharp-language-signature/specs/op_eq.spec.json | Adds == operation spec. |
| menagerie/csharp-language-signature/specs/op_div.spec.json | Adds division operation spec. |
| menagerie/csharp-language-signature/specs/op_decl.spec.json | Adds local declaration operation spec. |
| menagerie/csharp-language-signature/specs/op_continue.spec.json | Adds continue statement operation spec. |
| menagerie/csharp-language-signature/specs/op_cast.spec.json | Adds cast operation spec. |
| menagerie/csharp-language-signature/specs/op_call.spec.json | Adds call operation spec. |
| menagerie/csharp-language-signature/specs/op_break.spec.json | Adds break statement operation spec. |
| menagerie/csharp-language-signature/specs/op_bitxor.spec.json | Adds bitwise XOR operation spec. |
| menagerie/csharp-language-signature/specs/op_bitor.spec.json | Adds bitwise OR operation spec. |
| menagerie/csharp-language-signature/specs/op_bitnot.spec.json | Adds bitwise NOT operation spec. |
| menagerie/csharp-language-signature/specs/op_bitand.spec.json | Adds bitwise AND operation spec. |
| menagerie/csharp-language-signature/specs/op_assign.spec.json | Adds assignment operation spec. |
| menagerie/csharp-language-signature/specs/op_and.spec.json | Adds logical-and operation spec. |
| menagerie/csharp-language-signature/specs/op_add.spec.json | Adds addition operation spec. |
| menagerie/csharp-language-signature/specs/language_signature_csharp.spec.json | Registers all sorts/ops/equations/effects for the C# signature. |
| menagerie/csharp-language-signature/specs/eq_seq_skip_right.spec.json | Adds seq/skip-right equation. |
| menagerie/csharp-language-signature/specs/eq_seq_skip_left.spec.json | Adds seq/skip-left equation. |
| menagerie/csharp-language-signature/specs/eq_seq_assoc.spec.json | Adds seq associativity equation. |
| menagerie/csharp-language-signature/specs/effsig_write.spec.json | Adds MemWrite effect signature catalog entry. |
| menagerie/csharp-language-signature/specs/effsig_read.spec.json | Adds MemRead effect signature catalog entry. |
| menagerie/csharp-language-signature/specs/effsig_loop.spec.json | Adds Loop effect signature catalog entry. |
| menagerie/csharp-language-signature/specs/effsig_call.spec.json | Adds Call effect signature catalog entry. |
| menagerie/csharp-language-signature/specs/effsig_alloc.spec.json | Adds Alloc effect signature catalog entry. |
| menagerie/csharp-language-signature/specs/eff_write.spec.json | Adds write effect operation spec. |
| menagerie/csharp-language-signature/specs/eff_read.spec.json | Adds read effect operation spec. |
| menagerie/csharp-language-signature/specs/eff_loop.spec.json | Adds loop effect operation spec. |
| menagerie/csharp-language-signature/specs/eff_call.spec.json | Adds call effect operation spec. |
| menagerie/csharp-language-signature/specs/eff_alloc.spec.json | Adds alloc effect operation spec. |
| implementations/rust/provekit-cli/src/project_config.rs | Registers "csharp" in KNOWN_SURFACES. |
| implementations/csharp/Provekit.sln | Adds the new lifter and its tests to the solution. |
| implementations/csharp/Provekit.Lift.Csharp/RpcServer.cs | Implements JSON-RPC dispatch loop and result shaping for lift/compile. |
| implementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj | Adds new lifter project + Roslyn/System.CommandLine deps. |
| implementations/csharp/Provekit.Lift.Csharp/Program.cs | Adds CLI entrypoint with --rpc mode. |
| implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs | Implements Roslyn parse + per-method contract extraction. |
| implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs | Implements IR-to-C# emission (round-trip compiler). |
| implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs | Emits function-contract IR and C#-namespaced terms/effects. |
| implementations/csharp/Provekit.Lift.Csharp.Tests/Provekit.Lift.Csharp.Tests.csproj | Adds xUnit test project for the lifter. |
| implementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.cs | Adds lifter/compiler round-trip smoke tests. |
| implementations/csharp/Provekit.Lift.Csharp.Tests/fixtures/sample.cs | Adds fixture C# source for tests. |
| implementations/csharp/.provekit/lift/csharp/manifest.toml | Points provekit lift to the new C# lifter and advertises capabilities. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+39
to
+53
| return new JsonObject | ||
| { | ||
| ["schemaVersion"] = "1", | ||
| ["kind"] = "function-contract", | ||
| ["fnName"] = _method.Identifier.Text, | ||
| ["formals"] = JsonSerializer.SerializeToNode(formals), | ||
| ["formalSorts"] = JsonSerializer.SerializeToNode(formalSorts), | ||
| ["returnSort"] = PrimSort("Int"), | ||
| ["pre"] = TrueFormula(), | ||
| ["post"] = EqFormula(VarTerm("return_value"), stmtTerm), | ||
| ["bodyCid"] = null, | ||
| ["effects"] = JsonSerializer.SerializeToNode(_effects), | ||
| ["locus"] = new JsonObject { ["file"] = _path, ["line"] = line, ["col"] = 1 }, | ||
| ["autoMintedMementos"] = new JsonArray(), | ||
| }; |
Comment on lines
+214
to
+215
| var precond = DivByZeroPrecondition(op, rhs); | ||
| return Ctor(op, lhs, rhs, precond); |
Comment on lines
+315
to
+318
| return new JsonObject | ||
| { | ||
| ["kind"] = "ctor", | ||
| ["name"] = name, |
| ["sort"] = PrimSort("String"), | ||
| }; | ||
|
|
||
| private JsonObject Unit() => IntConst(0); |
Comment on lines
+372
to
+377
| private void AddEffect(string kind, string target) | ||
| { | ||
| var key = $"{kind}:{target}"; | ||
| if (_seenEffects.Add(key)) | ||
| { | ||
| _effects.Add(new JsonObject { ["kind"] = kind, ["target"] = target }); |
| { | ||
| "kind": "effect_signature", | ||
| "fn_name": "csharp:effect-signature:Call", | ||
| "sorts": ["sort_string.spec.json"], |
| { | ||
| "kind": "effect_signature", | ||
| "fn_name": "csharp:effect-signature:MemWrite", | ||
| "sorts": ["sort_string.spec.json"], |
| { | ||
| "kind": "effect_signature", | ||
| "fn_name": "csharp:effect-signature:MemRead", | ||
| "sorts": ["sort_string.spec.json"], |
| { | ||
| "kind": "effect_signature", | ||
| "fn_name": "csharp:effect-signature:Alloc", | ||
| "sorts": ["sort_string.spec.json"], |
| { | ||
| "kind": "effect_signature", | ||
| "fn_name": "csharp:effect-signature:Loop", | ||
| "sorts": ["sort_string.spec.json"], |
Owner
Author
Deep review — C# source language lifterReviewed Verdict: CHANGES-REQUIREDThe bones are sound — the project is isolated to Blocking1. [Critical] Every binop emitted with a spurious 3rd var precond = DivByZeroPrecondition(op, rhs); // always IntConst(0)
return Ctor(op, lhs, rhs, precond); // EVERY binop emitted with 3 args
...
private JsonObject DivByZeroPrecondition(string op, JsonObject rhs) => IntConst(0);Fires for all 19 binops ( 2. [Critical] No 3. [Critical] The "round-trip" test asserts nothing. 4. [Critical] Silent information loss on unhandled syntax (the corpus- 5. [Major] Path-traversal — 6. [Major] Contract names collide for nested / partial / overloaded methods. 7. [Major] Dangling effect-signature reference. 8. [Major] Non-blocking
60-second summary for the next readerLook at — automated deep review (Opus) |
TSavo
force-pushed
the
csharp-lifter-roundtrip
branch
5 times, most recently
from
03f7d12 to
8bcfcb6
Compare
…signature Add a C# source-to-IR lifter and IR-to-C# compiler with full round-trip support, integrated via the provekit RPC protocol. - Implement CsharpLifter using Roslyn to parse C# source and emit function-contract IR terms - Implement CsharpCompiler to lower IR terms back to C# source - Implement JSON-RPC server (initialize, lift, compile, shutdown) for provekit CLI integration - Add ContractEmitter walking C# methods (statements, expressions, control flow) into csharp:-namespaced IR ops - Update manifest.toml to point to the new lifter project - Register 'csharp' in KNOWN_SURFACES for project_config.rs - Add C# language signature menagerie with 6 sorts, 42 operations, 3 equations, 5 effect signatures - Add test suite (7 tests) validating lifting, compilation, round-trip, and void-method refusal - Fix fixture files to use proper class-wrapped methods for Roslyn semantic resolution
TSavo
force-pushed
the
csharp-lifter-roundtrip
branch
from
8bcfcb6 to
3fb642e
Compare
The rebase onto main (post-#589 CLR lifter) left unresolved <<<<<<< / ======= / >>>>>>> markers in the ProjectConfigurationPlatforms section of Provekit.sln, which broke `make build-csharp` -> `make cross-kit-conformance` (MSB5007: "<<<<<<< HEAD" is invalid). Resolved by union: keep both the CLR lifter+test project configs and the C# lifter+test project configs (all four GUIDs already had clean Project declarations; only the config-platform block conflicted). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 5
♻️ Duplicate comments (3)
implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs (3)
36-50:⚠️ Potential issue | 🟠 Major | 🏗️ Heavy liftUse semantic types for
formalSortsandreturnSort.This still emits every parameter and return as
Int, sobool,string, nullable, and reference-typed methods are lifted with the wrong signature.LiftSourceonly rejectsvoid, so non-Intmethods currently produce unsound contracts instead of refusals or correctly typed IR.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines 36 - 50, The contract emitter is hardcoding all parameter and return sorts to Int (see ParameterList, formalSorts, PrimSort and returnSort) which makes bool/string/nullable/reference types unsound; update Emit logic in ContractEmitter.cs to compute semantic sorts from the method's semantic model/type info instead of using PrimSort("Int"): for each parameter in _method.ParameterList and for the method return type use the Roslyn semantic model to get the ITypeSymbol (or use existing type-resolving helper), map that symbol to the correct lift sort (e.g., Bool, Int, String, Nullable<T>, Ref) and populate formalSorts and returnSort accordingly, and ensure functions like PrimSort or any mapping helper are extended/used to produce the proper Json node instead of always "Int" while leaving TrueFormula() and fnName generation unchanged.
187-195:⚠️ Potential issue | 🟠 Major | ⚡ Quick winDon't coerce
nullor unknown literals to0.Both branches silently change program meaning and recreate the silent-skew problem the lifter is supposed to refuse. Throw here until there's a real null/unsupported-literal representation so
LiftSourcerecords a refusal instead of bogus IR.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines 187 - 195, The switch in ContractEmitter that maps lit.Token.Value to IR currently coerces null/unknown values to IntConst(0); instead change the null and default branches to throw a descriptive exception (e.g., InvalidOperationException or a custom LiftingRefusalException) so that LiftSource records a refusal rather than producing bogus IR—update the lit.Token.Value switch (the branches that now return IntConst(0) for null and _ ) to throw with a message including the literal value/type and keep the int/long/bool/string branches returning IntConst/BoolConst/StrConst as before.
50-50:⚠️ Potential issue | 🔴 Critical | 🏗️ Heavy liftPropagate
/and%guards into the function precondition.
csharp:divandcsharp:modnow requirerhs != 0, but every emitted function contract still has"pre": true. A lifted method containing division or modulo is therefore callable without the guard its operator specs require.Also applies to: 201-227
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` at line 50, The emitted contract currently sets ["pre"] = TrueFormula(), so division/modulo guards (csharp:div and csharp:mod require rhs != 0) are not enforced; update the contract emission in ContractEmitter.cs to collect guard predicates produced for operations (e.g., zero-checks for csharp:div and csharp:mod), conjoin them with any existing precondition instead of using TrueFormula(), and assign that conjunction to ["pre"]; apply the same change to the other emission sites referenced (the block around lines 201-227) so all emitted function contracts include the rhs != 0 guards.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs`:
- Around line 305-308: In the ElementAccessExpressionSyntax handling in
ContractEmitter.cs (the case that currently returns Ctor("csharp:index",
EmitExpression(elem.Expression),
EmitExpression(elem.ArgumentList.Arguments[0].Expression))), avoid dropping
additional index arguments: collect all argument expressions from
elem.ArgumentList.Arguments, map each to EmitExpression, and pass the full list
of emitted index values into the Ctor("csharp:index", ...) call (or into
whatever container/arity the IR expects) so multidimensional accesses like a[i,
j] are encoded correctly; if the IR cannot represent multiple indices, instead
throw an explicit exception (from this branch) refusing to lift the construct
rather than silently using only the first argument.
- Around line 257-271: The emitted csharp:call (and similarly csharp:new)
currently spreads each argument into separate ctor slots; change EmitExpression
handling inside the InvocationExpressionSyntax case (and the
ObjectCreationExpressionSyntax case around the same area) so that after
computing args = inv.ArgumentList.Arguments.Select(...).ToList() you wrap those
elements into a single JsonArray/JsonObject representing the "args" slot and
pass that as one ctor argument after StrConst(methodName) (instead of AddRange),
i.e., construct callArgs as [StrConst(methodName), JsonArrayOf(args)] before
calling Ctor("csharp:call", ...); keep calling
AddUnresolvedCallEffect(methodName) as-is. Ensure the same pattern is applied to
the new-object emission that uses Ctor("csharp:new", ...).
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs`:
- Around line 93-100: WrapSeq is currently pulling expression RHSs via
d["post"]["args"][1] which yields raw expressions not lifted Stmt nodes; instead
locate the lifted statement in each declaration (e.g. check d["stmt"] or
d["body"] or the field your lifter uses to store lifted Stmt) and use that as
the element to sequence. If a declaration only has an expression, wrap it into a
statement node (e.g. create an expression-statement via Ctor, such as
Ctor("csharp:expr-stmt", expr)) as a fallback, then sequence those statements
with Ctor("csharp:seq", ...); keep Skip() behaviour when none found. Ensure this
change is made in WrapSeq and reuse Ctor/Skip as in the existing code.
In `@menagerie/csharp-language-signature/specs/op_assign.spec.json`:
- Around line 4-17: The spec for the "assign" operation is too narrow:
ContractEmitter now emits complex lvalues via EmitExpression(assign.Left)
(members/indexers) but the op_assign spec uses Int for both slots and arity,
causing mismatches; update the op signature in op_assign.spec.json (operator
"assign", formals ["lvalue","rvalue"], symbol names shown) to use a more general
sort (e.g., change the two formal_sorts and the arity array from {"name":"Int"}
/ "Int" to a broader sort such as {"kind":"ctor","name":"Expr","args":[]} /
"Expr" or another appropriate supertype used for emitted expressions), and keep
arity_shape and result ("Stmt") intact so field/element assignments type-check
against ContractEmitter's EmitExpression output.
---
Duplicate comments:
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs`:
- Around line 36-50: The contract emitter is hardcoding all parameter and return
sorts to Int (see ParameterList, formalSorts, PrimSort and returnSort) which
makes bool/string/nullable/reference types unsound; update Emit logic in
ContractEmitter.cs to compute semantic sorts from the method's semantic
model/type info instead of using PrimSort("Int"): for each parameter in
_method.ParameterList and for the method return type use the Roslyn semantic
model to get the ITypeSymbol (or use existing type-resolving helper), map that
symbol to the correct lift sort (e.g., Bool, Int, String, Nullable<T>, Ref) and
populate formalSorts and returnSort accordingly, and ensure functions like
PrimSort or any mapping helper are extended/used to produce the proper Json node
instead of always "Int" while leaving TrueFormula() and fnName generation
unchanged.
- Around line 187-195: The switch in ContractEmitter that maps lit.Token.Value
to IR currently coerces null/unknown values to IntConst(0); instead change the
null and default branches to throw a descriptive exception (e.g.,
InvalidOperationException or a custom LiftingRefusalException) so that
LiftSource records a refusal rather than producing bogus IR—update the
lit.Token.Value switch (the branches that now return IntConst(0) for null and _
) to throw with a message including the literal value/type and keep the
int/long/bool/string branches returning IntConst/BoolConst/StrConst as before.
- Line 50: The emitted contract currently sets ["pre"] = TrueFormula(), so
division/modulo guards (csharp:div and csharp:mod require rhs != 0) are not
enforced; update the contract emission in ContractEmitter.cs to collect guard
predicates produced for operations (e.g., zero-checks for csharp:div and
csharp:mod), conjoin them with any existing precondition instead of using
TrueFormula(), and assign that conjunction to ["pre"]; apply the same change to
the other emission sites referenced (the block around lines 201-227) so all
emitted function contracts include the rhs != 0 guards.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 60c9a9ca-f695-4cc8-8c34-4e8596276d77
📒 Files selected for processing (75)
implementations/csharp/.provekit/lift/csharp/manifest.tomlimplementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.csimplementations/csharp/Provekit.Lift.Csharp.Tests/Provekit.Lift.Csharp.Tests.csprojimplementations/csharp/Provekit.Lift.Csharp.Tests/fixtures/sample.csimplementations/csharp/Provekit.Lift.Csharp/ContractEmitter.csimplementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.csimplementations/csharp/Provekit.Lift.Csharp/CsharpLifter.csimplementations/csharp/Provekit.Lift.Csharp/Program.csimplementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csprojimplementations/csharp/Provekit.Lift.Csharp/RpcServer.csimplementations/csharp/Provekit.slnimplementations/rust/provekit-cli/src/project_config.rsmenagerie/csharp-language-signature/specs/eff_alloc.spec.jsonmenagerie/csharp-language-signature/specs/eff_call.spec.jsonmenagerie/csharp-language-signature/specs/eff_loop.spec.jsonmenagerie/csharp-language-signature/specs/eff_read.spec.jsonmenagerie/csharp-language-signature/specs/eff_write.spec.jsonmenagerie/csharp-language-signature/specs/effsig_alloc.spec.jsonmenagerie/csharp-language-signature/specs/effsig_call.spec.jsonmenagerie/csharp-language-signature/specs/effsig_loop.spec.jsonmenagerie/csharp-language-signature/specs/effsig_read.spec.jsonmenagerie/csharp-language-signature/specs/effsig_write.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_assoc.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_skip_left.spec.jsonmenagerie/csharp-language-signature/specs/eq_seq_skip_right.spec.jsonmenagerie/csharp-language-signature/specs/language_signature_csharp.spec.jsonmenagerie/csharp-language-signature/specs/op_add.spec.jsonmenagerie/csharp-language-signature/specs/op_and.spec.jsonmenagerie/csharp-language-signature/specs/op_assign.spec.jsonmenagerie/csharp-language-signature/specs/op_bitand.spec.jsonmenagerie/csharp-language-signature/specs/op_bitnot.spec.jsonmenagerie/csharp-language-signature/specs/op_bitor.spec.jsonmenagerie/csharp-language-signature/specs/op_bitxor.spec.jsonmenagerie/csharp-language-signature/specs/op_break.spec.jsonmenagerie/csharp-language-signature/specs/op_call.spec.jsonmenagerie/csharp-language-signature/specs/op_cast.spec.jsonmenagerie/csharp-language-signature/specs/op_continue.spec.jsonmenagerie/csharp-language-signature/specs/op_decl.spec.jsonmenagerie/csharp-language-signature/specs/op_div.spec.jsonmenagerie/csharp-language-signature/specs/op_eq.spec.jsonmenagerie/csharp-language-signature/specs/op_for.spec.jsonmenagerie/csharp-language-signature/specs/op_foreach.spec.jsonmenagerie/csharp-language-signature/specs/op_ge.spec.jsonmenagerie/csharp-language-signature/specs/op_gt.spec.jsonmenagerie/csharp-language-signature/specs/op_if.spec.jsonmenagerie/csharp-language-signature/specs/op_index.spec.jsonmenagerie/csharp-language-signature/specs/op_ite.spec.jsonmenagerie/csharp-language-signature/specs/op_le.spec.jsonmenagerie/csharp-language-signature/specs/op_lt.spec.jsonmenagerie/csharp-language-signature/specs/op_member.spec.jsonmenagerie/csharp-language-signature/specs/op_mod.spec.jsonmenagerie/csharp-language-signature/specs/op_mul.spec.jsonmenagerie/csharp-language-signature/specs/op_ne.spec.jsonmenagerie/csharp-language-signature/specs/op_neg.spec.jsonmenagerie/csharp-language-signature/specs/op_new.spec.jsonmenagerie/csharp-language-signature/specs/op_not.spec.jsonmenagerie/csharp-language-signature/specs/op_or.spec.jsonmenagerie/csharp-language-signature/specs/op_postdec.spec.jsonmenagerie/csharp-language-signature/specs/op_postinc.spec.jsonmenagerie/csharp-language-signature/specs/op_predec.spec.jsonmenagerie/csharp-language-signature/specs/op_preinc.spec.jsonmenagerie/csharp-language-signature/specs/op_return.spec.jsonmenagerie/csharp-language-signature/specs/op_seq.spec.jsonmenagerie/csharp-language-signature/specs/op_shl.spec.jsonmenagerie/csharp-language-signature/specs/op_shr.spec.jsonmenagerie/csharp-language-signature/specs/op_skip.spec.jsonmenagerie/csharp-language-signature/specs/op_source-unit.spec.jsonmenagerie/csharp-language-signature/specs/op_sub.spec.jsonmenagerie/csharp-language-signature/specs/op_while.spec.jsonmenagerie/csharp-language-signature/specs/sort_bool.spec.jsonmenagerie/csharp-language-signature/specs/sort_expr.spec.jsonmenagerie/csharp-language-signature/specs/sort_int.spec.jsonmenagerie/csharp-language-signature/specs/sort_stmt.spec.jsonmenagerie/csharp-language-signature/specs/sort_string.spec.jsonmenagerie/csharp-language-signature/specs/sort_unit.spec.json
✅ Files skipped from review due to trivial changes (25)
- menagerie/csharp-language-signature/specs/op_eq.spec.json
- menagerie/csharp-language-signature/specs/eff_alloc.spec.json
- menagerie/csharp-language-signature/specs/eff_read.spec.json
- menagerie/csharp-language-signature/specs/op_break.spec.json
- menagerie/csharp-language-signature/specs/op_shl.spec.json
- implementations/csharp/Provekit.Lift.Csharp/Provekit.Lift.Csharp.csproj
- menagerie/csharp-language-signature/specs/sort_expr.spec.json
- menagerie/csharp-language-signature/specs/effsig_loop.spec.json
- menagerie/csharp-language-signature/specs/op_bitxor.spec.json
- menagerie/csharp-language-signature/specs/eq_seq_skip_right.spec.json
- menagerie/csharp-language-signature/specs/sort_bool.spec.json
- menagerie/csharp-language-signature/specs/op_preinc.spec.json
- menagerie/csharp-language-signature/specs/op_skip.spec.json
- menagerie/csharp-language-signature/specs/op_neg.spec.json
- menagerie/csharp-language-signature/specs/sort_unit.spec.json
- menagerie/csharp-language-signature/specs/op_le.spec.json
- menagerie/csharp-language-signature/specs/effsig_write.spec.json
- menagerie/csharp-language-signature/specs/eq_seq_assoc.spec.json
- menagerie/csharp-language-signature/specs/sort_string.spec.json
- implementations/rust/provekit-cli/src/project_config.rs
- menagerie/csharp-language-signature/specs/op_sub.spec.json
- menagerie/csharp-language-signature/specs/sort_int.spec.json
- menagerie/csharp-language-signature/specs/op_cast.spec.json
- implementations/csharp/Provekit.Lift.Csharp.Tests/fixtures/sample.cs
- menagerie/csharp-language-signature/specs/op_shr.spec.json
🚧 Files skipped from review as they are similar to previous changes (44)
- menagerie/csharp-language-signature/specs/op_index.spec.json
- menagerie/csharp-language-signature/specs/effsig_read.spec.json
- menagerie/csharp-language-signature/specs/eq_seq_skip_left.spec.json
- menagerie/csharp-language-signature/specs/effsig_call.spec.json
- menagerie/csharp-language-signature/specs/op_mul.spec.json
- menagerie/csharp-language-signature/specs/op_ge.spec.json
- menagerie/csharp-language-signature/specs/op_return.spec.json
- menagerie/csharp-language-signature/specs/op_ite.spec.json
- menagerie/csharp-language-signature/specs/eff_loop.spec.json
- menagerie/csharp-language-signature/specs/op_lt.spec.json
- menagerie/csharp-language-signature/specs/op_ne.spec.json
- menagerie/csharp-language-signature/specs/op_bitand.spec.json
- menagerie/csharp-language-signature/specs/effsig_alloc.spec.json
- menagerie/csharp-language-signature/specs/op_seq.spec.json
- menagerie/csharp-language-signature/specs/op_foreach.spec.json
- menagerie/csharp-language-signature/specs/op_add.spec.json
- menagerie/csharp-language-signature/specs/op_decl.spec.json
- menagerie/csharp-language-signature/specs/op_postinc.spec.json
- menagerie/csharp-language-signature/specs/language_signature_csharp.spec.json
- menagerie/csharp-language-signature/specs/op_if.spec.json
- menagerie/csharp-language-signature/specs/op_predec.spec.json
- menagerie/csharp-language-signature/specs/op_bitor.spec.json
- menagerie/csharp-language-signature/specs/op_or.spec.json
- menagerie/csharp-language-signature/specs/eff_call.spec.json
- menagerie/csharp-language-signature/specs/op_while.spec.json
- menagerie/csharp-language-signature/specs/op_call.spec.json
- implementations/csharp/Provekit.Lift.Csharp/Program.cs
- menagerie/csharp-language-signature/specs/sort_stmt.spec.json
- menagerie/csharp-language-signature/specs/op_continue.spec.json
- menagerie/csharp-language-signature/specs/eff_write.spec.json
- implementations/csharp/Provekit.sln
- menagerie/csharp-language-signature/specs/op_bitnot.spec.json
- implementations/csharp/.provekit/lift/csharp/manifest.toml
- menagerie/csharp-language-signature/specs/op_member.spec.json
- menagerie/csharp-language-signature/specs/op_gt.spec.json
- implementations/csharp/Provekit.Lift.Csharp.Tests/Provekit.Lift.Csharp.Tests.csproj
- menagerie/csharp-language-signature/specs/op_and.spec.json
- implementations/csharp/Provekit.Lift.Csharp/RpcServer.cs
- menagerie/csharp-language-signature/specs/op_not.spec.json
- menagerie/csharp-language-signature/specs/op_postdec.spec.json
- menagerie/csharp-language-signature/specs/op_new.spec.json
- implementations/csharp/Provekit.Lift.Csharp/CsharpCompiler.cs
- implementations/csharp/Provekit.Lift.Csharp.Tests/LifterTests.cs
- menagerie/csharp-language-signature/specs/op_for.spec.json
Comment on lines
+257
to
+271
| case InvocationExpressionSyntax inv: | ||
| { | ||
| var symbol = _model.GetSymbolInfo(inv).Symbol as IMethodSymbol; | ||
| var methodName = symbol?.ToDisplayString() ?? "unknown"; | ||
|
|
||
| var args = inv.ArgumentList.Arguments | ||
| .Select(a => EmitExpression(a.Expression)) | ||
| .ToList(); | ||
|
|
||
| AddUnresolvedCallEffect(methodName); | ||
|
|
||
| var callArgs = new List<JsonObject> { StrConst(methodName) }; | ||
| callArgs.AddRange(args); | ||
| return Ctor("csharp:call", callArgs.ToArray()); | ||
| } |
There was a problem hiding this comment.
Match csharp:call and csharp:new to the menagerie arity shape.
Both emitters flatten every argument into separate ctor slots. The language signature models these with a single args slot, so multi-argument calls/constructions produced here will not validate or round-trip consistently against the shipped specs.
Also applies to: 294-302
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines
257 - 271, The emitted csharp:call (and similarly csharp:new) currently spreads
each argument into separate ctor slots; change EmitExpression handling inside
the InvocationExpressionSyntax case (and the ObjectCreationExpressionSyntax case
around the same area) so that after computing args =
inv.ArgumentList.Arguments.Select(...).ToList() you wrap those elements into a
single JsonArray/JsonObject representing the "args" slot and pass that as one
ctor argument after StrConst(methodName) (instead of AddRange), i.e., construct
callArgs as [StrConst(methodName), JsonArrayOf(args)] before calling
Ctor("csharp:call", ...); keep calling AddUnresolvedCallEffect(methodName)
as-is. Ensure the same pattern is applied to the new-object emission that uses
Ctor("csharp:new", ...).
Comment on lines
+305
to
+308
| case ElementAccessExpressionSyntax elem: | ||
| return Ctor("csharp:index", | ||
| EmitExpression(elem.Expression), | ||
| EmitExpression(elem.ArgumentList.Arguments[0].Expression)); |
There was a problem hiding this comment.
Don't drop additional index arguments.
elem.ArgumentList.Arguments[0] silently discards the rest of a multidimensional access or custom indexer, so a[i, j] is lifted as if it were single-argument. Either encode all indices or throw so the lifter refuses the construct instead of emitting skewed IR.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/ContractEmitter.cs` around lines
305 - 308, In the ElementAccessExpressionSyntax handling in ContractEmitter.cs
(the case that currently returns Ctor("csharp:index",
EmitExpression(elem.Expression),
EmitExpression(elem.ArgumentList.Arguments[0].Expression))), avoid dropping
additional index arguments: collect all argument expressions from
elem.ArgumentList.Arguments, map each to EmitExpression, and pass the full list
of emitted index values into the Ctor("csharp:index", ...) call (or into
whatever container/arity the IR expects) so multidimensional accesses like a[i,
j] are encoded correctly; if the IR cannot represent multiple indices, instead
throw an explicit exception (from this branch) refusing to lift the construct
rather than silently using only the first argument.
Comment on lines
+64
to
+65
| string source; | ||
| try { source = File.ReadAllText(path); } |
There was a problem hiding this comment.
Preserve raw file bytes in csharp:source-unit.
File.ReadAllText plus StrConst(source) only stores decoded text. The original bytes, encoding, and exact on-disk representation are already lost at that point, so the bytes slot cannot satisfy the “source bytes are recoverable” contract.
Also applies to: 74-84
Comment on lines
+93
to
+100
| private static JsonObject WrapSeq(List<JsonObject> decls, int start) | ||
| { | ||
| var contracts = decls.Skip(start).Select(d => d["post"]?["args"]?[1]).Where(n => n is not null).ToList(); | ||
| if (contracts.Count == 0) return Skip(); | ||
| var result = contracts[0]!.AsObject(); | ||
| for (int i = 1; i < contracts.Count; i++) | ||
| result = Ctor("csharp:seq", result, contracts[i]!.AsObject()); | ||
| return result; |
There was a problem hiding this comment.
WrapSeq is extracting postcondition RHSs, not lifted statements.
For a trivial method like return a + b;, d["post"]["args"][1] is just the expression term a + b, not a Stmt. That means csharp:source-unit can end up wrapping expressions where its spec requires an operational Stmt, which breaks the claimed round-trip wrapper.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/csharp/Provekit.Lift.Csharp/CsharpLifter.cs` around lines 93
- 100, WrapSeq is currently pulling expression RHSs via d["post"]["args"][1]
which yields raw expressions not lifted Stmt nodes; instead locate the lifted
statement in each declaration (e.g. check d["stmt"] or d["body"] or the field
your lifter uses to store lifted Stmt) and use that as the element to sequence.
If a declaration only has an expression, wrap it into a statement node (e.g.
create an expression-statement via Ctor, such as Ctor("csharp:expr-stmt", expr))
as a fallback, then sequence those statements with Ctor("csharp:seq", ...); keep
Skip() behaviour when none found. Ensure this change is made in WrapSeq and
reuse Ctor/Skip as in the existing code.
Comment on lines
+4
to
+17
| "formals": ["lvalue", "rvalue"], | ||
| "formal_sorts": [ | ||
| {"kind": "ctor", "name": "Int", "args": []}, | ||
| {"kind": "ctor", "name": "Int", "args": []} | ||
| ], | ||
| "return_sort": {"kind": "ctor", "name": "Stmt", "args": []}, | ||
| "pre": {"kind": "atomic", "name": "true", "args": []}, | ||
| "post": { | ||
| "kind": "operation-contract", | ||
| "operator": "assign", | ||
| "arity": ["Int", "Int"], | ||
| "result": "Stmt", | ||
| "wp": "post[rvalue / lvalue] (lvalue updated to rvalue)", | ||
| "arity_shape": {"kind": "named", "slots": [{"name": "lvalue"}, {"name": "rvalue"}]} |
There was a problem hiding this comment.
csharp:assign is typed too narrowly for the emitted lvalues.
ContractEmitter now lifts assignment targets via EmitExpression(assign.Left), which can produce member/index terms, but this spec still requires both slots to be Int. That makes field and element assignments ill-typed against the shipped signature.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@menagerie/csharp-language-signature/specs/op_assign.spec.json` around lines 4
- 17, The spec for the "assign" operation is too narrow: ContractEmitter now
emits complex lvalues via EmitExpression(assign.Left) (members/indexers) but the
op_assign spec uses Int for both slots and arity, causing mismatches; update the
op signature in op_assign.spec.json (operator "assign", formals
["lvalue","rvalue"], symbol names shown) to use a more general sort (e.g.,
change the two formal_sorts and the arity array from {"name":"Int"} / "Int" to a
broader sort such as {"kind":"ctor","name":"Expr","args":[]} / "Expr" or another
appropriate supertype used for emitted expressions), and keep arity_shape and
result ("Stmt") intact so field/element assignments type-check against
ContractEmitter's EmitExpression output.
…ve the source lifter its own `csharp-source` surface This PR had repointed `implementations/csharp/.provekit/lift/csharp/manifest.toml` at the new `Provekit.Lift.Csharp` source lifter (and set `working_dir` to a path that resolves outside the project root). But the `csharp` *kit* surface is the one `provekit mint --kit=csharp` uses to mint the C# kit's *self-contracts* (from `Provekit.SelfContracts`), so the repoint made `make conformance` mint an empty-set attestation with a blank `cid` -> `cross-kit-conformance` failed with `csharp.json cid is malformed`. Revert that manifest to `main`'s version (dispatch `Provekit.SelfContracts`, `working_dir = "."`). The new source lifter gets its own surface, `implementations/csharp/.provekit/lift/csharp-source/manifest.toml`, pointing at `Provekit.Lift.Csharp/bin/Release/net10.0/Provekit.Lift.Csharp.dll --rpc` (mirroring how `clr-bytecode` coexists alongside `csharp`). The lifter already declares its dialect as `csharp-source`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 11, 2026
TSavo
added a commit
that referenced
this pull request
May 11, 2026
#592) * feat(go): add Go source lift kit (self-hosted) + go-language-signature menagerie A self-hosted Go source-language lift kit, mirroring PR #590 (the C# source lifter): a Go program using stdlib go/parser + go/ast + go/types that lifts Go function definitions into ProvekIt function-contract mementos over a go:-namespaced operation algebra, plus menagerie/go-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a go:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no go:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing go kit surface manifest is untouched; the source lifter gets its own go-source surface. go build/test/vet ./... pass incl nested modules. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(go): real round-trip test + refuse unresolved receivers + drop spurious menagerie/manifest.yaml entry Review fixes for PR #592: (1) the round-trip test only exercised the go:source-unit hex-decode fast path — added CompileBody so Compile can drive the IR-to-Go path on a bare body term, plus a test that lifts → extracts the body term → compiles it via that path → re-lifts → asserts byte-identical IR; (2) methods with unresolved/non-named receiver types are now refused (unresolved-receiver-type) rather than collapsed onto a colliding fnName; (3) removed the go-language-signature registration from menagerie/manifest.yaml (that file is a destinations: list of runnable exhibits — no *-language-signature catalog belongs there). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…age-signature (#594) * feat(python): add Python source lift kit (self-hosted) + python-language-signature menagerie A self-hosted Python source-language lift kit, mirroring PR #590 (the C# source lifter): a Python program using stdlib ast that lifts Python function definitions into ProvekIt function-contract mementos over a python:-namespaced operation algebra, plus menagerie/python-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a python:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no python:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing python kit surface manifest is untouched; the source lifter gets its own python-source surface. pytest pass 8 tests; signature --check pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(python): reuse the existing canonicalizer (was rolling its own, divergent on control chars) + real round-trip test + drop spurious menagerie/manifest.yaml entry Review fixes for PR #594: (1) canonical.py was computing canonical bytes via json.dumps which emits RFC-8785 named short escapes (\n, \t, ...) where the protocol canonicalizer escapes U+0000..U+001F as \u00XX — since python:source-unit always carries newline-laden source bytes and loopCid = cid_of_json(loop_term), every loop/source-unit CID was unreproducible by the Rust verifier; now delegates JCS + BLAKE3-512 to provekit_lift_py_tests.canonicalizer (the existing in-repo one), drops the blake3 PyPI dep, adds a newline-CID regression test; (2) added a body-term round-trip canonical-byte test driving the ast.unparse path (compile_body_term); (3) removed the python-language-signature entry from menagerie/manifest.yaml. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…signature (#595) * feat(ts): add TypeScript source lift kit (self-hosted) + ts-language-signature menagerie A self-hosted TypeScript source-language lift kit, mirroring PR #590 (the C# source lifter): a TypeScript program using the TypeScript compiler API that lifts TypeScript function definitions into ProvekIt function-contract mementos over a ts:-namespaced operation algebra, plus menagerie/ts-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a ts:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no ts:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing ts kit surface manifest is untouched; the source lifter gets its own ts-source surface. vitest 6/6 + full suite 785 tests pass; tsc --noEmit pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(ts): real round-trip test (drives the ts.createPrinter path) + distinct refusal reasons + drop spurious menagerie/manifest.yaml entry Review fixes for PR #595 (verdict was MERGE-WITH-NITS): (1) the lift(compile(lift(src))) test was tautological — compileTypeScriptSourceIr returns the stored <source-unit> bytes when one exists, so the ts.createPrinter AST-emit path was dead code under normal use; added compileTypeScriptSourceBodyIr so the test can compile a bare body term through the printer path, plus a canonical-byte/CID body-term round-trip test (kept the source-unit fast-path test too); (2) split the collapsed unsupported- function-shape refusal into a distinct reason per case (async / generator / decorator / generic / rest-param / default-param / destructured-param) so Refusal.reason is actionable; (3) removed the typescript-language-signature destination entry from menagerie/manifest.yaml (no *-language-signature catalog belongs in that list). NOTE: codex couldn't run tsc/vitest locally (sandbox blocked pnpm install — offline tarballs missing, online DNS ENOTFOUND); CI will verify. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…ture menagerie A self-hosted Zig source-language lift kit, mirroring PR #590 (the C# source lifter): a Zig program using std.zig.Ast that lifts Zig function definitions into ProvekIt function-contract mementos over a zig:-namespaced operation algebra, plus menagerie/zig-language-signature/, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a zig:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (comptime / error unions / try-catch / defer / async / inline-for / switch / @-builtins are refused; no zig:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs, a lift(compile(lift(src))) round-trip test, version 0.1.0-draft. The existing zig kit surface manifest (provekit-lift-zig) is untouched; the source lifter gets its own zig-source surface. make test-zig + zig build test pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…ture (#596) * feat(zig): add Zig source lift kit (self-hosted) + zig-language-signature menagerie A self-hosted Zig source-language lift kit, mirroring PR #590 (the C# source lifter): a Zig program using std.zig.Ast that lifts Zig function definitions into ProvekIt function-contract mementos over a zig:-namespaced operation algebra, plus menagerie/zig-language-signature/, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a zig:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (comptime / error unions / try-catch / defer / async / inline-for / switch / @-builtins are refused; no zig:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs, a lift(compile(lift(src))) round-trip test, version 0.1.0-draft. The existing zig kit surface manifest (provekit-lift-zig) is untouched; the source lifter gets its own zig-source surface. make test-zig + zig build test pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(zig): refuse escaped string literals; round-trip for/break/continue in the IR-to-Zig compiler Review nit-fixes for PR #596 (verdict was MERGE-WITH-NITS): (1) emitString refused to decode escape sequences — a Zig "oops\n" lifted to a Str term with a literal backslash-n, so the canonical term (and its CID) misrepresented the runtime value; now any string literal containing \ is refused with Refusal{kind:'unsupported-string-escape'} rather than lifted wrong (the Supra-omnia-rectum-aligned choice); (2) compileContract (the IR-to-Zig path) didn't handle zig:for / zig:break / zig:continue (they fell to a literal "unreachable"), so loop-bearing functions wouldn't round-trip and the single zig:add round-trip test camouflaged it; now those ops emit the corresponding Zig syntax and a loop-body canonical-byte round-trip test (via provekit-ir's jcsStringify/jcsHash) exercises it. make test-zig passes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…gnature menagerie A self-hosted Java source-language lift kit, mirroring PR #590 (the C# source lifter): a Java program using the JDK compiler API com.sun.source.* that lifts Java function definitions into ProvekIt function-contract mementos over a java:-namespaced operation algebra, plus menagerie/java-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a java:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no java:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing java kit surface manifest is untouched; the source lifter gets its own java-source surface. mvn -pl provekit-lift-java-source -am test pass; jar RPC reports 0.1.0-draft. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…gnature menagerie (#598) A self-hosted Ruby source-language lift kit, mirroring PR #590 (the C# source lifter) and the merged Go/Python/TypeScript/Zig lifters: a Ruby program using stdlib Ripper that lifts Ruby function definitions into ProvekIt function-contract mementos over a ruby:-namespaced operation algebra, plus menagerie/ruby-language-signature/, plus a round-trip compiler. Built to the conventions the C#/Go/Java/Python/TS/Zig review rounds settled: namespaced op CIDs, arity_shape on every op spec, a ruby:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no ruby:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs via the existing per-language canonicalizer (not a rolled-own one), a lift(compile(lift(src))) round-trip test driving the real IR->source compiler path (not just the source-unit byte-copy fast-path), deterministic JSON, version 0.1.0-draft. The existing ruby kit surface manifest is untouched; the source lifter gets its own ruby-source surface. rake test 113 runs/284 assertions + make test-ruby pass; signature --check pass. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…-signature menagerie (#599) A self-hosted Swift source-language lift kit, mirroring PR #590 (the C# source lifter) and the merged Go/Python/TypeScript/Zig lifters: a Swift program using SwiftSyntax that lifts Swift function definitions into ProvekIt function-contract mementos over a swift:-namespaced operation algebra, plus menagerie/swift-language-signature/, plus a round-trip compiler. Built to the conventions the C#/Go/Java/Python/TS/Zig review rounds settled: namespaced op CIDs, arity_shape on every op spec, a swift:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no swift:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs via the existing per-language canonicalizer (not a rolled-own one), a lift(compile(lift(src))) round-trip test driving the real IR->source compiler path (not just the source-unit byte-copy fast-path), deterministic JSON, version 0.1.0-draft. The existing swift kit surface manifest is untouched; the source lifter gets its own swift-source surface. static checks pass (60 signature JSON files, no swift:unknown/binop/skip); swift build/test couldn't run locally (sandbox blocked ~/.cache/clang + DNS for swift-syntax) — CI verifies. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…ture menagerie A self-hosted PHP source-language lift kit, mirroring PR #590 (the C# source lifter) and the merged Go/Python/TypeScript/Zig lifters: a PHP program using nikic/php-parser that lifts PHP function definitions into ProvekIt function-contract mementos over a php:-namespaced operation algebra, plus menagerie/php-language-signature/, plus a round-trip compiler. Built to the conventions the C#/Go/Java/Python/TS/Zig review rounds settled: namespaced op CIDs, arity_shape on every op spec, a php:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no php:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs via the existing per-language canonicalizer (not a rolled-own one), a lift(compile(lift(src))) round-trip test driving the real IR->source compiler path (not just the source-unit byte-copy fast-path), deterministic JSON, version 0.1.0-draft. The existing php kit surface manifest is untouched; the source lifter gets its own php-source surface. PHP unit tests pass; signature generator deterministic; RPC initialize reports 0.1.0-draft/php-source; composer install couldn't run locally (no composer in sandbox) — CI verifies the php-parser-dependent compiler path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 11, 2026
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…ture menagerie (#600) A self-hosted PHP source-language lift kit, mirroring PR #590 (the C# source lifter) and the merged Go/Python/TypeScript/Zig lifters: a PHP program using nikic/php-parser that lifts PHP function definitions into ProvekIt function-contract mementos over a php:-namespaced operation algebra, plus menagerie/php-language-signature/, plus a round-trip compiler. Built to the conventions the C#/Go/Java/Python/TS/Zig review rounds settled: namespaced op CIDs, arity_shape on every op spec, a php:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no php:unknown/skip catch-all), provably-unique qualified fnName, effects on the canonical Effect wire shapes sorted by sort_key(), BLAKE3/JCS loop CIDs via the existing per-language canonicalizer (not a rolled-own one), a lift(compile(lift(src))) round-trip test driving the real IR->source compiler path (not just the source-unit byte-copy fast-path), deterministic JSON, version 0.1.0-draft. The existing php kit surface manifest is untouched; the source lifter gets its own php-source surface. PHP unit tests pass; signature generator deterministic; RPC initialize reports 0.1.0-draft/php-source; composer install couldn't run locally (no composer in sandbox) — CI verifies the php-parser-dependent compiler path. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…ix Swift unparseable-sig refusal (#602) * chore: align effect sort-key strings to Rust canonical (5:unresolved: not 5:unresolved_call:) Go, TypeScript, Ruby, and Swift lifters emitted "5:unresolved_call:" as the internal sort key for UnresolvedCall effects. The Rust canonical (libprovekit/src/compose.rs Effect::sort_key) uses "5:unresolved:". Zig and C# sort by integer rank so they were already correct. Python was already emitting the correct "5:unresolved:" string. This is a purely internal / cosmetic change: the wire kind emitted in the JSON contract ("unresolved_call") is untouched, so no contract CIDs change. The sort key is used only to canonicalise the order of effects within an EffectSet before signing; aligning it across lifters makes the cross-language order consistent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: add "csharp-source" to KNOWN_SURFACES PR #590 added "csharp" but the C# source lifter's authoring surface is "csharp-source" (matches implementations/csharp/.provekit/lift/csharp-source/). Every other <lang>-source lifter added its own "<lang>-source" entry; this closes the one gap. cargo test -p provekit-cli passes including the known_lists_include_anchor_entries test. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(swift): emit Refusal for unparseable function signatures; fix ThrowStmt API Two changes to SwiftSourceLifter: 1. SwiftDefinitionCollector.visit(FunctionDeclSyntax) previously used `try? functionInfo(for:)` and returned .skipChildren on failure -- silently dropping any function whose signature couldn't be parsed. Changed to a do/catch block that emits a JcsCanonical Refusal (kind: "unparseable-function-signature") and then skips, mirroring the refusal pattern already used for body-level failures in liftSource. A function the lifter can't handle must produce a loud refusal, not disappear from the corpus. 2. ThrowStmtSyntax.expression is non-optional in the pinned swift-syntax version; the old `throwStmt.expression.map(expression) ?? unitConst()` call did not compile. Replaced with `try expression(throwStmt.expression)` which matches the actual API. (Boy-scout fix -- pre-existing build error in the same file.) New test: testRefusesUnparseableFunctionSignatureNotSilentlyDropped -- verifies that generic and async functions (which fail validateSignature) produce refusals and that a valid function in the same source file is still lifted. swift build passes. swift test requires XCTest which is unavailable in the local toolchain; CI's Cross-language conformance gate (macOS swift) verifies the test suite. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…gnature menagerie A self-hosted Java source-language lift kit, mirroring PR #590 (the C# source lifter): a Java program using the JDK compiler API com.sun.source.* that lifts Java function definitions into ProvekIt function-contract mementos over a java:-namespaced operation algebra, plus menagerie/java-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a java:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no java:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing java kit surface manifest is untouched; the source lifter gets its own java-source surface. mvn -pl provekit-lift-java-source -am test pass; jar RPC reports 0.1.0-draft. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 11, 2026
…gnature (#593) * feat(java): add Java source lift kit (self-hosted) + java-language-signature menagerie A self-hosted Java source-language lift kit, mirroring PR #590 (the C# source lifter): a Java program using the JDK compiler API com.sun.source.* that lifts Java function definitions into ProvekIt function-contract mementos over a java:-namespaced operation algebra, plus menagerie/java-language-signature/ cataloging that algebra, plus a round-trip compiler. Built to the conventions #590's review rounds established: namespaced op CIDs, arity_shape on every op spec, a java:source-unit lossless wrapper actually emitted, loud Refusals for unhandled syntax (no java:unknown/skip catch-all), provably-unique fnName, effects on the canonical Effect wire shapes sorted by sort_key(), a lift(compile(lift(src))) round-trip test, deterministic JSON, version 0.1.0-draft. The existing java kit surface manifest is untouched; the source lifter gets its own java-source surface. mvn -pl provekit-lift-java-source -am test pass; jar RPC reports 0.1.0-draft. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(java): consolidate canonicalization into provekit-ir (one BLAKE3 + JCS, not two); code-point key sort Review fix for PR #593: the PR had added a second hand-rolled BLAKE3 + JCS encoder to provekit-ir/Jcs.java when the Java tree already had a vetted one in provekit-claim-envelope (BouncyCastle Blake3Digest, 'mirrors rust/csharp 1:1'), and the new one sorted object keys by UTF-16 code unit (String.compareTo) rather than Unicode code point (spec §7.3 / RFC 8785). Consolidated: moved the BouncyCastle-backed BLAKE3 (Blake3.java) and the code-point-sorted JCS (Jcs.java) into provekit-ir; deleted the duplicate copies from provekit-claim-envelope; updated the Java consumers (claim-envelope, java-self-contracts, realize-java-core, provekit-lift-java-source) to import the IR canonicalization classes; added IR tests pinned to the Rust/b3sum canonical bytes + BLAKE3 vectors, including non-BMP key ordering. mvn -DskipTests=false test passes across the affected + downstream modules. (No menagerie/manifest.yaml change — that file is a destinations: list of runnable exhibits, no *-language-signature catalog belongs there; #593 correctly never added one.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(java): repoint the cross-kit-conformance Java harness at the consolidated canonicalizer location CI follow-up for PR #593: the canonicalizer consolidation (Jcs/Blake3 moved from provekit-claim-envelope into provekit-ir) broke the Cross-language conformance gate two ways: (1) the cross-kit-conformance harness (tools/cross-kit-conformance/src/lib.rs) generates a PkJavaConformance.java whose import still pointed at com.provekit.claimenvelope.Blake3 (now com.provekit.ir.Blake3) -> javac 'cannot find symbol'; (2) the harness's native BridgeV14RoundtripTest check ran 'mvn test -f provekit-claim-envelope/pom.xml' against a stale provekit-ir-0.1.0.jar in ~/.m2 -> NoClassDefFoundError: com/provekit/ir/Jcs at runtime. Fixed both in lib.rs: the generated source imports com.provekit.ir.Blake3, and the BridgeV14 check now runs via the parent reactor with -pl provekit-claim-envelope -am so provekit-ir is built from source; added regression tests for both wiring points. Confirmed Jcs.Value is public static; repo-wide grep for stale claimenvelope.Jcs/Blake3 imports is clean. (mvn test ... -pl provekit-claim-envelope -am -Dtest=BridgeV14RoundtripTest and cargo test -p ... java_ pass; full make test-java/conformance verified via sandbox-adjusted HOME/MAVEN_OPTS since the default ~/.m2 and DNS are blocked locally.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * java-source: fix bug-zoo smoke conformance failure (shaded-jar SecurityException + non-deterministic C# build) Two root causes broke `cargo test -p provekit-bug-zoo --test smoke` on this branch (the smoke dispatches every registered lift surface, including the new java-source one and the existing csharp one): 1. The Java core/source lifter shaded jars bundled BouncyCastle's signed META-INF entries (`*.SF`/`*.DSA`/`*.RSA`), causing a `SecurityException` at runtime when the jar is dispatched. Added shade filters to strip them. 2. The bug-zoo C# lifter invocations were non-deterministic (MSBuild node reuse / shared compilation / parallel build), making `csharp_discover_cli_finds_null_boundary_with_language_lifter` flaky. Pinned `-p:UseSharedCompilation=false -p:BuildInParallel=false --nodeReuse:false`. The canonicalizer consolidation and all pins are untouched. Verified: `cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-bug-zoo --test smoke` 6/6 (debug + release); `mvn -q test -pl provekit-lift-java-source,provekit-ir,provekit-claim-envelope -am` passes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
Adds a C# language lifter in C# with round-trip support (C# source → Provekit IR → C# source), integrated via the provekit RPC protocol. Feature-parity with the JVM bytecode lifter (PR #588) and C11 lifter.
Changes
implementations/csharp/Provekit.Lift.Csharp/— C# lifter using Roslyn:CsharpLifter.cs— parses C# source via Roslyn, extracts method bodies, emits function-contract IRContractEmitter.cs— walks statements/expressions, emitscsharp:-namespaced IR ops (42 ops: all binary, unary, control flow, declarations)CsharpCompiler.cs— lowers IR terms back to C# source (full round-trip)RpcServer.cs— JSON-RPC handler:initialize,lift,compile,shutdownProgram.cs— CLI entry point with--rpcflagimplementations/csharp/Provekit.Lift.Csharp.Tests/— 7 xunit tests (all passing) covering lifting, compilation, round-trip, void refusalmenagerie/csharp-language-signature/— 6 sorts, 42 operations, 3 equations, 5 effect signatures, 5 effect signature catalogsmanifest.tomlpointsprovekit liftto the new C# lifterproject_config.rsadds"csharp"toKNOWN_SURFACESProvekit.slnincludes both new projectsVerification
dotnet test Provekit.Lift.Csharp.Testsprovekit mint language-signatureandprovekit mint algorithmsucceed for all specsSummary by CodeRabbit
New Features
Tests
Chores