Verisyntax — brugermanual (prototype 0.1)

Editor og live syntakskontrol

Den første IDE-komponent er implementeret som en separat C++ language server:

<compiler>/verisyntax-ls --version

En LSP-kompatibel editor skal starte den absolutte sti <compiler>/verisyntax-ls for .vsx-filer. Serveren arbejder over standard input/output og åbner ingen port. Den kontrollerer det aktuelle, også endnu ikke gemte, dokument og leverer:

syntaks- og semantikfejl med stabile kodefamilier;
completion for engelske nøgleord, deklarationer, predicates, aliases og typede alias.column-referencer;
hover-information for databases, sources, datasets, columns og nøgleord;
C++-autorativ Format Document, der bevarer kommentarer, quoted strings, deklarationsrækkefølge og interne blanklinjer;
standard Go to Definition og Find All References i det aktuelle dokument for declarations, probabilistiske variable, predicates og source-bundne columns; et dataset-alias går til sin source declaration;
korrekt positionering af Unicode via LSP's UTF-16-konvention.

Version 0.1 bruger full-document synchronization. Databasekontakt sker kun gennem eksplicitte, bekræftede read-only handlinger eller særskilt godkendte mutationer. IR-, SQL- og fil-import-preview åbner ikke databasen; Preview Source Data Read-Only er derimod en synligt bekræftet live query. Serveren kontakter kun lokal Ollama via den særskilte, off-by-default claim-kommando efter synlig evidensbekræftelse og ændrer aldrig .vsx-filer. Den præcise klientkontrakt står i LANGUAGE_SERVER.md.

Den lokale VS Code-klient kan installeres efter build:

code --install-extension <editor-extension> --force

Åbn derefter projektmappen i VS Code og en .vsx-fil. Editorhandlingerne omfatter C++-baseret semantisk fremhævning, formattering, Normalize safe whitespace, F12 Go to Definition, Find All References, Rename Symbol, Compile C++ Plan, IR/SQL-preview, logik/sandsynlighed, read-only data, import, schema-browser, join composer samt Configure Local Review Identity, claim-review og rule-review med særskilte propose/inspect/approve-or-reject-trin. Semantisk fremhævning virker også over et ufuldstændigt dokument; den fulde formatterings- og compilerhandling kræver gyldig syntaks og semantik. Handlingerne er synlige og versionsbundne og anvendes aldrig automatisk. Navigation og rename er i version 0.1 begrænset til det aktuelle dokument; rename afviser eksisterende eller ugyldige navne og returnerer først ændringer, når hele kandidatdokumentet igen kan parses og typecheckes. Dataset-aliaser kan endnu ikke omdøbes. Kvalificerede columns opløses gennem dataset-aliaset til den eksakte source-column, mens en tvetydig ukvalificeret column ikke gættes. SQL-, compiler-, run- og review-handlingerne bruger kun C++-validerede elementer fra den aktuelle buffer.

Kør Verisyntax: Compile C++ Plan fra Command Palette eller editorens titellinje. Vælg en lokal outputfil, normalt <model>.plan.cpp, og godkend dialogen med source, C++17/IR v1-target, dokumenthash og outputsti. Language serveren compiler den præcise aktive buffer—også ikke-gemte ændringer—med samme backend som verisyntax compile --target cpp. Resultatet indeholder dokumenthash, canonical IR-hash og C++-artefakthash. IDE'en afviser en ændret buffer, kontrollerer artefakthashen før og efter filskrivning og åbner derefter den genererede C++-fil. Denne handling genererer den linkbare C++-plan; den starter ikke skjult en systemlinker og kører ikke programmet.

Vælg derefter Build Native Executable i beskeden, eller kør kommandoen med samme navn separat. Dialogen viser dokument-, IR- og C++-hash, lokal VerisyntaxConfig.cmake, build-mappe og eksekverbar fil. Efter godkendelse kopieres det verificerede artefakt til <managed-storage>, og to synlige VS Code tasks kører CMake configure og build med adskilte procesargumenter. Det faste, sanitiserede CMake-projekt linker kun Verisyntax::core. Build-handlingen kører ikke programmet. Standardindstillingerne er verisyntax.native.cmakePath = cmake og verisyntax.native.packageDir = <workspace-build>.

