Skip to content
This repository was archived by the owner on Oct 14, 2022. It is now read-only.

location_invariant YAML entry type as schema #62

Open
wants to merge 22 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
494bb57
Change loop-invariant-schema to be YAML witness schema
sim642 Jun 13, 2022
7dd4191
Extract $defs in YAML schema
sim642 Jun 13, 2022
37b23fa
Add oneOf around YAML schema for extensibility
sim642 Jun 13, 2022
4c6a1ea
Add descriptions from README to YAML schema
sim642 Jun 13, 2022
03fbbbe
Add loop_invariant_certificate to YAML schema
sim642 Jun 13, 2022
caf63d4
Fix inconsistencies between YAML witness README and schema
sim642 Jun 30, 2022
34aab19
Add more descriptions and SHA-256 patterns to YAML schema
sim642 Jun 30, 2022
a456feb
Add examples to YAML schema
sim642 Jun 30, 2022
62b9bdf
Add long entry type descriptions to YAML schema
sim642 Jun 30, 2022
40c8c18
Rewrite most YAML schema descriptions
sim642 Jun 30, 2022
26ad4be
Remove YAML format descriptions from README
sim642 Jun 30, 2022
e51d956
Update YAML witness format description
sim642 Jun 30, 2022
db9be43
Add json-schema-for-humans for YAML witness
sim642 Jun 30, 2022
daebade
Add GitHub Actions workflow for deploying YAML schema
sim642 Jun 30, 2022
32f9ba9
Improve schema according to review comments
sim642 Aug 11, 2022
529da03
Fix invalid file_hash in loop_invariant_certificate example
sim642 Aug 11, 2022
5d4dcc4
Add pages directory to .gitignore
sim642 Aug 11, 2022
de744a1
Change schema workflow branch to main
sim642 Aug 11, 2022
74d4de0
Expand long examples in generated YAML schema
sim642 Aug 17, 2022
f5ac226
Add location_invariant YAML entry type
sim642 Sep 2, 2022
f8cab59
Generalize loop_invariant_certificate to invariant_certificate
sim642 Sep 2, 2022
c06aa07
Clarify loop_invariant and location_invariant difference
sim642 Sep 2, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update YAML witness format description
sim642 committed Jun 30, 2022
commit e51d95665e9cb4abc6929510746c10ee705d0c8d
15 changes: 5 additions & 10 deletions README-YAML.md
Original file line number Diff line number Diff line change
@@ -27,21 +27,16 @@ Files of verification entries are UTF-8 encoded.

Each file of verification entries contains an array of entries.
The format of an entry depends on its entry type.
Currently, we have the following entry types:
- `loop_invariant`
- `loop-invariant_certificate`

Entry types are use-case specific and independent.
Each producer and consumer of entries can filter those entry types that it supports.

The following sections describe the format of a verification entry for each entry-type.

### Schema

#### Schema
All entry types and their formats are specified using
a [json-schema](http://json-schema.org/):
[witness.schema.json](witness.schema.json).

A [json-schema](http://json-schema.org/) of the format can be found in file
[loop-invariant-schema.json](loop-invariant-schema.json).
This schema can be used for validation and for code generation.
This schema can be used for documentation generation, validation and code generation.


## Examples