Skip to content

feat(lift): add OpenAPI/Swagger/Protobuf lift adapter#225

Merged
TSavo merged 5 commits into
mainfrom
feat/lift-openapi-protobuf
May 4, 2026
Merged

feat(lift): add OpenAPI/Swagger/Protobuf lift adapter#225
TSavo merged 5 commits into
mainfrom
feat/lift-openapi-protobuf

Conversation

@TSavo
Copy link
Copy Markdown
Owner

@TSavo TSavo commented May 4, 2026

Summary

New crate provekit-lift-openapi that speaks the provekit-lift/1 RPC plugin protocol and emits Provekit IR contracts from:

  • OpenAPI 3.x specs (YAML/JSON)
  • Protobuf .proto files

The adapter produces ir-document responses — raw Declaration[] IR. The Rust CLI handles minting, signing, and .proof bundling downstream.

Surfaces

surface Input What it emits
openapi OpenAPI 3.x YAML/JSON Per-endpoint response/request contracts, parameter contracts, schema contracts
swagger Same as openapi Identical behavior
protobuf .proto files Per-message type contracts, per-RPC request/response contracts

Constraint mapping (OpenAPI → IR)

Schema constraint IR atomic predicate
minimum: 1 ≥(field, 1)
maximum: 100 ≤(field, 100)
minLength: 1 ≥(length(field), 1)
pattern: "..." matches(field, "...")
format: email email(field)
required: [x] not_null(x)
enum: [a,b] member(field, Set(a,b))

Tests

7 tests, all passing
  openapi::tests::lifts_petstore_yaml               ✓
  openapi::tests::extracts_integer_constraints       ✓
  openapi::tests::extracts_string_constraints        ✓
  openapi::tests::extracts_enum_constraints          ✓
  protobuf::tests::lifts_user_proto                  ✓
  protobuf::tests::parses_user_message_fields        ✓
  protobuf::tests::parses_rpc_definitions            ✓

Files

File Purpose
src/main.rs RPC server (NDJSON over stdio, initialize/lift/shutdown)
src/openapi.rs OpenAPI 3.x spec parser + IR emitter
src/protobuf.rs .proto file parser + IR emitter
src/ir_builder.rs IR formula construction helpers
src/types.rs Declaration, Diagnostics types
manifest.toml Plugin manifest for ~/.config/provekit/lift/openapi/ discovery

Summary by CodeRabbit

  • New Features
    • Added OpenAPI and Swagger specification lifting to convert API definitions into formal contract representations with extracted constraints (nullability, value ranges, patterns, enumerations, type constraints).
    • Extended support to Protobuf format with automatic message and RPC contract generation.

New crate  speaks the provekit-lift/1 RPC protocol
and emits IR contracts from OpenAPI 3.x specs and .proto files.

Surfaces: openapi, swagger, protobuf
Response shape: ir-document (IR declarations, Rust CLI handles minting)
Tests: 7 passing (OpenAPI + protobuf schema parsing, RPC round-trip)
Copilot AI review requested due to automatic review settings May 4, 2026 05:14
@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 4, 2026

Warning

Rate limit exceeded

@TSavo has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 35 minutes and 46 seconds before requesting another review.

To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

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 configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 1b32977e-b61b-4ee6-8b7d-1972fd050952

📥 Commits

Reviewing files that changed from the base of the PR and between 671cd8d and da28e81.

📒 Files selected for processing (10)
  • implementations/c/provekit-ir/Makefile
  • implementations/c/provekit-ir/tests/test_runner.c
  • implementations/rust/provekit-cli/src/cmd_mint.rs
  • implementations/rust/provekit-lift-openapi/Cargo.toml
  • implementations/rust/provekit-lift-openapi/src/annotate.rs
  • implementations/rust/provekit-lift-openapi/src/main.rs
  • implementations/typescript/src/lift/adapters/provekit-annotations.ts
  • implementations/typescript/src/lift/cli.ts
  • implementations/typescript/src/lift/index.ts
  • implementations/typescript/src/lift/types.ts

Walkthrough