Kør til sidst Verisyntax: Run Last Native Plan. Vælg enten programmets deklarerede ask/probability-queries eller ét compiler-valideret dataset. Datasettilstanden viser den genererede read-only SQL, databaseprofil, engine, query-hash og de præcise --dataset-argumenter før godkendelse; vilkårlige argumenter kan ikke indtastes. IDE'en genkontrollerer den aktive source-hash og hele executable-hashen både før og efter den særskilte bekræftelse og kører derefter valget i en synlig task-terminal. Live databaseindhold kan have ændret sig efter SQL-previewet. Build-mappen indeholder også et versionsmærket manifest.json med source, hashes, package, build type og executable path.

Den hurtigste ende-til-ende-prøve er <example-project>. Den bruger SQLite :memory: og kræver derfor ingen databaseopsætning. Vælg Program queries for logic- og Bayes-resultater eller datasettet catalog_names for at afprøve compiler-genereret read-only SQL.

Selvstændig macOS-IDE

Den selvstændige Tauri-applikation ligger her efter release-build:

<desktop-release>/Verisyntax IDE.app

Den kan åbnes direkte i Finder eller med:

open "<desktop-release>/Verisyntax IDE.app"

Appen indeholder Monaco-editor, Verisyntax CLI og language server, public headers, schemas, eksempler, den statiske C++-runtime og en flytbar CMake-pakke. Første skærm er en ikke-gemt kopi af ide_native_demo.vsx, så originaleksemplet ikke overskrives. Open og Save arbejder kun med lokale .vsx-filer; Save afviser en fil, der er ændret på disken siden åbning.

Check viser parser- og typefejl fra C++-compileren som editormarkører. Format og Preview IR bruger samme compiler. Databaser, sources og datasets kommer fra canonical IR. Schema kræver synlig bekræftelse og læser kun katalogmetadata. Preview rows er read-only, begrænset til 100 rækker og advarer om uspecificeret rækkefølge og ændringer i live data. Initialize metadata… opretter eller migrerer provenance/review-tabeller efter en særskilt bekræftelse. Import data… håndterer CSV, JSON, line-text og XLSX gennem hashbundet preview og separat commit. Local AI kontakter kun den viste lokale Ollama-adresse, og validerede komplette programforslag forbliver uanvendte, indtil Replace editor with reviewed draft vælges. Regelpanelet gemmer først en inaktiv proposal og kræver en senere godkendelse af den eksakte version og hash.

Native workflow er opdelt i tre særskilte godkendelser: Compile C++, Build native og Run. Dokument-, IR-, C++- og executable-hashes vises i højre side. Datasetkørsel viser først compiler-genereret SQL, database, engine, query-hash og eksakte --dataset-argumenter. Der kan ikke indtastes vilkårlige procesargumenter.

Dokumentér en Run i database og resultatfil

Kørselslinjen har to valg ved siden af Program queries/datasetvælgeren:

Vælg No database audit, hvis kørslen ikke skal skrive i en database, eller vælg Audit: DATABASE (sqlite/postgresql) for at gemme én revisionspost.
Tryk eventuelt Result file… og vælg en lokal .json-fil. Filen er valgfri og kan bruges uden database-audit.
Tryk Run. Godkendelsesdialogen viser både auditdatabasen og resultatfilen, før executable-filen startes.

Database-audit kræver, at den valgte deklarerede database allerede har metadata-schema version 7. Vælg databasen under Data, tryk Initialize metadata…, og godkend oprettelsen/migrationen først. En SQLite-database med path ":memory:" kan ikke bruges som varig auditdatabase, fordi hver proces får sin egen tomme database; brug en filsti. PostgreSQL-forbindelsen skal have skriveret til verisyntax_meta.execution_runs.

En gemt execution_runs-post indeholder:

unikt run-ID, start- og sluttidspunkt i UTC samt varighed i millisekunder;
source-, canonical-IR- og executable-hash;
program/dataset-mode og eventuelt datasetnavn;
succeeded/failed, exit-kode og det fulde stdout/stderr;
separate SHA-256-hashes af stdout og stderr;
eventuel resultatfilsti og SHA-256-hash af de bytes, som faktisk blev gemt.

Resultatfilen har schema verisyntax.execution-result-file version 1 og indeholder samme kørselskontrakt plus det rå output. Efter kørslen åbner IDE'en en struktureret resultatdialog med status, tidspunkt, varighed, eventuel auditpost og resultatfil samt læsbare kort eller en tabel. Den fulde RUN DOCUMENTATION bevares i Results, hvor run-ID, tider, outputhashes og eventuel fil vises. Hvis selve programmet kørte, men efterfølgende auditlagring fejlede, bevares programresultatet og vises sammen med AUDIT WARNING; en mislykket lagring påstås aldrig at være dokumenteret.

