Repository navigation
Bind Janus invariants L6 and L7 to tests - #20
Conversation
Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>
Signed-off-by: Calvin Secrest <dev@calvinsecrest.com>
NetworkTheoryAppliedResearchInstitute
left a comment
There was a problem hiding this comment.
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:
testL7LengthPinnedhas no positive control: it still passes ifCheckpoint.Verifyalways returns false. Assertingbase.Verify()andcp.Verify(op.pub)before padding would fix that.Entry.Acceptorand 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>
|
Thanks — both fixed.
Also: the padding test now has passing controls and pads all 11 Verified by planting Entry.Memo []byte, Catalog.Delete, |
NetworkTheoryAppliedResearchInstitute
left a comment
There was a problem hiding this comment.
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.
Adds tests for two more Janus invariants, in internal/record.
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.
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).