A new Rust binary crate provekit-lift-openapi is added to the workspace, implementing a JSON-RPC 2.0 service that lifts OpenAPI/Swagger specifications and Protocol Buffer definitions into an internal representation (IR) used for proof verification.

Changes

OpenAPI & Protobuf Lifting Service

Layer / File(s) Summary
Workspace & Package Configuration
implementations/rust/Cargo.toml, implementations/rust/provekit-lift-openapi/Cargo.toml
New workspace member provekit-lift-openapi is registered. Binary crate is configured with dependencies: serde, serde_json, serde_yaml, thiserror, and provekit-canonicalizer.
Service Manifest & Type Definitions
implementations/rust/provekit-lift-openapi/manifest.toml, src/types.rs
Service metadata declares support for openapi, swagger, protobuf surfaces and IR v1.1.0. Core types (Diagnostics, Declaration, ContractDecl, BridgeDecl) define the output structure for lifted declarations.
IR Construction Helpers
src/ir_builder.rs
Factory functions construct JSON-encoded IR expressions: sorts (int_sort, string_sort, etc.), constants, logical operators (and, or, not, implies), quantifiers (forall, exists), and domain-specific predicates (matches, is_null, length_of, member_of, contract_with_pre, contract_with_post).
Input Format Parsing & Lifting
src/openapi.rs, src/protobuf.rs
lift_spec parses OpenAPI/Swagger YAML/JSON, resolves $ref schemas, translates JSON Schema keywords into constraint formulas, and generates contracts from requestBody/responses/parameters. lift_proto parses .proto syntax, extracts message fields and RPC definitions, and converts them into contracts with type and nullability constraints.
RPC Dispatch & Integration
src/main.rs
JSON-RPC 2.0 dispatcher reads newline-delimited requests, routes initialize, lift, and shutdown methods, orchestrates lifting by calling openapi::lift_spec or protobuf::lift_proto, accumulates diagnostics, and writes JSON-RPC responses to stdout.

Sequence Diagram

sequenceDiagram
    participant Client
    participant RpcDispatcher as Dispatcher<br/>(main.rs)
    participant Lifter as Lifter<br/>(openapi/protobuf)
    participant Parser as Parser
    participant IRBuilder as IR Builder
    participant Output as Response

    Client->>RpcDispatcher: JSON-RPC lift request<br/>(surface, source_paths)
    RpcDispatcher->>Lifter: Route to openapi::lift_spec<br/>or protobuf::lift_proto
    Lifter->>Parser: Parse spec/proto file
    Parser->>Parser: Extract schemas, operations,<br/>messages, RPCs
    Lifter->>IRBuilder: Build constraints<br/>(schema → IR formulas)
    IRBuilder->>IRBuilder: Combine operators,<br/>quantifiers, predicates
    IRBuilder-->>Lifter: Return IR Values
    Lifter-->>RpcDispatcher: Return Declarations<br/>+ Diagnostics
    RpcDispatcher->>Output: Serialize to JSON-RPC<br/>result + diagnostics
    Output-->>Client: IR document response
Loading

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~45 minutes

Possibly related PRs

Poem