Kørsler kan også inspiceres uden mutation fra terminalen:

<compiler>/verisyntax execution-runs list model.vsx local --limit 20

Auditposten dokumenterer, hvad den bestemte executable returnerede på det bestemte tidspunkt. Den beviser ikke, at eksterne live tabeller havde en uforanderlig snapshot-version, medmindre data allerede var importeret med Verisyntax-provenance.

Projektets virtuelle miljøer er lokale: <python-qa-environment> reserveres til Python-QA uden globale pakker, <dependency-storage> styres af package-lock.json, og Rust-artifacts ligger i <native-build-output>. Produktionsappen kræver ikke Python. Den lokale .app er ad-hoc-signeret; offentlig distribution kræver Developer ID-signering og Apple-notarisering.

Preview bruger også ændringer, der endnu ikke er gemt. Både IR- og SQL-resultatet knyttes derfor til sha256 for præcis den buffer. SQL-visningen indeholder source URI, hash, databaseprofil og engine som kommentarer. IR forbliver gyldig JSON; dens hash vises i statuslinjen og outputkanalen Verisyntax Previews. Preview forbinder ikke til databasen og skriver ikke filer.

Read-only resultatgrid

Run Dataset Read-Only viser først databaseprofil, engine og hash og kræver en synlig bekræftelse. Den bekræftede hash sendes tilbage til C++-serveren. Hvis dokumentet er ændret i mellemtiden, afvises kørslen før databaseforbindelsen åbnes.

Resultatgridet viser:

database, engine, read-only-status, varighed og antal rækker;
dokumenthash og hash af den faktisk genererede SQL;
kolonnens Verisyntax-type samt logical/physical source-column;
rigtig SQL NULL adskilt fra tekstværdien "NULL";
provenance coverage for hver source/alias.

Row identity vises kun som tilgængelig, når sourcen bruger provenance row, har en deklareret primary_key, og alle key-felter er valgt ind i datasettet. Ellers forklarer gridet præcist, om primary key mangler, ikke er valgt, eller provenance ikke blev anmodet. Dette er compiler-afledt lineage; en ekstern tabelrække påstås ikke at have en gemt immutable source-version, medmindre den faktisk er importeret og registreret.

SQLite åbnes read-only med en 10-sekunders progress-timeout. PostgreSQL bruger en read-only transaction og 10 sekunders statement-timeout. Runtime afviser mere end 10.000 rækker. Gridet renderer højst de første 1.000 og oplyser det samlede returnerede antal. Resultatpanelet er scriptfrit, bruger restriktiv Content Security Policy og HTML-escaper alle databaseværdier og advarsler.

Logikresultater og forklaringer

Run Logic Queries viser dokumenthashen og kræver bekræftelse, før alle ask-udtryk i bufferen evalueres. Hashen kontrolleres igen af C++-serveren. Handlingen bruger hverken database eller LLM og ændrer ingen filer. Det scriptfri panel viser bindings, samlet truth status, positive/negative proof-ID'er og forklaringsgrafens fact/rule-lokationer og premises. Open-world-reglerne vises også som permanente semantiske advarsler.

Run Probability Queries gør det samme for bare ask rain-queries. Panelet viser exact-status, metode, enumererede tilstande, evidenssandsynlighed og begge boolske posteriorværdier. C++ håndhæver grænsen på 20 variable; handlingen bruger ingen LLM og ændrer intet.

Run Continuous Bayesian Inference læser seed, chains, warmup, retained samples og proposal scale fra verisyntax.inference.*. Før kørsel vælger brugeren enten Run without storing eller Store audited run og derefter eventuelt en deklareret SQLite/PostgreSQL-database. En modal viser dokumenthash og alle indstillinger; C++ kontrollerer hashen igen før sampling. Det scriptfri panel viser posterior mean/SD, HDI, ESS, split R-hat, acceptance, seed og eventuelt audit-run-ID. Uden den særskilte storage-godkendelse ændres databasen ikke.

Show Audited Inference History vælger en deklareret metadata-database og læser højst verisyntax.inference.historyLimit poster (50 som standard, højst 100) read-only. Hver kørsel viser metode, seed, settings, posteriorer og diagnostics. Panelet sammenligner den gemte program_ir_hash med den aktuelle canonical IR og markerer tydeligt Current model IR eller Different model IR. Et hashmatch viser modelidentitet, ikke modelkorrekthed eller datafriskhed.

