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"
LineRelationAllowed targetsWhat it gives
Requirement-ID:identityone IDThe stable identity. Evidence, review decisions and Compare match a requirement only by this ID.
Depends-On:depends_onrequirementsAn edge in the dependencies and impact views.
Assumes:assumesassumptions, premise groupsThe premises of the requirement in Review. An edge in the dependencies and impact views.
Evaluated-By:evaluated_bychecksAn annotation only. It is never a coverage binding.
Modeled-By:modeled_bymodelsA 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/1 pattern ^[A-Z][A-Z0-9]*-[A-Z0-9]+-[0-9]{3,}$, for example NOTE-R-010.
  • Keep the Requirement-ID of 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 reads GIVEN, WHEN, THEN, AND and BUT bullets 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.

KindID key (required)Other keys
AssumptionAssumption-IDCategory (required), Applies-To, Rationale, Exclusions, If-False
Premise-GroupGroup-IDOperator (required), Members (required)
CheckCheck-IDMethod (a warning without it)
ModelModel-IDAssumes
ComponentComponent-IDImplements
DecisionDecision-IDJustified-By
QuestionQuestion-IDRaised-By

The list keys make these edges:

KeyEdgeAllowed items
Applies-To (Assumption)item assumes the assumptionrequirements, models
Members (Premise-Group)group member itemrequirements, assumptions, premise groups
Assumes (Model)model assumes itemassumptions, premise groups
Implements (Component)component implements itemrequirements
Justified-By (Decision)decision justified_by itemrequirements, assumptions, results
Raised-By (Question)item raises the questionany node except a question

Use these values:

  • Category: environment, storage_durability, scheduler_fairness, identity_security, model_abstraction, implementation_obligation or product_hypothesis.
  • Operator: all_of or any_of, with an underscore. all-of is 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, measurement or human_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.

SourceReviewExplore and graph query
RequirementOne row with its exact source, assessment rows and missing dimensions.A requirement node.
Depends-OnThe inspector lists the relationship.depends_on edge. The dependencies view follows it forward, the impact view in reverse.
Assumption, Assumes, Applies-ToThe 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 groupA 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.
QuestionA row under "Open questions".question node with raises edges.
Check, Evaluated-ByThe diagnostic missing_check_binding until binding import binds the check.check node. The impact view shows evaluated_by as explanation.
Model, Modeled-ByNot in the change report list.model node and the diagnostic missing_model_to_code_mapping.
Component, DecisionNot 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:

MistakeSeverity 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-oferror group_operator; the group stays unresolved
Category: businesserror declaration_invalid_value; the assumption has a problem
Members: in a Check blockwarning declaration_key_for_other_kind; the line is ignored
a Question block without Question-IDerror declaration_missing_id; the block is rejected
Implements: names an assumptionerror endpoint_invalid; the edge is invalid
### Requirement: in declarations.mdwarning 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.

All Notarizing documents