Notarizing documentation
Writing specifications for notarizing
Developer preview. Not yet production ready. This page is rendered from docs/writing-specs.md of the Notarizing repository at revision d23579e737f9d1e16e07b3c6b21a51282d64027e. It describes the behavior of that revision.
Contents
This guide tells you how to write an OpenSpec change that notarizing reads well. Notarizing reads only explicit identities and links. It never mines prose. A requirement without the lines of this guide is still imported, but it has no stable identity and no relationships.
The rules come from n0-decisions.md section 7
and the OpenSpec adapter (internal/adapters/openspec). Each output in this guide comes from
a run of the binary. The test internal/cli/writing_specs_test.go imports the example change
and makes each documented mistake. The test fails when the output of the product and the
text of this guide differ.
What notarizing reads
notarizing change import reads one exact commit. It reads only these files:
openspec/specs/<capability>/spec.md: the accepted requirements;openspec/specs/<capability>/declarations.md: accepted declarations;openspec/changes/<change>/specs/<capability>/spec.md: the deltas of the change;openspec/changes/<change>/declarations.md: the declarations of the change.
The adapter applies the deltas to the accepted specifications with the rules of OpenSpec
1.13.2 archive: RENAMED, then REMOVED, then MODIFIED, then ADDED. The result is the
effective target. A case that OpenSpec refuses is a fatal diagnostic. Then notarizing stores
a target with the status target_error and no requirements.
The example change
The directory examples/writing-specs holds a
complete small repository: one accepted capability notes and the change add-note-export.
openspec/specs/notes/spec.md accepted: NOTE-R-001
openspec/changes/add-note-export/proposal.md
openspec/changes/add-note-export/tasks.md
openspec/changes/add-note-export/specs/notes/spec.md ADDED NOTE-R-010, NOTE-R-011; MODIFIED NOTE-R-001
openspec/changes/add-note-export/declarations.md one block of each of the seven kinds
To import it, copy the directory into a new Git repository and commit:
cp -R examples/writing-specs /tmp/notes
git -C /tmp/notes init -q
git -C /tmp/notes add -A
git -C /tmp/notes commit -q -m "Propose note export"
notarizing init
notarizing repo add notes /tmp/notes
notarizing change import --repo notes --at main --change add-note-export
Use the name of your default branch in --at. HEAD is not accepted. The import prints
these lines:
requirements: 3 (proposed 3, accepted 1, removed 0); declared nodes 8, edges 15
diagnostics: fatal 0, error 0, warning 0, info 0
The 3 effective requirements are NOTE-R-010, NOTE-R-011 and the modified NOTE-R-001.
accepted 1 is the accepted baseline of NOTE-R-001. The 8 declared nodes are the blocks of
declarations.md. The 15 edges are 6 requirement links and 9 declaration links.
Before you push a change, import it and read the diagnostics line. A clean change has 0 in
each severity. notarizing change report --target tgt_ID lists each diagnostic with its file
and line under "Extractor diagnostics".
Requirement blocks
A requirement block starts with ### Requirement: <name>. Its preamble is the lines after
the heading and before the first heading of any level, usually the first #### Scenario:.
Notarizing reads link lines only in the preamble:
### Requirement: Export all notes
Requirement-ID: NOTE-R-010
Depends-On: NOTE-R-001
Assumes: GRP-EXPORT-PREMISES
Evaluated-By: CHK-EXPORT-TEST
Modeled-By: MDL-EXPORT
The service SHALL write every note of the user to one export file.
#### Scenario: Two notes
- **GIVEN** a user with the notes "A" and "B"
- **WHEN** the user exports the notes
- **THEN** the export file holds "A" and "B"
| Line | Relation | Allowed targets | What it gives |
|---|---|---|---|
Requirement-ID: | identity | one ID | The stable identity. Evidence, review decisions and Compare match a requirement only by this ID. |
Depends-On: | depends_on | requirements | An edge in the dependencies and impact views. |
Assumes: | assumes | assumptions, premise groups | The premises of the requirement in Review. An edge in the dependencies and impact views. |
Evaluated-By: | evaluated_by | checks | An annotation only. It is never a coverage binding. |
Modeled-By: | modeled_by | models | A link to a model. Model evidence does not establish implementation correspondence. |
Follow these rules:
- Write each key exactly as in the table.
depends-on:is not read. - Start the line in column 1 to 4. A line with four or more leading spaces is code.
- Separate several IDs with commas:
Depends-On: NOTE-R-001, NOTE-R-002. - Do not put link lines in fenced code, block quotes or HTML comments. There they only show syntax.
- Write an ID that matches
^[A-Za-z0-9][A-Za-z0-9_.:-]{0,127}$. - If evidence producers name the requirement in reports, also match the
notarizing.check-report/1pattern^[A-Z][A-Z0-9]*-[A-Z0-9]+-[0-9]{3,}$, for exampleNOTE-R-010. - Keep the
Requirement-IDof a MODIFIED requirement. A changed ID stops the import. - Write scenarios as
#### Scenario: <name>with a body. A heading without a body is not a scenario. Notarizing readsGIVEN,WHEN,THEN,ANDandBUTbullets as steps.
A requirement without Requirement-ID gets a provisional reference: the commit, the path, the
heading and the block digest. A provisional reference is unstable. It never matches another
revision, so evidence and review do not carry over. A link to such a requirement does not
resolve.
Declaration blocks
declarations.md declares the nodes that are not requirements. Each block starts with a
level-3 heading ### <Kind>: <title> and ends at the next heading of level 1 to 3. Other
lines in a block are prose. The title must not be empty.
| Kind | ID key (required) | Other keys |
|---|---|---|
Assumption | Assumption-ID | Category (required), Applies-To, Rationale, Exclusions, If-False |
Premise-Group | Group-ID | Operator (required), Members (required) |
Check | Check-ID | Method (a warning without it) |
Model | Model-ID | Assumes |
Component | Component-ID | Implements |
Decision | Decision-ID | Justified-By |
Question | Question-ID | Raised-By |
The list keys make these edges:
| Key | Edge | Allowed items |
|---|---|---|
Applies-To (Assumption) | item assumes the assumption | requirements, models |
Members (Premise-Group) | group member item | requirements, assumptions, premise groups |
Assumes (Model) | model assumes item | assumptions, premise groups |
Implements (Component) | component implements item | requirements |
Justified-By (Decision) | decision justified_by item | requirements, assumptions, results |
Raised-By (Question) | item raises the question | any node except a question |
Use these values:
Category:environment,storage_durability,scheduler_fairness,identity_security,model_abstraction,implementation_obligationorproduct_hypothesis.Operator:all_oforany_of, with an underscore.all-ofis an error.Method:static_analysis,implementation_test,component_simulation,integration_test,finite_model_exploration,bounded_symbolic_check,inductive_model_proof,implementation_trace_conformance,implementation_refinement_proof,measurementorhuman_review.
A premise group with a problem (no members, an unknown operator, an unresolved member, a membership cycle or nesting deeper than 16 levels) stays unresolved. Notarizing never simplifies it to true.
The example declares one block of each kind:
### Assumption: The database gives snapshot reads
Assumption-ID: ASM-SNAPSHOT-READ
Category: storage_durability
Applies-To: NOTE-R-011
Rationale: The export reads all notes in one read transaction.
Exclusions: Read replicas with a replication delay.
If-False: An export can hold a note without its last change.
### Premise-Group: Export premises
Group-ID: GRP-EXPORT-PREMISES
Operator: all_of
Members: ASM-SNAPSHOT-READ, ASM-NOTE-COUNT
### Check: Export integration test
Check-ID: CHK-EXPORT-TEST
Method: integration_test
See declarations.md
for the model, component, decision and question blocks.
What each declaration gives in the product
A declaration is a claim for review. It is not a proof or an approval.
| Source | Review | Explore and graph query |
|---|---|---|
| Requirement | One row with its exact source, assessment rows and missing dimensions. | A requirement node. |
Depends-On | The inspector lists the relationship. | depends_on edge. The dependencies view follows it forward, the impact view in reverse. |
Assumption, Assumes, Applies-To | The requirement lists its premises. The assumption has a review state (open until a reviewer decides). | assumption node and assumes edges. The gaps view lists assumptions without review. |
| Premise group | A row such as ALL OF: ASM-SNAPSHOT-READ (open), ASM-NOTE-COUNT (open). A problem shows as problem: .... | premise_group node. A group view always shows all members. |
| Question | A row under "Open questions". | question node with raises edges. |
Check, Evaluated-By | The diagnostic missing_check_binding until binding import binds the check. | check node. The impact view shows evaluated_by as explanation. |
Model, Modeled-By | Not in the change report list. | model node and the diagnostic missing_model_to_code_mapping. |
| Component, Decision | Not in the change report list. | component and decision nodes. |
For the example, change report prints these rows:
Premise groups
GRP-EXPORT-PREMISES ALL OF: ASM-SNAPSHOT-READ (open), ASM-NOTE-COUNT (open)
Open questions
Q-DELETED-NOTES Do deleted notes go into the export?
To see the graph of one requirement from the CLI:
notarizing graph query --target tgt_ID --object NOTE-R-010 --view dependencies
The dependencies view of NOTE-R-010 holds NOTE-R-001, GRP-EXPORT-PREMISES and its two
assumptions. A declared Evaluated-By never makes a requirement pass. Only an approved
binding (notarizing binding import) and an eligible report do. See
section 6 of the user guide.
Common mistakes
The test makes these mistakes in the example change in one commit:
| Mistake | Severity and code |
|---|---|
depends-on: NOTE-R-010 (wrong case) | warning link_key_case; the line is ignored |
Verified-By: CHK-EXPORT-TEST (unknown key) | warning link_unknown_key; the line is ignored |
Assumes: ..., ASM-MISSING (no such ID) | error reference_unresolved; the edge stays unresolved |
Evaluated-By: after #### Scenario: | warning link_after_preamble; the line is ignored |
Operator: all-of | error group_operator; the group stays unresolved |
Category: business | error declaration_invalid_value; the assumption has a problem |
Members: in a Check block | warning declaration_key_for_other_kind; the line is ignored |
a Question block without Question-ID | error declaration_missing_id; the block is rejected |
Implements: names an assumption | error endpoint_invalid; the edge is invalid |
### Requirement: in declarations.md | warning declaration_requirement_block; the block is ignored |
The import succeeds with diagnostics: fatal 0, error 5, warning 5, info 0. The change report
lists each diagnostic:
Extractor diagnostics
error declaration_invalid_value openspec/changes/add-note-export/declarations.md:15 the category "business" is not one of the seven assumption categories
error group_operator openspec/changes/add-note-export/declarations.md:20 the operator "all-of" is not all_of or any_of; the group stays unresolved
warning declaration_key_for_other_kind openspec/changes/add-note-export/declarations.md:26 the key "Members" is for Premise-Group declarations, not Check; the line is ignored
error endpoint_invalid openspec/changes/add-note-export/declarations.md:34 the implements relation cannot go from component CMP-EXPORT to assumption ASM-NOTE-COUNT
error declaration_missing_id openspec/changes/add-note-export/declarations.md:40 the Question declaration has no Question-ID line; the block is rejected
warning declaration_requirement_block openspec/changes/add-note-export/declarations.md:43 requirement blocks are read only from spec.md; this block is ignored
warning link_after_preamble openspec/changes/add-note-export/specs/notes/spec.md:14 the Evaluated-By line is after the first heading of the requirement and is ignored
warning link_key_case openspec/changes/add-note-export/specs/notes/spec.md:22 the key "depends-on" must be written "Depends-On"; the line is ignored
warning link_unknown_key openspec/changes/add-note-export/specs/notes/spec.md:23 the key "Verified-By" is not a requirement link key; the line is ignored
error reference_unresolved openspec/changes/add-note-export/specs/notes/spec.md:24 the Assumes reference to ASM-MISSING does not resolve in the effective target
The same report shows problem: unknown category "business" on the assumption and
problem: unknown operator "all-of" on the premise group.
A requirement without Requirement-ID gives an info diagnostic. Links to its old ID then do
not resolve:
error reference_unresolved openspec/changes/add-note-export/declarations.md:8 the Applies-To reference to NOTE-R-011 does not resolve in the effective target
error reference_unresolved openspec/changes/add-note-export/declarations.md:33 the Implements reference to NOTE-R-011 does not resolve in the effective target
info requirement_id_missing openspec/changes/add-note-export/specs/notes/spec.md:18 the requirement "Consistent export" has no Requirement-ID; its reference is provisional and unstable
Mistakes that stop the import
A fatal diagnostic stops the construction of the effective target. change import exits
with code 1 and the error target_error. It prints the diagnostics of the stored target.
Two requirements with one ID:
fatal duplicate_id openspec/changes/add-note-export/specs/notes/spec.md:3 the Requirement-ID NOTE-R-010 has different effective proposed definitions at openspec/changes/add-note-export/specs/notes/spec.md:3, openspec/changes/add-note-export/specs/notes/spec.md:18
A MODIFIED requirement with another ID than the accepted one:
fatal requirement_id_changed openspec/changes/add-note-export/specs/notes/spec.md:33 MODIFIED requirement "Save a note" changes its Requirement-ID from NOTE-R-001 to NOTE-R-002; the identity is ambiguous
Other fatal codes come from OpenSpec delta rules, for example delta_modified_not_found (a
MODIFIED heading that does not match an accepted requirement), delta_added_exists and
delta_conflict. Fix the source, commit and import the new commit. A stored target never
changes.
Limits
The adapter refuses a file with more than 2,000 requirement or declaration blocks, and a target with more than 200,000 declared edges. See Limits for all limits of an import.