Skip to content

Bind Janus invariants L6 and L7 to tests - #20

Merged
NetworkTheoryAppliedResearchInstitute merged 4 commits into
mainfrom
conformance/bind-l6-l7
Oct 3, 2026
Merged

NetworkTheoryAppliedResearchInstitute merged 4 commits into
mainfrom
conformance/bind-l6-l7

Conversation

@csecrestjr

Copy link
Copy Markdown
Contributor

Adds tests for two more Janus invariants, in internal/record.

  • L6 (never edit or delete records): a correction is added as a new entry and the original stays exactly as it was; a secret
    rewrite of history on disk is caught by the record's own proofs; no store, log, ledger, or book in Cloudy has an update or delete function. The "dismissal is annotation" half of L6 is already covered by TestAnswersCloseTheSymmetryBreach in internal/covenant.
  • L7 (no personal info in the shared record): every shared record type holds only hashes, keys, numbers, and times, with no text fields; an address hidden inside a signature or key is rejected.

Both tests were checked by breaking the code on purpose (adding a Memo text field, adding a Delete function) and confirming they fail. CONFORMANCE.md lists the two new bindings.

This brings Cloudy to 4 of 23 delegated invariants bound
(L1, L6, L7, L8).

Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>
Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks Calvin, these are solid tests. I ran the suite locally (all green, race detector clean) and repeated your two break-it checks (Memo string on Entry, Delete on MemStore); both fail as described. I then planted a few more defects and some got through. Two are worth fixing before merge, because the CONFORMANCE.md rows claim more than the tests enforce:

1. L7: an open []byte field passes both subtests. The schema check allows any byte slice on the promise that runtime pins its length, but the runtime subtest only pads Proposer, ProposerSeal, AcceptorSeal and Checkpoint.Signature. Adding Memo []byte to Entry (or Note []byte to FilingCommitment) passes everything. Suggest an explicit allowlist of the byte-slice fields that are ed25519 keys or signatures, so any new one fails until it's added on purpose:

var byteFields = map[string]bool{
	"Entry.Proposer": true, "Entry.Acceptor": true, "Entry.ProposerSeal": true, "Entry.AcceptorSeal": true,
	"Checkpoint.Signature": true, "Countersignature.Witness": true, "Countersignature.Signature": true,
	"FilingCommitment.Filer": true, "FilingCommitment.Signature": true,
	"FilingReceipt.Witness": true, "FilingReceipt.Signature": true,
}

In the reflect.Struct case, reject any []byte field whose TypeName.FieldName isn't listed. I tried this locally: no false positives on current code, and it catches both planted fields.

2. L6: the verb scan skips market.Catalog and techtree.Tree. Both are documented as append-only, but neither name ends in Store/Log/Ledger/Book, so Catalog.Delete or Tree.Remove passes. Adding Catalog|Tree to persistentType catches both, with no false positives today.

Smaller and optional:

  • testL7LengthPinned has no positive control: it still passes if Checkpoint.Verify always returns false. Asserting base.Verify() and cp.Verify(op.pub) before padding would fix that.
  • Entry.Acceptor and the filing and countersignature keys and signatures aren't padded. The test could loop over the allowlist from #1.
  • The verb list is a blocklist, so MemStore.Forget() passes. An allowlist of the exported methods each record type may have would be stronger, and is fine as a follow-up.
  • In CONFORMANCE.md the L6 and L7 rows come after L8; ID order would read better.

Happy to approve once 1 and 2 are in.

Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>
Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>
@csecrestjr

Copy link
Copy Markdown
Contributor Author

Thanks — both fixed.

  1. L7: every []byte field in a commons type must now be named in
    openBytesAllowed (the 11 ed25519 key/signature fields). An unlisted
    one like Entry.Memo []byte fails; a stale list entry also fails.
  2. L6: a type is checked if its name ends in Store/Log/Ledger/Book OR
    its doc says "append-only". market.Catalog and techtree.Tree are
    pinned, so rewording their docs can't drop them out of scope.

Also: the padding test now has passing controls and pads all 11
allowlisted fields; CONFORMANCE.md rows are in ID order. I kept the
verb list as a blocklist for now. An allowlist of permitted verbs is
a bigger change, and I'd suggest it as a follow-up.

Verified by planting Entry.Memo []byte, Catalog.Delete,
Tree.RemoveClaim, and removing Catalog's doc wording: all four fail.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Re-checked after your update: the full suite, vet and race detector are clean, and I re-ran every planted defect from my review plus a few new ones. Both items are fixed: Entry.Memo []byte, FilingCommitment.Note []byte, Catalog.Delete and Tree.Remove all fail now. The new guards hold too. A nested [][]byte, a deleted padding case, a stale allowlist entry, rewording Catalog's doc, and a brand-new type documented append-only with a Purge() method are all caught. The positive controls make the padding test meaningful. Agreed that the verb allowlist is a fine follow-up. Thanks, approving.

@NetworkTheoryAppliedResearchInstitute
NetworkTheoryAppliedResearchInstitute merged commit 8f0591e into main Oct 3, 2026
5 checks passed
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