🐰 A new lifter hops into view,
OpenAPI specs to IR, shiny and new!
Proto messages parsed with care,
Constraints and formulas float through the air—
The proof-kit grows, hopping everywhere! ✨

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name Status Explanation Resolution
Docstring Coverage ⚠️ Warning Docstring coverage is 16.67% which is insufficient. The required threshold is 80.00%. Write docstrings for the functions missing them to satisfy the coverage threshold.
✅ Passed checks (4 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title accurately summarizes the main change: adding a new OpenAPI/Swagger/Protobuf lift adapter crate with its implementation, which is the core purpose of this PR.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/lift-openapi-protobuf

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share
Review rate limit: 0/1 reviews remaining, refill in 35 minutes and 46 seconds.

Comment @coderabbitai help to get the list of available commands and usage tips.

Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 671cd8dd13

ℹ️ 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".

Comment on lines +455 to +456
let prop_schema = resolve_schema_ref(prop_schema);
let field =
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Resolve $ref schemas before recursing into property constraints

When a property schema is a $ref, this path converts it into a raw string value and then feeds it into schema_to_constraints_on_value, which treats it as unconstrained. As a result, nested component schemas (for object properties, array items, etc.) silently lose their required/type/range constraints, so the emitted contract is materially weaker than the OpenAPI spec for any referenced nested type.

Useful? React with 👍 / 👎.

Comment on lines +343 to +346
operands.push(ir_builder::gte(
value.clone(),
ir_builder::const_int(min as i64),
));
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Preserve fractional bounds for number minimum/maximum

The inclusive bound path casts numeric limits to i64, so decimal constraints are truncated (for example minimum: 0.5 becomes >= 0). This changes the intended semantics of OpenAPI number schemas and can admit values that should be rejected, producing incorrect IR constraints.

Useful? React with 👍 / 👎.

Comment on lines +492 to +495
let response_type = rest[idx + 11..]
.trim_start_matches("stream ")
.trim_end_matches(')')
.trim()
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Strip RPC block suffix from parsed response types

Proto3 allows RPC declarations with an option block (rpc ... returns (...) { ... }), but this parser only trims a trailing ) and leaves ") {" attached to the response type. In those files, generated contracts use malformed type names (e.g. has_type(x, "MyResp) {")), so RPC request/response contracts no longer match actual message types.

Useful? React with 👍 / 👎.

Copy link
Copy Markdown

@coderabbitai coderabbitai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 2

🧹 Nitpick comments (5)
implementations/rust/provekit-lift-openapi/src/protobuf.rs (2)

30-37: ⚡ Quick win

Empty loop body is dead code.

This loop iterates over filtered messages but performs no action. This appears to be placeholder code for enum handling that was never completed. Consider removing it or implementing the intended functionality.

♻️ Remove dead code or add TODO
-    for _enum_def in parser.messages.iter().filter_map(|m| {
-        if m.fields.is_empty() && !m.nested.is_empty() {
-            Some(m)
-        } else {
-            None
-        }
-    }) {
-    }
+    // TODO: Implement enum contract generation from parser.enums
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/protobuf.rs` around lines 30 -
37, The for loop iterating parser.messages.filter_map(|m| ...) has an empty body
and is dead code; either remove this loop entirely or implement the intended
enum handling for messages where m.fields.is_empty() && !m.nested.is_empty().
Locate the loop (the iterator over parser.messages and the variable _enum_def)
in protobuf.rs and either delete it or replace it with the actual processing
logic (e.g., handling enum conversions/registration for _enum_def) or at minimum
add a clear TODO comment indicating the intended work to avoid silent no-ops.

101-102: 💤 Low value

Unused variable _typ suggests incomplete implementation.

The proto-to-IR sort conversion result is computed but never used. Either remove it or use it to add type sort information to the generated constraints.

🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/protobuf.rs` around lines 101
- 102, The unused `_typ` indicates the proto-to-IR sort was computed but not
applied; either remove the call or use its result to annotate the generated IR
for the field. Replace `_typ` with a meaningful name (e.g., `typ`) and pass it
into the constraint/IR construction that uses `field_var` (created by
`ir_builder::field_access`) so the field is declared/checked with the correct
sort returned by `proto_to_ir_sort`; if you choose not to use it, remove the
`proto_to_ir_sort(&field.field_type)` call entirely to avoid dead code.
implementations/rust/provekit-lift-openapi/src/types.rs (1)

64-83: 💤 Low value

Consider using serde's tagged enum representation.

The manual insertion of the "kind" field could be simplified by using serde's #[serde(tag = "kind")] attribute on the Declaration enum. This would also avoid the edge case where unwrap_or_default() silently produces an empty object on serialization failure.

♻️ Alternative approach using serde's tagged enum
#[derive(Debug, Clone, Serialize)]
#[serde(tag = "kind", rename_all = "lowercase")]
pub enum Declaration {
    Contract(ContractDecl),
    Bridge(BridgeDecl),
}

