Verisyntax — User Manual (prototype 0.1)

Practical exercise: import a CSV file and run a result

The repository includes a ready-to-run project:

<example-project>
├── customer_report.vsx
└── customers.csv

You may copy this folder to your own project location. The CSV file contains:

id,name,country,active
1,Customer A,DK,true
2,Customer B,SE,true
3,Customer C,DK,false
4,Customer D,DK,true

The Verisyntax program is:

database local:
  engine sqlite
  path "customer_report.sqlite"

source customers:
  database local
  table "customers"
  column id: integer
  column name: text
  column country: text
  column active: boolean
  primary_key id
  provenance row

dataset danish_customers:
  from customers as customer
  select customer.id as id
  select customer.name as name
  where customer.country = "DK"

Complete these steps in the IDE:

1. Open Verisyntax IDE and click Open Project….
2. Select the practical_customer_report folder and open customer_report.vsx from the project list.
3. Click Check. The document should be valid. Database, source, and dataset menus are populated from compiler-validated IR.
4. Select local (sqlite) under Database….
5. Click More tools… → Initialize metadata… and approve the operation. This creates customer_report.sqlite and the provenance/review tables. It does not alter unrelated databases.
6. Select customers · customers under Source… and click Import data….
7. Select customers.csv. Enter create, because the destination table does not exist yet.
8. Review the Artifact tab. Check the file hash, mapping, destination, data types, warnings, and four input rows. Approve Commit import.
9. Click Preview rows and approve the bounded read-only query. All four source rows should appear.

1. Click Compile C++ and approve the exact document hash.
2. Click Build native and approve the local build.
3. Select danish_customers (sqlite) in the run menu and click Run.
4. The result dialog table should contain Customer A, Customer C, and Customer D. Customer B is excluded because his country is SE. Close the dialog or choose Open Results tab to inspect the complete run documentation.

This exercise is part of the automated test suite. The test copies the files to a temporary folder, initializes SQLite, imports the CSV file, runs the documented dataset, and checks the actual returned names.

Optional evidence-and-claim extension:

1. Click Configure reviewer and store a project-local reviewer ID and name.
2. Select local (sqlite) again and click Load imported cells under CLAIM REVIEW.
3. Choose a cell such as the one containing Customer A, then click Capture selected mention. The immutable mention records source, import record, cell, and content hashes. It is not a claim or fact.
4. Select the mention, keep glm-4.7-flash:latest and 64K, and click Suggest claim locally. Approve only if local Ollama may read the displayed excerpt.
5. Read and edit the claim JSON. Store reviewed proposal creates an inactive version only.
6. Finish with Approve as fact or Reject claim. Only approval of the displayed exact hash creates an active fact. This adds review history to metadata; it does not silently change the dataset result.

The deterministic desktop acceptance test covers this review chain without a model call. A separate live acceptance test covers the complete flow with the default local model and 64K.

When repeating an import:

• use create only when the physical table does not exist;
• use append to add rows without changing existing rows;
• use merge to compare rows by the declared primary_key, insert new keys, and update changed non-key values.

Merge shows a hash-bound plan before commit and never deletes destination rows automatically.