Repository navigation
docs(recon): as-built identity model, modality evidence, proof obligations and v1 consumer contract - #337
Conversation
|
Caution Review failedThe pull request is closed.
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. |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![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: 7e3d18d5c1
ℹ️ 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".
|
|
||
| == Endpoint and versioning | ||
|
|
||
| * HTTP Axum API listens on \`ApiConfig.host:port\` (defaults \`[::1]:8080\`). |
There was a problem hiding this comment.
When the server binary starts without VERISIM_HOST, main.rs constructs ApiConfig with [::], bypassing the [::1] value from ApiConfig::default; with authentication also disabled by default, this distinction determines whether the API is remotely reachable over IPv6. Describing the operational default as loopback can therefore lead deployments to expose an unauthenticated listener unintentionally.
Useful? React with 👍 / 👎.
| |Route |Current semantics |Important guarantee boundary | ||
| |\`POST /octads\` |Create subject, server-generated ID, 201 |Flattened payload accepted by runtime, *not* the nested published OctadInput schema; default storage is in-memory | ||
| |\`GET /octads/{id}\` |Read current subject, 200 or 404 |Results may be incomplete if a modality store is inconsistent | ||
| |\`PUT /octads/{id}\` |Merge supplied fields into existing subject, 200 or 404 |Not a replace; omissions retain earlier modalities |
There was a problem hiding this comment.
For an existing document, this is not a field-level merge: OctadRequest::to_octad_input turns a title-only request into a replacement document with an empty body, while a body-only request creates no document input and leaves the old document untouched. A consumer following this contract can therefore erase content when attempting to update only the title; describe this asymmetry or require both fields rather than promising that supplied fields are merged.
Useful? React with 👍 / 👎.
| \`graph\`, \`document\`, \`vector\` nested root keys from | ||
| \`connectors/shared/json-schema/octad-input.json\` are **not** runtime | ||
| HTTP request fields. On the base revision, serde ignores them, silently | ||
| losing their values. Proposed PR #334 rejects such payloads instead. |
There was a problem hiding this comment.
A schema-conforming payload such as {"semantic":{"types":[...]}} is also silently discarded on the reviewed revision: OctadRequest has no semantic field and expects top-level types instead. Because this warning enumerates only graph, document, and vector, clients may reasonably infer that the schema's nested semantic object is supported and receive a successful response with their annotations missing.
Useful? React with 👍 / 👎.
| |=== | ||
| |Route |Current semantics |Important guarantee boundary | ||
| |\`POST /octads\` |Create subject, server-generated ID, 201 |Flattened payload accepted by runtime, *not* the nested published OctadInput schema; default storage is in-memory | ||
| |\`GET /octads/{id}\` |Read current subject, 200 or 404 |Results may be incomplete if a modality store is inconsistent |
There was a problem hiding this comment.
The runtime OctadResponse contains only the ID, timestamps/version, has_* flags, and version/provenance counts; it drops the loaded document, embedding, tensor, semantic annotation, graph data, spatial data, and metadata. Consequently GET /octads/{id} cannot actually return the current subject content, even when every store is consistent, so consumers need this response-shape incompatibility called out rather than only a warning about inconsistent stores.
Useful? React with 👍 / 👎.
| |\`GET /search/related/{id}\` |Graph traversal |Graph edges may outlive deleted registry rows | ||
| |\`GET /drift/entity/{id}\` |Per-entity score and computability flags |Score not an identity or authority proof | ||
| |\`POST /normalizer/trigger/{id}\` |Regeneration of selected modality |Side effects and ranked authority; not a guaranteed safe proof-preserving repair | ||
| |\`GET /provenance/{id}\`, \`/verify\` |Hash-chain retrieval and verification |No external signed root or certified actor identity |
There was a problem hiding this comment.
For any existing entity, provenance_verify_handler returns "chain_valid": true without calling verify_chain, including when the entity has no provenance or its persisted chain is corrupt. Only the retrieval handler performs verification, so presenting /verify as hash-chain verification can cause consumers to accept fabricated integrity success.
Useful? React with 👍 / 👎.
| . \`PUT /octads/{id}\`: currently *merge/update*, not replace. Omitted | ||
| modalities remain populated; the temporal snapshot stores the supplied | ||
| update input, not a complete materialized entity. |
There was a problem hiding this comment.
With the persistent feature, a clean partial update followed by restart does not retain the earlier modality status: replay_wal keeps only the last operation payload per entity and rebuilds ModalityStatus solely from that partial OctadInput. The older modality data remains in its physical stores but becomes inaccessible through the registry, so the claim that omitted modalities remain populated is only true before replay and misses a production data-visibility failure distinct from the interrupted-intent bug described below.
Useful? React with 👍 / 👎.
| @@ -0,0 +1,134 @@ | |||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | |||
| = VeriSimDB Consumer Interface Contract — Observed v1 Boundary | |||
There was a problem hiding this comment.
docs/INDEX.adoc explicitly describes itself as the table of contents for everything under docs/, but none of the three documents added here is listed there. The only reference from the handover to the consumer contract is an inline literal rather than an AsciiDoc link, so readers following the repository's official documentation navigation cannot discover this contract or either review document.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cb8890d4a3
ℹ️ 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".
| |429 |Auth rate limiter (when enabled) | ||
| |500 |Store/serialization/runtime error; generic client message for \`ApiError::Internal\` | ||
| |501 |Explicit \`ApiError::NotImplemented\` | ||
| |503 or startup failure |Do not assume readiness; persistent WAL replay failure is non-fatal on \`main\`, proposed PR #333 makes it fatal before listener start |
There was a problem hiding this comment.
This no longer describes the reviewed revision: commit c5e6ac8 is this commit's parent, and its AppState::new_async returns an error when replay_wal fails, preventing the listener from starting; its replay implementation also pairs each intent with its own commit marker. Presenting that behavior as merely proposed can mislead operators about whether ambiguous persistent state will be served, and the other references to PR #333 as unmerged should be updated at the same time.
Useful? React with 👍 / 👎.
| |401 |Authentication middleware enabled, credentials absent/invalid | ||
| |403 |RBAC authorization denial, or federation registration without configured PSK | ||
| |404 |Unknown subject or endpoint | ||
| |413 |Oversized request body, under body-limit middleware | ||
| |422 |Axum JSON deserialization rejection (including unknown input keys after proposed PR #334) | ||
| |429 |Auth rate limiter (when enabled) |
There was a problem hiding this comment.
For deployments of the stock server binary, these authentication-dependent statuses are not merely conditional on configuration: serve() obtains its state from AppState::new_async, which always installs AuthState::default() with enabled = false, while neither ApiConfig nor main.rs exposes auth settings or API-key registration. Consequently operators cannot enable the middleware through the advertised executable at all, so describing 401/RBAC/limiting as available “when enabled” obscures that every request remains unauthenticated unless a separate embedding application constructs and mutates AppState itself.
Useful? React with 👍 / 👎.
| |\`GET /provenance/{id}\`, \`/verify\` |Hash-chain retrieval and verification |No external signed root or certified actor identity | ||
| |\`POST /provenance/{id}/record\` |Append provenance event |Caller-provided actor text must not be treated as attestation | ||
| |\`POST /vcl/execute\` |Subset SELECT, SEARCH, INSERT, DELETE, SHOW, COUNT, EXPLAIN |TypeLL/VCL-UT request is best-effort and never blocks an action if unavailable | ||
| |\`POST /federation/query\` |HTTP query fan-out to registered peers |Not atomic identity federation or independent witness verification |
There was a problem hiding this comment.
This qualifier understates the observed behavior when TypeLL is reachable: vcl_execute_handler executes INSERT or DELETE before merely attaching the returned safety metadata, and it also proceeds when the checker returns a non-success status. Thus no TypeLL verdict—including a level indicating an unsafe transition—can block the action, not just checker unavailability; consumers relying on a live validator as an admission gate can still perform rejected mutations.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bdf8d68ab9
ℹ️ 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".
| \`OctadInput\`. The coordinator generates an ID and logs intent, locks | ||
| requested modalities, writes stores sequentially, appends a temporal | ||
| version, updates the registry, then emits a commit marker. |
There was a problem hiding this comment.
With the default non-persistent build described immediately above, InMemoryOctadStore::new leaves wal as None, so the pre-write wal_append and commit-marker calls are no-ops; only AppState::new_async under the persistent feature invokes with_wal. Stating unconditionally that every POST logs an intent and emits a commit marker can make operators of the default build assume recovery evidence exists when it does not, so this lifecycle step should be explicitly scoped to persistent deployments.
Useful? React with 👍 / 👎.
| * GraphQL: \`POST /graphql\` and \`GET /graphiql\`; gRPC Tonic service on | ||
| separate configurable port, default 50051. Authentication of gRPC is |
There was a problem hiding this comment.
In deployments of the stock binary with both VERISIM_TLS_CERT and VERISIM_TLS_KEY set, main.rs calls serve_tls, and that function starts only the Axum TLS listener; the configurable Tonic server is started exclusively by the non-TLS serve path. Thus clients following this contract will find no service on port 50051 in an otherwise supported TLS configuration, so the endpoint description should document this exception rather than presenting gRPC as uniformly available.
Useful? React with 👍 / 👎.
| |Route |Current semantics |Important guarantee boundary | ||
| |\`POST /octads\` |Create subject, server-generated ID, 201 |Flattened payload accepted by runtime, *not* the nested published OctadInput schema; default storage is in-memory | ||
| |\`GET /octads/{id}\` |Read current subject, 200 or 404 |Results may be incomplete if a modality store is inconsistent | ||
| |\`PUT /octads/{id}\` |Merge supplied fields into existing subject, 200 or 404 |Not a replace; omissions retain earlier modalities |
There was a problem hiding this comment.
When an update omits an already-populated modality, storage retains it in modality_status, but InMemoryOctadStore::update returns an Octad containing only modalities written by that request, and OctadResponse::from derives every has_* flag from those optional payload fields. A document-only update to an entity that already has a vector therefore returns has_vector: false even though a subsequent GET reports it as present; consumers using the PUT response as the current merged state need this inconsistency called out.
Useful? React with 👍 / 👎.
|
|
||
| * PR #333: committed-intent WAL replay, fail closed on ambiguity. | ||
| * PR #334: refuse silently dropped Octad JSON fields. | ||
| * PR #335: unrelated strict-Clippy baseline fixes. |
There was a problem hiding this comment.
The reviewed commit's immediate parent is 8af7bde, whose subject is the landed fix(ci): remove pre-existing unused RAM promotion fields (#335). Listing #335 under changes still under review and then stating that none of them is merged gives readers an incorrect CI-baseline status and may prompt duplicate remediation work; record it as landed rather than proposed.
Useful? React with 👍 / 👎.
| |\`GET /drift/entity/{id}\` |Per-entity score and computability flags |Score not an identity or authority proof | ||
| |\`POST /normalizer/trigger/{id}\` |Regeneration of selected modality |Side effects and ranked authority; not a guaranteed safe proof-preserving repair | ||
| |\`GET /provenance/{id}\`, \`/verify\` |Hash-chain retrieval and verification |No external signed root or certified actor identity | ||
| |\`POST /provenance/{id}/record\` |Append provenance event |Caller-provided actor text must not be treated as attestation |
There was a problem hiding this comment.
For POST /provenance/{id}/record with a well-formed but nonexistent ID, OctadStore::update returns OctadError::NotFound, but this handler maps every store error to ApiError::Internal; the observed response is therefore a generic 500 rather than the 404 that the contract associates with an unknown subject. Clients may otherwise treat this permanent missing-entity condition as a retryable server failure, so the route-specific behavior should be stated until the handler maps NotFound correctly.
Useful? React with 👍 / 👎.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8ab971dc4a
ℹ️ 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".
| HTTP request fields. On the base revision, serde ignores them, silently | ||
| losing their values. Proposed PR #334 rejects such payloads instead. |
There was a problem hiding this comment.
PR #334 is already the immediate parent of this revision, where OctadRequest has #[serde(deny_unknown_fields)] and nested schema payloads return 422. Presenting rejection as merely proposed leaves consumers unable to determine the actual wire behavior and incorrectly suggests that current requests may succeed while losing values; document rejection as the observed behavior and mark #334 as landed.
Useful? React with 👍 / 👎.
| The repository's \`docs/proof-debt.adoc\` reports 13 declared Coq | ||
| \`Axiom\` instances, zero \`Admitted\` and an assumption-whitelist build gate. | ||
| That is a useful audit inventory, not proof that the Rust implementation |
There was a problem hiding this comment.
The formal corpus at this revision declares 11 Axiom commands, not 13: six in Drift.v, two in Normalizer.v, and one each in PlannerSemantic.v, Provenance.v, and WAL.v. The referenced proof-debt ledger still counts two discharged optimize_is_permutation assumptions even though Planner.v now proves that result and PlannerSemantic.v imports it, so presenting the ledger as a useful current inventory gives proof reviewers the wrong trusted-base count; report 11 or explicitly identify the ledger as stale.
Useful? React with 👍 / 👎.
Independent code-grounded reconnaissance as of main
5876bc67e8962e3b276fb0161664e0b3a420a64c.Adds three review documents:
docs/reviews/2026-10-29-verisimdb-as-built-recon.adoc— source-derived architecture, conceptual ER, eight-modality/persistence matrix, actual lifecycle, P0/P1/P2 discrepancy register, tests and formal proof obligations, independent Mathesis/QuandleDB/JanusKey/Marches reuse, prioritized engineering programme.docs/consumer-interface-contract-v1-observed.adoc— actual flatten-vs-nested HTTP ABI, operations, HTTP statuses, feature/configuration guarantees and explicit non-guarantees.docs/reviews/2026-10-29-hypatia-verified-handover.adoc— only verified downstream integration facts.No rewrite of the Octad schema; accepted generic term modality profile distinguished from modality set and consonance subject. References separate code fixes #333, #334, #335, #336. Makes no soundness claims beyond observed source/test status. No data mutation.