Preview Source Data Read-Only genbruger gridet til op til 100 aktuelle rækker fra en deklareret source. Før forbindelsen åbnes, viser en modal database, engine, relation og dokumenthash. C++ afviser en ændret buffer, citerer de deklarerede physical columns og håndhæver 10 sekunders timeout. Rækkefølgen er uspecificeret, og senere databaseændringer kan gøre previewet forældet. Lineage er compiler-afledt; uncaptured live rows får ikke automatisk immutable import-provenance.

Schema-browser og redigerbart source-udkast

Kør Verisyntax: Browse Database Schema, vælg en deklareret databaseprofil, og godkend den read-only katalogforespørgsel. Browseren inspicerer profilens valgte schema (main for SQLite, ellers det deklarerede PostgreSQL-schema eller public) og viser tabeller/views, fysiske kolonner, database-type, foreslået Verisyntax-type, nullability og primary-key-rækkefølge. Panelet er scriptfrit og ændrer intet.

Typeforslag er synligt markeret som usikre, når konverteringen ikke er entydig. SQLite bruger dynamisk typing; BLOB/utypede felter kræver review. PostgreSQL numeric/decimal kan miste præcision ved mapping til real, timestamp uden timezone kræver en eksplicit timezone-politik, og ukendte/komplekse typer foreslås som text med advarsel.

Efter inspektionen kan Verisyntax: Generate Source Draft From Last Schema Browse bruges. Vælg relationen og et engelsk source-navn. C++ genlæser kataloget og afviser operationen, hvis enten den åbne .vsx-buffer eller schemafingerprintet er ændret. Det genererede udkast:

beholder physical names gennem from "...";
normaliserer og deduplikerer logical identifiers;
bevarer primary-key-rækkefølge og tilføjer provenance row, når en key blev fundet;
viser review-advarsler og åbnes som et separat, redigerbart Verisyntax-dokument.

Udkastet indsættes aldrig automatisk i projektfilen. Brugeren skal kontrollere typer, nullability, key-stabilitet og row grain og derefter selv vælge, om koden skal overføres. Views uden en sikker primary key får ingen automatisk row-provenance. Samme kataloginspektion kan køres i terminalen med:

<compiler>/verisyntax schema model.vsx local_data

Join composer og dataset-udkast

Kør Verisyntax: Compose Dataset Join Draft for at kombinere to allerede deklarerede sources. Den første version har syv eksplicitte trin:

vælg base source;
vælg en anden source på samme databaseforbindelse;
vælg inner join eller left join;
vælg base-sourcens join-kolonne;
vælg en typekompatibel kolonne på den joined source;
vælg en eller flere outputkolonner — ingen vælges automatisk;
angiv et engelsk dataset-navn.

Compileren afviser cross-database joins, self joins i denne første UI, inkompatible key-typer, dublerede/ukendte outputfelter, ugyldige identifiers og en buffer, der har ændret sig efter valgsekvensen. Resultatet åbnes i et separat, redigerbart dokument og indsættes ikke automatisk.

Outputkanalen viser compiler-afledt lineage og advarsler. En join-kolonne, der ikke er en deklareret single-column primary key, beviser ikke one-to-one-cardinality. Optional join-felter kan ikke matche NULL med lighed. Ved left join markeres joined output som potentielt manglende, også når den oprindelige source-kolonne var required. Hvis valgte outputfelter ikke indeholder hele en sources primary key, oplyses det, at stabil row identity ikke kan vises i senere resultater.

Efter valg af begge join-kolonner tilbyder IDE'en valgfri read-only key-profilering. Brugeren kan fortsætte uden profilering eller godkende to aggregate queries, én pr. source. Hver query har 10 sekunders timeout og kan scanne hele tabellen. Resultatet viser total, non-NULL, NULL, distinct non-NULL, duplicate non-NULL samt complete, unique when present og complete unique. Queryhash og varighed gemmes i outputkanalen, og mulige NULL-, duplicate- og many-to-many-problemer vises før komponeringen fortsætter.

Profilen er to point-in-time observationer, ikke en constraint eller garanti for fremtidige data. Den infererer eller godkender aldrig en key. Multi-column keys, self joins og tre eller flere sources er fortsat senere UI-snit; sproget kan allerede udtrykke flere joins direkte.