impl Declaration {
    pub fn to_json(&self) -> Value {
        serde_json::to_value(self).unwrap_or(Value::Null)
    }
}
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/types.rs` around lines 64 -
83, Replace the manual JSON-kind injection in Declaration::to_json by deriving
Serialize on the Declaration enum and using serde's internally-tagged
representation: add #[derive(Serialize)] and #[serde(tag = "kind", rename_all =
"lowercase")] to the Declaration enum (which contains Contract(ContractDecl) and
Bridge(BridgeDecl)), then simplify Declaration::to_json to serialize self
directly (avoid unwrap_or_default and return a safe fallback like Value::Null on
error); this removes the manual map insertion and the unwrap_or_default edge
case.
implementations/rust/provekit-lift-openapi/src/openapi.rs (1)

6-6: 💤 Low value

BridgeDecl is imported but never instantiated.

The import suggests bridge declarations were planned but lift_schema_to_contract always returns None for the bridge (line 210). Consider removing the unused import or completing the bridge implementation.

🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/openapi.rs` at line 6, The
import of BridgeDecl is unused because lift_schema_to_contract currently never
constructs a bridge (it always returns None for the bridge); either remove
BridgeDecl from the use statement or implement bridge construction in
lift_schema_to_contract: locate lift_schema_to_contract and either remove
BridgeDecl from the use crate::types list or create and return a proper
BridgeDecl instance (populating its required fields) alongside the
ContractDecl/Declaration so BridgeDecl is actually instantiated and used.
implementations/rust/provekit-lift-openapi/Cargo.toml (1)

18-18: Remove unused dependency: provekit-canonicalizer.

This dependency is declared in Cargo.toml but is not imported or used anywhere in the crate's source code. Either remove it or address the incomplete implementation.

🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/Cargo.toml` at line 18, The
Cargo.toml entry provekit-canonicalizer = { path = "../provekit-canonicalizer" }
is unused; remove this dependency from the crate's Cargo.toml to eliminate the
unused dependency warning (or, if the crate is meant to use it, add the actual
imports/usages referencing types or functions from the provekit-canonicalizer
crate in source files such as lib.rs or main.rs and update Cargo.toml
accordingly). Ensure Cargo.toml no longer lists provekit-canonicalizer unless
corresponding code (use statements and API calls from provekit-canonicalizer) is
added to the project.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@implementations/rust/provekit-lift-openapi/src/ir_builder.rs`:
- Around line 29-31: The current const_real function silently maps NaN/Infinity
to 0 due to serde_json::Number::from_f64(...).unwrap_or(...); update const_real
to explicitly handle non-finite floats: change its signature to return a
Result<Value, Error> (or Result<Value, String>) and check value.is_finite()
inside const_real; if finite, construct the Number via
serde_json::Number::from_f64 and return Ok(json!(...)) using real_sort(),
otherwise return an Err with a clear message including the offending value (or
alternatively encode a special JSON representation for non-finite values) so
callers of const_real can handle/report invalid IR inputs instead of silently
using 0.

In `@implementations/rust/provekit-lift-openapi/src/openapi.rs`:
- Around line 167-169: The fallback currently returns Some(body) when body
contains "application/json", which is a no-op; change the logic so that if body
lacks "content" you extract the "application/json" entry itself (e.g., replace
the or_else closure to return body.get("application/json") instead of
Some(body)) so the variable content holds the actual content object; update the
resolution around the content and body variables in openapi.rs (the expression
that sets content) to return the JSON content value under the "application/json"
key rather than the whole body.

---

Nitpick comments:
In `@implementations/rust/provekit-lift-openapi/Cargo.toml`:
- Line 18: The Cargo.toml entry provekit-canonicalizer = { path =
"../provekit-canonicalizer" } is unused; remove this dependency from the crate's
Cargo.toml to eliminate the unused dependency warning (or, if the crate is meant
to use it, add the actual imports/usages referencing types or functions from the
provekit-canonicalizer crate in source files such as lib.rs or main.rs and
update Cargo.toml accordingly). Ensure Cargo.toml no longer lists
provekit-canonicalizer unless corresponding code (use statements and API calls
from provekit-canonicalizer) is added to the project.

In `@implementations/rust/provekit-lift-openapi/src/openapi.rs`:
- Line 6: The import of BridgeDecl is unused because lift_schema_to_contract
currently never constructs a bridge (it always returns None for the bridge);
either remove BridgeDecl from the use statement or implement bridge construction
in lift_schema_to_contract: locate lift_schema_to_contract and either remove
BridgeDecl from the use crate::types list or create and return a proper
BridgeDecl instance (populating its required fields) alongside the
ContractDecl/Declaration so BridgeDecl is actually instantiated and used.

In `@implementations/rust/provekit-lift-openapi/src/protobuf.rs`:
- Around line 30-37: The for loop iterating parser.messages.filter_map(|m| ...)
has an empty body and is dead code; either remove this loop entirely or
implement the intended enum handling for messages where m.fields.is_empty() &&
!m.nested.is_empty(). Locate the loop (the iterator over parser.messages and the
variable _enum_def) in protobuf.rs and either delete it or replace it with the
actual processing logic (e.g., handling enum conversions/registration for
_enum_def) or at minimum add a clear TODO comment indicating the intended work
to avoid silent no-ops.
- Around line 101-102: The unused `_typ` indicates the proto-to-IR sort was
computed but not applied; either remove the call or use its result to annotate
the generated IR for the field. Replace `_typ` with a meaningful name (e.g.,
`typ`) and pass it into the constraint/IR construction that uses `field_var`
(created by `ir_builder::field_access`) so the field is declared/checked with
the correct sort returned by `proto_to_ir_sort`; if you choose not to use it,
remove the `proto_to_ir_sort(&field.field_type)` call entirely to avoid dead
code.

In `@implementations/rust/provekit-lift-openapi/src/types.rs`:
- Around line 64-83: Replace the manual JSON-kind injection in
Declaration::to_json by deriving Serialize on the Declaration enum and using
serde's internally-tagged representation: add #[derive(Serialize)] and
#[serde(tag = "kind", rename_all = "lowercase")] to the Declaration enum (which
contains Contract(ContractDecl) and Bridge(BridgeDecl)), then simplify
Declaration::to_json to serialize self directly (avoid unwrap_or_default and
return a safe fallback like Value::Null on error); this removes the manual map
insertion and the unwrap_or_default edge case.
🪄 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: b64bf3ba-5b99-4d3f-b4cd-b92dfa8d1f9a

📥 Commits

Reviewing files that changed from the base of the PR and between f6907d2 and 671cd8d.

⛔ Files ignored due to path filters (1)
  • implementations/rust/Cargo.lock is excluded by !**/*.lock
📒 Files selected for processing (8)
  • implementations/rust/Cargo.toml
  • implementations/rust/provekit-lift-openapi/Cargo.toml
  • implementations/rust/provekit-lift-openapi/manifest.toml
  • implementations/rust/provekit-lift-openapi/src/ir_builder.rs
  • implementations/rust/provekit-lift-openapi/src/main.rs
  • implementations/rust/provekit-lift-openapi/src/openapi.rs
  • implementations/rust/provekit-lift-openapi/src/protobuf.rs
  • implementations/rust/provekit-lift-openapi/src/types.rs

Comment on lines +29 to +31
pub fn const_real(value: f64) -> Value {
json!({ "kind": "const", "value": Value::Number(serde_json::Number::from_f64(value).unwrap_or(serde_json::Number::from(0))), "sort": real_sort() })
}
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

NaN and Infinity values silently become 0.

serde_json::Number::from_f64() returns None for NaN and Infinity values. The unwrap_or fallback to 0 silently produces incorrect IR. Consider returning an error or using a special representation for non-finite values.

🛡️ Proposed fix to handle non-finite floats explicitly
 pub fn const_real(value: f64) -> Value {
-    json!({ "kind": "const", "value": Value::Number(serde_json::Number::from_f64(value).unwrap_or(serde_json::Number::from(0))), "sort": real_sort() })
+    let num = if value.is_finite() {
+        Value::Number(serde_json::Number::from_f64(value).unwrap())
+    } else {
+        // Represent non-finite values as strings for downstream handling
+        Value::String(value.to_string())
+    };
+    json!({ "kind": "const", "value": num, "sort": real_sort() })
 }
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/ir_builder.rs` around lines 29
- 31, The current const_real function silently maps NaN/Infinity to 0 due to
serde_json::Number::from_f64(...).unwrap_or(...); update const_real to
explicitly handle non-finite floats: change its signature to return a
Result<Value, Error> (or Result<Value, String>) and check value.is_finite()
inside const_real; if finite, construct the Number via
serde_json::Number::from_f64 and return Ok(json!(...)) using real_sort(),
otherwise return an Err with a clear message including the offending value (or
alternatively encode a special JSON representation for non-finite values) so
callers of const_real can handle/report invalid IR inputs instead of silently
using 0.

Comment on lines +167 to +169
let content = body
.get("content")
.or_else(|| body.get("application/json").and_then(|_| Some(body)));
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Confusing fallback logic in content resolution.

The or_else clause returns Some(body) unchanged if body contains "application/json", which doesn't extract the actual content. This appears to be a no-op fallback that may not behave as intended.

🔍 Suggested simplification
         let content = body
             .get("content")
-            .or_else(|| body.get("application/json").and_then(|_| Some(body)));
+            .or_else(|| Some(body)); // Fall back to treating body itself as schema

Or if the intent was to check for inline application/json keys at body level, the logic needs rework.

📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
let content = body
.get("content")
.or_else(|| body.get("application/json").and_then(|_| Some(body)));
let content = body
.get("content")
.or_else(|| Some(body)); // Fall back to treating body itself as schema
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@implementations/rust/provekit-lift-openapi/src/openapi.rs` around lines 167 -
169, The fallback currently returns Some(body) when body contains
"application/json", which is a no-op; change the logic so that if body lacks
"content" you extract the "application/json" entry itself (e.g., replace the
or_else closure to return body.get("application/json") instead of Some(body)) so
the variable content holds the actual content object; update the resolution
around the content and body variables in openapi.rs (the expression that sets
content) to return the JSON content value under the "application/json" key
rather than the whole body.

Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Adds a new Rust workspace member, provekit-lift-openapi, intended to act as a provekit-lift/1 adapter that turns OpenAPI/Swagger and Protobuf inputs into Provekit IR for the broader multi-language lift pipeline.

Changes:

  • Adds a new NDJSON/JSON-RPC lift plugin binary for openapi, swagger, and protobuf surfaces.
  • Implements OpenAPI schema/parameter lifting and a handwritten Protobuf parser that emit IR declarations plus diagnostics.
  • Wires the new crate into the Rust workspace and adds a plugin manifest/dependency lockfile entries.

Reviewed changes

Copilot reviewed 8 out of 9 changed files in this pull request and generated 19 comments.

Show a summary per file
File Description
implementations/rust/provekit-lift-openapi/src/types.rs Defines diagnostics and declaration JSON shapes for emitted IR.
implementations/rust/provekit-lift-openapi/src/protobuf.rs Adds .proto parsing and Protobuf-to-IR contract generation logic plus unit tests.
implementations/rust/provekit-lift-openapi/src/openapi.rs Adds OpenAPI/Swagger parsing, schema constraint extraction, and IR emission plus unit tests.
implementations/rust/provekit-lift-openapi/src/main.rs Implements the lift-plugin RPC server entrypoint and request dispatch.
implementations/rust/provekit-lift-openapi/src/ir_builder.rs Adds JSON helpers for constructing IR terms, formulas, and declaration fragments.
implementations/rust/provekit-lift-openapi/manifest.toml Declares plugin metadata/capabilities for lift-plugin discovery.
implementations/rust/provekit-lift-openapi/Cargo.toml Registers the new crate binary and its dependencies.
implementations/rust/Cargo.toml Adds the new adapter crate to the Rust workspace members list.
implementations/rust/Cargo.lock Locks the new crate and its added dependencies (serde_yaml, unsafe-libyaml).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment on lines +273 to +275
if let Some(ref_path) = schema.get("$ref").and_then(|v| v.as_str()) {
return Value::String(ref_path.to_string());
}
Comment on lines +360 to +363
operands.push(ir_builder::lte(
value.clone(),
ir_builder::const_int(max as i64),
));
Comment on lines +86 to +87
let route_slug =
slugify(&format!("{spec_prefix}-{method}-{op_id}"));
Comment on lines +104 to +108
match field.label {
FieldLabel::Required => {
operands.push(ir_builder::not_null(field_var.clone()));
}
FieldLabel::Optional => {}
Comment on lines +22 to +27
for msg in &parser.messages {
let name = format!("proto-{}", slugify(&msg.name));
if let Some(contract) = message_to_contract(&name, msg) {
decls.push(Declaration::Contract(contract));
diagnostics.push(format!("lifted message {}", msg.name));
}
Comment on lines +142 to +153
out_binding: "out".to_string(),
pre: None,
post: Some(ir_builder::atomic("true", vec![])),
inv: None,
});
}

let post = ir_builder::forall_ref("x", ir_builder::and(operands));

Some(ContractDecl {
name: name.to_string(),
out_binding: "out".to_string(),
Comment on lines +151 to +153
"kind": "ir-document",
"ir": ir,
"diagnostics": diagnostics.messages
let mut operands = Vec::new();

for param in params {
let name = param.get("name").and_then(|v| v.as_str())?;
Comment on lines +126 to +130
if let Some(parameters) = operation.get("parameters") {
if let Value::Array(params) = parameters {
let param_constraints =
self.lift_parameters(params);
if let Some(formula) = param_constraints {
Comment on lines +487 to +491
let single_line = format!("{}", line.trim_end_matches(';'));

if let Some(rest) = single_line.strip_prefix(&format!("rpc {} (", name)) {
if let Some(idx) = rest.find(") returns (") {
let request_type = rest[..idx].trim_start_matches("stream ").to_string();
TSavo added 3 commits May 3, 2026 22:56
The lift-plugin protocol defines three response shapes:
(a) ir-document, (b) signed-mementos, (c) proof-envelope.
The CLI previously only supported (c) proof-envelope.

This adds support for (a) ir-document: the CLI now mints each
IR contract declaration (JCS -> BLAKE3 -> Ed25519 -> CBOR bundle)
and writes the resulting .proof file.

Also: lift-openapi adapter now auto-discovers .yaml/.yml/.json
(OpenAPI) and .proto (Protobuf) files when source_paths is ['.'],
matching the pattern used by other self-contracts lifters.
…to generated clients

The --annotate mode reads an OpenAPI spec and a directory of generated
client code, then:
1. Matches generated functions to OpenAPI operations via name patterns
2. Injects @provekit.target + @provekit.post annotations
3. Writes provekit-contracts.ts reference file

Supports TypeScript, Go, and Rust generated code syntax.
When lifted by the per-language adapter, these annotations connect
to the OpenAPI .proof contracts, enabling the linker to produce
red squigglies for assumption violations.
…tions

New adapter reads @provekit.target and @provekit.post JSDoc comments
injected by the annotate mode of provekit-lift-openapi. Each annotated
function becomes a ContractDecl with a post-condition from the OpenAPI
spec, plus a targetContract field for cross-kit bridge linking.

Extended ContractDecl with optional targetContract field.
Registered in liftPath() pipeline alongside zod, fast-check, etc.
When the provekit-annotations adapter finds @provekit.target on a
function, mintProof() now generates a CallEdgeDecl with the source
contract CID and the target symbol. Call edges are included in the
RPC proof-envelope response for linkerd consumption.

Also: RPC lift mode now reads source_paths from the request params,
allowing the lifter to target specific directories.
@TSavo TSavo merged commit 2fdbc40 into main May 4, 2026
4 checks passed
ConstCorrectness pushed a commit to ConstCorrectness/provekit that referenced this pull request May 6, 2026
ConstCorrectness pushed a commit to ConstCorrectness/provekit that referenced this pull request May 6, 2026
docs: replace phantom issue refs (TSavo#222-TSavo#225) with real bridge-IR migration issues per kit
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants