diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-gh-pages.yml new file mode 100644 index 0000000..0e4eb15 --- /dev/null +++ b/.github/workflows/jekyll-gh-pages.yml @@ -0,0 +1,56 @@ +# Build and deploy this repository to GitHub Pages (Jekyll). +# Repository name can be anything: set Pages source to "GitHub Actions" in repo Settings → Pages. +name: Deploy Jekyll to GitHub Pages + +on: + push: + branches: + - main + workflow_dispatch: + +permissions: + contents: read + pages: write + id-token: write + +concurrency: + group: pages + cancel-in-progress: false + +jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Setup Ruby + uses: ruby/setup-ruby@v1 + with: + ruby-version: "3.3.6" + bundler-cache: true + + - name: Setup Pages + id: pages + uses: actions/configure-pages@v5 + + - name: Build with Jekyll + run: bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}" + env: + JEKYLL_ENV: production + + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 + with: + path: _site + + deploy: + runs-on: ubuntu-latest + needs: build + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..cc80dcb --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +_site/ +.sass-cache/ +.jekyll-cache/ +.jekyll-metadata +vendor/ +.bundle/ diff --git a/.ruby-version b/.ruby-version new file mode 100644 index 0000000..9c25013 --- /dev/null +++ b/.ruby-version @@ -0,0 +1 @@ +3.3.6 diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..d8035cc --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,151 @@ +# KAAS Fuzzing + +KAAS provides remote compute for Go and Rust fuzz testing. Jobs run on cloud machines with configurable timeouts (default 8 hours). + +## When to Suggest Fuzzing + +Proactively suggest fuzzing when working on: +- Functions that parse, decode, or deserialize external input +- Encoding/decoding or serialization roundtrips +- Protocol message handling or wire format parsing +- State machines or complex branching logic +- Any code handling untrusted or user-supplied data +- New or refactored code paths before a release + +## Go Fuzz Tests + +Use `testing.F`. Name targets `FuzzXxx(f *testing.F)` in `_test.go` files. Add seeds with `f.Add(...)`, call `f.Fuzz(func(t *testing.T, ...))`. + +```go +func FuzzParseMessage(f *testing.F) { + f.Add([]byte(`{"type":"transfer","amount":100}`)) + f.Add([]byte(``)) + f.Fuzz(func(t *testing.T, data []byte) { + msg, err := ParseMessage(data) + if err != nil { + return + } + encoded, err := msg.Encode() + if err != nil { + t.Fatalf("re-encode failed: %v", err) + } + msg2, err := ParseMessage(encoded) + if err != nil { + t.Fatalf("parse re-encoded message failed: %v", err) + } + if !msg.Equal(msg2) { + t.Fatal("roundtrip mismatch") + } + }) +} +``` + +## Rust Fuzz Tests + +Use `cargo-fuzz` with targets in `fuzz/fuzz_targets/`. Supported engines: libfuzzer, afl, hongfuzz. + +```rust +#![no_main] +use libfuzzer_sys::fuzz_target; +fuzz_target!(|data: &[u8]| { + if let Ok(msg) = parse_message(data) { + let encoded = msg.encode(); + assert_eq!(msg, parse_message(&encoded).unwrap()); + } +}); +``` + +## Running Jobs + +### `kaas go test` (preferred for Go) + +```bash +kaas go test -fuzz='^FuzzParseMessage$' ./pkg/parser/ +kaas go test -fuzz='^FuzzTransfer$,^FuzzMint$' ./pkg/token/ # multiple targets +``` + +Flags: `--commit` (pin commit, default HEAD), `--fuzztime` (Go duration like `5m`), `--execution-timeout` (minutes, default 480), `--vault-spec`, `--token`, `--branch`, `--go-version`, `--go-build-directory`. + +### `kaas-cli run` (Go and Rust) + +```bash +# Go +kaas-cli run --mode remote --test-mode go \ + --vault-spec org/vault --token "$KAAS_TOKEN" --branch main \ + --fuzz-targets "^FuzzTarget$" --go-version 1.23.8 + +# Rust +kaas-cli run --mode remote --test-mode rust \ + --vault-spec org/vault --token "$KAAS_TOKEN" --branch main \ + --fuzz-targets "fuzz_target" --rust-version stable \ + --rust-fuzz-engine libfuzzer +``` + +## Configuration (`.kaas-cli.toml`) + +```toml +[default] +vault_spec = "org/vault" +token = "your-token" +branch = "main" +url = "https://kaas.runtimeverification.com/" + +[go] +go_version = "latest" +go_build_directory = "./..." +execution_timeout = 480 +``` + +Auto-added to `.gitignore`. CLI flags override config values. + +## API Endpoints + +| Method | Endpoint | Description | +|--------|----------|-------------| +| POST | `/api/orgs/{org}/vaults/{vault}/jobs` | Create a fuzz job | +| GET | `/api/orgs/{org}/vaults/{vault}/jobs` | List vault jobs | +| GET | `/api/jobs/{jobId}` | Get job details | +| POST | `/api/jobs/{jobId}/cancel` | Cancel a job | + +Auth: Bearer token in `Authorization` header. + +**Job `kind` vs CLI:** Remote Forge jobs use API `kind: "foundry"` (Foundry/Forge test suite). That corresponds to **`kaas-cli run --test-mode forge`** — the string `forge` is the CLI test mode name; the API payload uses `foundry`. + +### Go Job Payload + +```json +{ + "kind": "go", "branch": "main", "profiles": [], + "workflowBranch": "main", + "kaasServerUrl": "https://kaas.runtimeverification.com/", + "kaasTestRoot": "./path/to/pkg/", + "executionTimeout": 480, "commitHash": "abc123...", + "goFuzzTarget": "^FuzzMyFunction$", + "goVersion": "1.23.8", "goBuildDirectory": "./..." +} +``` + +### Rust Job Payload + +```json +{ + "kind": "rust", "branch": "main", "profiles": [], + "workflowBranch": "main", + "kaasServerUrl": "https://kaas.runtimeverification.com/", + "kaasTestRoot": ".", "executionTimeout": 480, + "rustFuzzTarget": "fuzz_transfer", "rustVersion": "stable", + "rustBuildDirectory": ".", "rustFuzzEngine": "libfuzzer" +} +``` + +Job statuses: `pending` → `running` → `success` / `failure` / `error` + +Dashboard: `https://kaas.runtimeverification.com/app/organization/{org}/{vault}/job/{jobId}/dashboard` + +## Environment Variables + +| Variable | Description | +|----------|-------------| +| `KAAS_TOKEN` | API token | +| `KAAS_SERVER_URL` | Server URL (default: production) | +| `KAAS_ORG_VAULT` | Default vault spec (`org/vault`) | diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..8bf0e29 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,78 @@ +# KAAS Fuzzing Knowledge + +KAAS provides remote compute for Go/Rust fuzz testing. Jobs run on cloud machines, default timeout 8 hours. + +## When to Suggest Fuzzing + +Suggest fuzzing for: parsing/deserialization, encoding roundtrips, protocol handling, state machines, untrusted input handling, pre-release code paths. + +## Go Fuzz Tests + +Name: `FuzzXxx(f *testing.F)` in `_test.go`. Add seeds with `f.Add(...)`. Call `f.Fuzz(func(t *testing.T, ...))`. Test invariants, not just "doesn't crash." + +## Rust Fuzz Tests + +Use `cargo-fuzz` with targets in `fuzz/fuzz_targets/`. Engines: libfuzzer (default), afl, hongfuzz. + +## CLI Commands + +### `kaas go test` (preferred for Go) + +```bash +kaas go test -fuzz='^FuzzTarget$' ./path/to/pkg/ +kaas go test -fuzz='^FuzzA$,^FuzzB$' ./pkg/ # multiple targets, separate jobs +``` + +Flags: `--commit`, `-fuzz`/`--fuzz` (same option), `--fuzztime` (Go duration), `--execution-timeout` (minutes, default 480), `--vault-spec`, `--token`, `--branch`, `--go-version`, `--go-build-directory`. + +### `kaas-cli run` (Go and Rust) + +```bash +kaas-cli run --mode remote --test-mode go \ + --vault-spec org/vault --token "$KAAS_TOKEN" --branch main \ + --fuzz-targets "^FuzzTarget$" --go-version 1.23.8 + +kaas-cli run --mode remote --test-mode rust \ + --vault-spec org/vault --token "$KAAS_TOKEN" --branch main \ + --fuzz-targets "fuzz_target" --rust-version stable --rust-fuzz-engine libfuzzer +``` + +## Config (`.kaas-cli.toml`) + +```toml +[default] +vault_spec = "org/vault" +token = "your-token" +branch = "main" +url = "https://kaas.runtimeverification.com/" + +[go] +go_version = "latest" +go_build_directory = "./..." +execution_timeout = 480 +``` + +CLI flags override config. File auto-added to `.gitignore`. + +## API + +Auth: Bearer token. Base: `https://kaas.runtimeverification.com` + +- `POST /api/orgs/{org}/vaults/{vault}/jobs` — create job +- `GET /api/orgs/{org}/vaults/{vault}/jobs` — list jobs +- `GET /api/jobs/{jobId}` — job details +- `POST /api/jobs/{jobId}/cancel` — cancel job + +Go payload: `{"kind":"go","branch":"main","profiles":[],"workflowBranch":"main","kaasServerUrl":"...","kaasTestRoot":"./pkg/","executionTimeout":480,"commitHash":"...","goFuzzTarget":"^Fuzz$","goVersion":"1.23.8","goBuildDirectory":"./..."}` + +Rust payload: `{"kind":"rust","branch":"main","profiles":[],"workflowBranch":"main","kaasServerUrl":"...","kaasTestRoot":".","executionTimeout":480,"rustFuzzTarget":"fuzz_target","rustVersion":"stable","rustBuildDirectory":".","rustFuzzEngine":"libfuzzer"}` + +## Environment Variables + +`KAAS_TOKEN` (API token), `KAAS_SERVER_URL` (server URL), `KAAS_ORG_VAULT` (default vault spec `org/vault`). + +## Dashboard + +`https://kaas.runtimeverification.com/app/organization/{org}/{vault}/job/{jobId}/dashboard` + +Statuses: pending → running → success / failure / error diff --git a/Gemfile b/Gemfile new file mode 100644 index 0000000..d99ca9b --- /dev/null +++ b/Gemfile @@ -0,0 +1,4 @@ +source "https://rubygems.org" + +gem "jekyll", "~> 4.3" +gem "webrick", "~> 1.8" diff --git a/Gemfile.lock b/Gemfile.lock new file mode 100644 index 0000000..52cba3b --- /dev/null +++ b/Gemfile.lock @@ -0,0 +1,81 @@ +GEM + remote: https://rubygems.org/ + specs: + addressable (2.8.9) + public_suffix (>= 2.0.2, < 8.0) + base64 (0.3.0) + colorator (1.1.0) + concurrent-ruby (1.3.6) + csv (3.3.5) + em-websocket (0.5.3) + eventmachine (>= 0.12.9) + http_parser.rb (~> 0) + eventmachine (1.2.7) + ffi (1.17.4) + forwardable-extended (2.6.0) + google-protobuf (3.25.8-x86_64-linux) + http_parser.rb (0.8.1) + i18n (1.14.8) + concurrent-ruby (~> 1.0) + jekyll (4.4.1) + addressable (~> 2.4) + base64 (~> 0.2) + colorator (~> 1.0) + csv (~> 3.0) + em-websocket (~> 0.5) + i18n (~> 1.0) + jekyll-sass-converter (>= 2.0, < 4.0) + jekyll-watch (~> 2.0) + json (~> 2.6) + kramdown (~> 2.3, >= 2.3.1) + kramdown-parser-gfm (~> 1.0) + liquid (~> 4.0) + mercenary (~> 0.3, >= 0.3.6) + pathutil (~> 0.9) + rouge (>= 3.0, < 5.0) + safe_yaml (~> 1.0) + terminal-table (>= 1.8, < 4.0) + webrick (~> 1.7) + jekyll-sass-converter (3.0.0) + sass-embedded (~> 1.54) + jekyll-watch (2.2.1) + listen (~> 3.0) + json (2.19.3) + kramdown (2.5.2) + rexml (>= 3.4.4) + kramdown-parser-gfm (1.1.0) + kramdown (~> 2.0) + liquid (4.0.4) + listen (3.10.0) + logger + rb-fsevent (~> 0.10, >= 0.10.3) + rb-inotify (~> 0.9, >= 0.9.10) + logger (1.7.0) + mercenary (0.4.0) + pathutil (0.16.2) + forwardable-extended (~> 2.6) + public_suffix (6.0.2) + rake (13.3.1) + rb-fsevent (0.11.2) + rb-inotify (0.11.1) + ffi (~> 1.0) + rexml (3.4.4) + rouge (4.7.0) + safe_yaml (1.0.5) + sass-embedded (1.69.5) + google-protobuf (~> 3.23) + rake (>= 13.0.0) + terminal-table (3.0.2) + unicode-display_width (>= 1.1.1, < 3) + unicode-display_width (2.6.0) + webrick (1.9.2) + +PLATFORMS + x86_64-linux + +DEPENDENCIES + jekyll (~> 4.3) + webrick (~> 1.8) + +BUNDLED WITH + 2.4.19 diff --git a/README.md b/README.md index 3074bdd..6296bfc 100644 --- a/README.md +++ b/README.md @@ -1,21 +1,34 @@ ---- -description: Revolutionize your K framework experience ---- -### Get Started Here +# KaaS documentation (source) -# KaaS +User-facing documentation for [KaaS](https://kaas.runtimeverification.com), published as a static site with **Jekyll** and **GitHub Pages**. -Introducing **KaaS** (**K** as a Service), a cloud-based solution designed to enhance the [**K** framework](https://kframework.org/) experience. **KaaS** is engineered to introduce new features, streamline operations, and foster collaboration among teams. By leveraging caching proofs and remote computation, it eliminates redundant processes, saving your team precious time. +## Local preview -**KaaS** integrates seamlessly with continuous integration (CI) systems, allowing developers to pull the latest cached results and bypass repetitive computations. It's a perfect solution for internal teams, centralizing shared computational results for improved collaboration. +```bash +bundle install +bundle exec jekyll serve +``` -For data management, **KaaS** employs reliable and secure storage. User access is protected through unique project keys, ensuring your data's safety. Additionally, **KaaS** provides a robust Command Line Interface (CLI) with commands for efficient cache management, remote and local proof execution for user sessions. +Open . If you use a non-empty `baseurl` (project Pages URL), run: -Cloud Compute: KaaS takes advantage of cloud computing to provide scalable and efficient remote computation. This allows users to offload heavy computational tasks to the cloud. The integration with cloud computing services makes KaaS a powerful tool for large-scale computations with the K framework. +```bash +bundle exec jekyll serve --baseurl /your-repo-name +``` -With **KaaS**, our vision is to make the **K** framework more accessible to users, serving as the perfect entry point for anyone looking to leverage the power of the **K** framework +## GitHub Pages -# Next Steps +1. Repository **Settings** → **Pages** → **Build and deployment**: source **GitHub Actions**. +2. Push to `main`; the workflow [`.github/workflows/jekyll-gh-pages.yml`](.github/workflows/jekyll-gh-pages.yml) builds and deploys the `jekyll build` output. +3. Optional: set a **custom domain** (e.g. `docs.kaas.runtimeverification.com`) in Pages settings and add the DNS records GitHub shows. -- [KaaS Web Setup](/overview/kaas/kaas-web_setup.md) -- [KaaS CLI Tool Installation](/overview/kaas/kaas-cli_installation.md) +`jekyll build --baseurl` is supplied automatically in CI so the site works both at `https://.github.io//` and behind a custom domain (with `baseurl` empty in `_config.yml` once the domain is configured—GitHub still passes the correct base path for subdirectory installs). + +## Content + +- Markdown pages live under [`guides/`](guides/) and [`overview/kaas/`](overview/kaas/). +- Navigation is [`_data/nav.yml`](_data/nav.yml). +- `AGENTS.md` / `CLAUDE.md` are for AI assistants and are **not** published on the site (see `_config.yml` `exclude`). + +### Images + +Screenshots previously referenced as `/.gitbook/assets/...` should be placed under `assets/images/` (same filenames). Add files there to fix broken images until they are migrated. diff --git a/SUMMARY.md b/SUMMARY.md index 01a9a34..4cb6c76 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -1,9 +1,11 @@ -# Table of contents +# Table of contents (legacy) + +> **Note:** This file was used by GitBook. The published site navigation is defined in [`_data/nav.yml`](_data/nav.yml). ## Overview * [KaaS](README.md) - * [KaaS Organization Setup](/overview/kaas/kaas-web_setup.md) + * [Organizations, Vaults & GitHub App](/overview/kaas/kaas-web_setup.md) * [KaaS CLI Installation](/overview/kaas/kaas-cli_installation.md) ## Guides @@ -11,6 +13,9 @@ * [Using KaaS CLI](/guides/kaas-cli_connecting-using-tokens.md) * [Authentification Using Device Flow](/guides/kaas-cli_connecting-using-device-flow.md) * [`run` Command Documentation](/guides/kaas-cli_run_command.md) +* [Foundry (`forge test`) with kaas-cli](/guides/kaas-cli_forge_test.md) +* [Remote Fuzzing](/guides/kaas-cli_remote_fuzzing.md) +* [AI Agent Setup](/guides/kaas-ai-agent-setup.md) * [Using KaaS in CI](/guides/kaas_setting-up-ci.md) * [KCFG Tagging Tutorial](/guides/kaas-cli_tagging-best-practices.md) diff --git a/_config.yml b/_config.yml new file mode 100644 index 0000000..7bc1b28 --- /dev/null +++ b/_config.yml @@ -0,0 +1,32 @@ +title: KaaS Documentation +description: K as a Service — user documentation +url: "" # optional; set in GitHub repo Settings → Pages → Custom domain (e.g. https://docs.kaas.runtimeverification.com) + +# Overridden in CI via: jekyll build --baseurl "" +# For a project site without custom domain, GitHub supplies the repo base path (e.g. /gitbook-kaas). +baseurl: "" + +permalink: pretty + +markdown: kramdown +kramdown: + input: GFM + hard_wrap: false + +exclude: + - Gemfile + - Gemfile.lock + - README.md + - SUMMARY.md + - AGENTS.md + - CLAUDE.md + - vendor + - "*.code-workspace" + - ".git" + - ".github" + +defaults: + - scope: + path: "" + values: + layout: default diff --git a/_data/nav.yml b/_data/nav.yml new file mode 100644 index 0000000..765ad96 --- /dev/null +++ b/_data/nav.yml @@ -0,0 +1,38 @@ +- title: Overview + items: + - title: KaaS (home) + url: / + - title: Organizations, Vaults & GitHub App + url: /overview/kaas/kaas-web_setup/ + - title: KaaS CLI Installation + url: /overview/kaas/kaas-cli_installation/ + +- title: Guides + items: + - title: Using KaaS CLI (tokens) + url: /guides/kaas-cli_connecting-using-tokens/ + - title: Authentication (device flow) + url: /guides/kaas-cli_connecting-using-device-flow/ + - title: "`run` command" + url: /guides/kaas-cli_run_command/ + - title: Foundry (`forge test`) + url: /guides/kaas-cli_forge_test/ + - title: Remote fuzzing + url: /guides/kaas-cli_remote_fuzzing/ + - title: AI agent setup + url: /guides/kaas-ai-agent-setup/ + - title: KaaS in CI + url: /guides/kaas_setting-up-ci/ + - title: KCFG tagging + url: /guides/kaas-cli_tagging-best-practices/ + - title: CLI deep dive (CI upload/download) + url: /guides/kaas-cli-deep-dive/ + +- title: Community + items: + - title: Telegram + url: https://t.me/rv_inc + external: true + - title: Discord + url: https://discord.gg/CurfmXNtbN + external: true diff --git a/_includes/nav.html b/_includes/nav.html new file mode 100644 index 0000000..d5ee957 --- /dev/null +++ b/_includes/nav.html @@ -0,0 +1,18 @@ + diff --git a/_layouts/default.html b/_layouts/default.html new file mode 100644 index 0000000..6515c25 --- /dev/null +++ b/_layouts/default.html @@ -0,0 +1,26 @@ + + + + + + {% if page.title %}{{ page.title | escape }} | {% endif %}{{ site.title | escape }} + + + + + +
+ +
+
+ {{ content }} +
+
+
+ + diff --git a/assets/css/style.css b/assets/css/style.css new file mode 100644 index 0000000..cd1973a --- /dev/null +++ b/assets/css/style.css @@ -0,0 +1,254 @@ +:root { + --bg: #fafafa; + --sidebar-bg: #f0f0f2; + --text: #1a1a1a; + --muted: #5c5c5c; + --link: #0b5fff; + --border: #d9d9de; + --active-bg: #e8eefc; + --code-bg: #f3f3f5; + --max-prose: 48rem; +} + +*, +*::before, +*::after { + box-sizing: border-box; +} + +html { + font-size: 16px; +} + +body { + margin: 0; + font-family: system-ui, -apple-system, "Segoe UI", Roboto, Ubuntu, Cantarell, "Noto Sans", sans-serif; + line-height: 1.6; + color: var(--text); + background: var(--bg); +} + +.skip-link { + position: absolute; + left: -9999px; + top: 0.5rem; + padding: 0.5rem 1rem; + background: var(--link); + color: #fff; + z-index: 100; +} + +.skip-link:focus { + left: 0.5rem; +} + +.page-wrapper { + display: flex; + min-height: 100vh; +} + +.sidebar { + flex: 0 0 16rem; + max-width: 100%; + background: var(--sidebar-bg); + border-right: 1px solid var(--border); +} + +.sidebar-inner { + position: sticky; + top: 0; + max-height: 100vh; + overflow-y: auto; + padding: 1.25rem 1rem 2rem; +} + +.site-title { + margin: 0 0 1.25rem; + font-size: 1.1rem; + font-weight: 700; +} + +.site-title a { + color: var(--text); + text-decoration: none; +} + +.site-title a:hover { + text-decoration: underline; +} + +.nav-heading { + margin: 1.25rem 0 0.35rem; + font-size: 0.7rem; + font-weight: 600; + text-transform: uppercase; + letter-spacing: 0.04em; + color: var(--muted); +} + +.nav-section:first-child .nav-heading { + margin-top: 0; +} + +.nav-list { + margin: 0; + padding: 0; + list-style: none; +} + +.nav-link { + display: block; + padding: 0.25rem 0.5rem; + margin: 0.1rem 0; + font-size: 0.9rem; + color: var(--link); + text-decoration: none; + border-radius: 4px; +} + +.nav-link:hover { + background: rgba(0, 0, 0, 0.04); +} + +.nav-link.is-active { + background: var(--active-bg); + font-weight: 600; + color: var(--text); +} + +.main { + flex: 1; + min-width: 0; + padding: 1.5rem 1.75rem 3rem; +} + +.prose { + max-width: var(--max-prose); +} + +.prose h1, +.prose h2, +.prose h3 { + line-height: 1.25; + scroll-margin-top: 1rem; +} + +.prose h1 { + margin-top: 0; + font-size: 1.75rem; +} + +.prose h2 { + margin-top: 2rem; + font-size: 1.35rem; + border-bottom: 1px solid var(--border); + padding-bottom: 0.25rem; +} + +.prose h3 { + margin-top: 1.5rem; + font-size: 1.1rem; +} + +.prose p, +.prose ul, +.prose ol { + margin: 0.75rem 0; +} + +.prose table { + border-collapse: collapse; + width: 100%; + font-size: 0.9rem; + margin: 1rem 0; +} + +.prose th, +.prose td { + border: 1px solid var(--border); + padding: 0.4rem 0.6rem; + text-align: left; + vertical-align: top; +} + +.prose th { + background: var(--code-bg); +} + +.prose pre, +.prose code { + font-family: ui-monospace, "Cascadia Code", "Source Code Pro", Menlo, Consolas, monospace; + font-size: 0.88em; +} + +.prose pre { + background: var(--code-bg); + border: 1px solid var(--border); + border-radius: 6px; + padding: 0.75rem 1rem; + overflow-x: auto; +} + +.prose code { + background: var(--code-bg); + padding: 0.12rem 0.35rem; + border-radius: 4px; +} + +.prose pre code { + background: none; + padding: 0; +} + +.prose blockquote { + margin: 1rem 0; + padding: 0.5rem 1rem; + border-left: 4px solid var(--link); + background: #f7f9fc; + color: #333; +} + +.prose blockquote.note-warn { + border-left-color: #c27a00; + background: #fff9ed; +} + +.prose img, +.prose iframe { + max-width: 100%; + height: auto; +} + +.prose figure { + margin: 1rem 0; +} + +.callout { + margin: 1rem 0; + padding: 0.75rem 1rem; + border-radius: 6px; + border: 1px solid var(--border); + background: #f7f9fc; +} + +.callout-warn { + border-color: #e8c066; + background: #fff9ed; +} + +@media (max-width: 768px) { + .page-wrapper { + flex-direction: column; + } + + .sidebar { + flex: none; + border-right: none; + border-bottom: 1px solid var(--border); + } + + .sidebar-inner { + position: relative; + max-height: none; + } +} diff --git a/assets/images/.gitkeep b/assets/images/.gitkeep new file mode 100644 index 0000000..e69de29 diff --git a/guides/kaas-ai-agent-setup.md b/guides/kaas-ai-agent-setup.md new file mode 100644 index 0000000..17a9809 --- /dev/null +++ b/guides/kaas-ai-agent-setup.md @@ -0,0 +1,82 @@ +--- +title: AI agent setup +description: AGENTS.md, CLAUDE.md, and other tools for KAAS fuzzing +--- + +# AI Agent Setup for KAAS Fuzzing + +KAAS publishes **tool-agnostic** knowledge at the root of the [gitbook-kaas](https://github.com/runtimeverification/gitbook-kaas) repository so you can use the same material with **Cursor**, **Claude Code**, **GitHub Copilot**, **Codex**, **ChatGPT** (Projects / Custom GPTs), and other assistants that load project instructions or uploaded files. + +This guide explains how to wire that content into your workflow. The canonical copies live as **`AGENTS.md`** (widely supported) and **`CLAUDE.md`** (Claude-specific). Treat those files as the source of truth; any IDE-specific layout under `.cursor/` or similar in a fork is an **optional supplement**, not a different product contract. + +The knowledge covers: +- When and why to write fuzz tests +- Go and Rust fuzz test patterns +- Using the `kaas-cli` and `kaas go test` commands +- KAAS API endpoints for programmatic access +- `.kaas-cli.toml` configuration + +## Option 1: AGENTS.md (recommended baseline) + +`AGENTS.md` is recognized by Cursor, Claude Code, GitHub Copilot, Codex, and many other agents. Place it in your project root so the tool can load it automatically. + +**Install:** + +Copy the KAAS fuzzing `AGENTS.md` into the root of any project where you want AI-assisted fuzzing: + +```bash +curl -o AGENTS.md https://raw.githubusercontent.com/runtimeverification/gitbook-kaas/main/AGENTS.md +``` + +Or copy it manually from the [gitbook-kaas repository](https://github.com/runtimeverification/gitbook-kaas/blob/main/AGENTS.md). + +The file is picked up automatically — no additional configuration needed. + +## Option 2: Claude Code (CLAUDE.md) + +Claude Code loads `CLAUDE.md` files automatically from your project root or `~/.claude/CLAUDE.md` for global preferences. + +**Project-level:** + +```bash +curl -o CLAUDE.md https://raw.githubusercontent.com/runtimeverification/gitbook-kaas/main/CLAUDE.md +``` + +**Global (personal, all projects):** + +```bash +curl -o ~/.claude/CLAUDE.md https://raw.githubusercontent.com/runtimeverification/gitbook-kaas/main/CLAUDE.md +``` + +If you already have a `CLAUDE.md`, append the KAAS content or use `@import` to reference it. + +## Option 3: IDE- or vendor-specific folders (optional) + +Some products also read instructions from paths like `.cursor/rules/` or `.cursor/skills/`. If your team maintains such files, keep them aligned with **`AGENTS.md`** / **`CLAUDE.md`** so every agent sees the same flags, defaults, and API notes. You do **not** need a particular IDE to use KAAS fuzzing documentation—start from the root files above. + +## Option 4: ChatGPT (Custom GPT / Projects) + +ChatGPT supports knowledge files through Custom GPTs and Projects. Since there's no filesystem integration, you upload the knowledge file manually. Use `AGENTS.md` from gitbook-kaas — it is the same canonical content as for other agents. + +**Using ChatGPT Projects:** + +1. Open [ChatGPT](https://chatgpt.com) and go to **Projects** +2. Create or open a project +3. Click **Add files** and upload `AGENTS.md` from [gitbook-kaas](https://github.com/runtimeverification/gitbook-kaas/blob/main/AGENTS.md) +4. Add a custom instruction: *"Refer to the KAAS fuzzing knowledge file when helping with fuzz testing or KAAS CLI usage."* + +**Using a Custom GPT:** + +1. Go to **Explore GPTs** → **Create** +2. In the **Knowledge** section, upload `AGENTS.md` +3. In **Instructions**, add: *"You are a KAAS fuzzing assistant. Use the uploaded knowledge file to help users write fuzz tests and run them on KAAS infrastructure."* + +> **Info.** Custom GPTs require a ChatGPT Plus, Team, or Enterprise subscription. + +## Verifying Installation + +After installation, test that your AI agent has the knowledge by asking: + +> "How do I run a Go fuzz test on KAAS?" + +It should know about `kaas go test`, the **`-fuzz` / `--fuzz`** flag, vault specs, `.kaas-cli.toml` configuration, and the KAAS API. diff --git a/guides/kaas-cli-deep-dive.md b/guides/kaas-cli-deep-dive.md index 1a4d6c1..0626fd4 100644 --- a/guides/kaas-cli-deep-dive.md +++ b/guides/kaas-cli-deep-dive.md @@ -1,10 +1,15 @@ +--- +title: CLI deep dive (CI upload/download) +description: Upload and download proofs with kaas-cli in CI +--- + # Using KaaS CLI This guide will walk you through setting up your CI to upload and download proofs using the **`kaas-cli`** tool. Once set up in your CI pipeline, new proofs will be uploaded automatically with each build, and the latest set of proofs will be downloaded for use in your verification jobs. -First, make sure you have **`kaas-cli`** installed. You can find instructions here: [kaas-cli_installation.md](/overview/kaas/kaas-cli_installation.md "mention"). +First, make sure you have **`kaas-cli`** installed. See [KaaS CLI installation]({% link overview/kaas/kaas-cli_installation.md %}). ### Know Your Vault Name @@ -39,9 +44,7 @@ kaas-cli upload -d ./kout kaas-cli download -d ./kout ``` -{% hint style="info" %} -Specifying a subdirectory is optional. -{% endhint %} +> **Info.** Specifying a subdirectory is optional. ### Authentication @@ -52,11 +55,7 @@ To verify authentication is working before uploading/downloading you can run the kaas-cli check-auth ``` -{% hint style="success" %} -Confirm the message: - -`You are currently authenticated.` -{% endhint %} +> **Success.** You should see: `You are currently authenticated.` ### Tips: diff --git a/guides/kaas-cli_connecting-using-device-flow.md b/guides/kaas-cli_connecting-using-device-flow.md index dda2374..7841eaa 100644 --- a/guides/kaas-cli_connecting-using-device-flow.md +++ b/guides/kaas-cli_connecting-using-device-flow.md @@ -1,4 +1,9 @@ -# Authentification kaas-cli Using Device Flow +--- +title: Authentication (device flow) +description: Sign in to kaas-cli with GitHub device flow +--- + +# Authentication with kaas-cli (device flow) ### **Login** @@ -17,17 +22,9 @@ Then hit 'Enter'. Press Enter to continue or type 'q' to quit: ``` -Follow the link in the browser, and you will see the following window: - -
- -Copy the code from the terminal and paste it into the browser. Then click "Continue." After the code is confirmed, click the "Authorize runtimeverification" button. - -
- -You will then see the message below. +Follow the link in the browser. On GitHub’s **device activation** page, paste the user code from the terminal, choose **Continue**, then approve the **runtimeverification** OAuth application when prompted (**Authorize runtimeverification** or equivalent). -
+When activation succeeds, GitHub shows a short confirmation that the device is connected and you can close the browser tab. You can now return to the terminal where the `cli` is open and click "Enter." You will see this message: diff --git a/guides/kaas-cli_connecting-using-tokens.md b/guides/kaas-cli_connecting-using-tokens.md index 32ed581..3e54482 100644 --- a/guides/kaas-cli_connecting-using-tokens.md +++ b/guides/kaas-cli_connecting-using-tokens.md @@ -1,5 +1,6 @@ --- -description: Step-by-step Guidance on Using the Tool +title: Using KaaS CLI (tokens) +description: Tokens, upload/download, and environment variables --- # Getting started @@ -10,7 +11,7 @@ This guide provides step-by-step instructions on how to use **KaaS**. You can us ### **Login** -You can refer to [kaas-cli_connecting-using-device-flow.md](/guides/kaas-cli_connecting-using-device-flow.md "mention") for the detailed guide on how to authenticate using CLI and github device flow. +You can refer to [Authentication (device flow)]({% link guides/kaas-cli_connecting-using-device-flow.md %}) for the detailed guide on how to authenticate using the CLI and GitHub device flow. ### **Creating and Using a Token** @@ -21,12 +22,9 @@ Providing token allows you to skip authentication flow and have same level of ac * Click on `Profile` picture in right top corner * Click on the `Access Tokens` button in the drop-down menu. * Create a new token and copy the `Key`. -2. **Obtain Organization Name and Vault Name:** - * Go to the [KaaS dashboard](https://kaas.runtimeverification.com/app). - * Click the desired organization. - * And click on a Vault. - * Copy the vault name with organization name. It has format: - * Refered to as Vault Spec: `organization-name/vault-name` +2. **Obtain organization and vault (vault spec):** + * Open the [KaaS app](https://kaas.runtimeverification.com/app) and select an **organization**, then a **vault** (or read the names from the URL: `/app/organization/{org}/{vault}`). + * The **vault spec** passed to the CLI is always `organization-name/vault-name` (two path segments, not the optional cache tag). GitHub-linked orgs use the GitHub login as the first segment; user-managed org names include the leading `@`. See [Organizations, Vaults & GitHub App]({% link overview/kaas/kaas-web_setup.md %}) for how orgs and vaults are created. 3. **Use the Token**: * Replace `xxx` with your actual token from previous steps. * Replace `organization-name/vault-name` with names from the previous step @@ -43,9 +41,7 @@ Providing token allows you to skip authentication flow and have same level of ac ``` -{% hint style="info" %} -Use the command `kaas-cli upload --help` and `kaas-cli download --help` to see all available flags. -{% endhint %} +> **Info.** Use `kaas-cli upload --help` and `kaas-cli download --help` to see all available flags. # Authentication Using Environment Variables diff --git a/guides/kaas-cli_forge_test.md b/guides/kaas-cli_forge_test.md new file mode 100644 index 0000000..c147ea1 --- /dev/null +++ b/guides/kaas-cli_forge_test.md @@ -0,0 +1,86 @@ +--- +title: "Foundry (`forge test`) with kaas-cli" +description: Run `forge build` and `forge test` via `--test-mode forge` (local or Docker) +--- + +# Foundry (`forge test`) with `kaas-cli` + +Use **`kaas-cli run --test-mode forge`** to run a standard Foundry workflow: **`forge build`**, then **`forge test`**. This is separate from **`--test-mode kontrol`** (symbolic proofs). The CLI test mode name is **`forge`**; some KaaS APIs and compute jobs refer to the same work as **Foundry** / **`foundry`**. + +## What gets executed + +| Step | Local mode (`--mode local`) | Container mode (`--mode container`) | +|------|-----------------------------|--------------------------------------| +| Build | `forge build` (+ `--extra-build-args`) | Same inside the container | +| Test | `forge test` (+ `--extra-test-args`) | `forge test --json` (+ `--extra-test-args`), streamed to **`foundry_test_report.json`** in the container, then copied back to the host | + +**Remote mode:** **`kaas-cli run --mode remote --test-mode forge` is not implemented.** Remote jobs on KaaS today use this Foundry path through **managed compute / CI workers** that clone your repo and invoke the CLI with **`--mode container`** (see [KaaS in CI]({% link guides/kaas_setting-up-ci.md %})). + +## Prerequisites + +- A **Foundry project** (typically **`foundry.toml`** at the directory you run from, or under **`--test-root`**). +- **`--mode local`:** **`forge`** on your **`PATH`**. +- **`--mode container`:** **Docker** available to the CLI, with permission to pull and run images. + +## Basic usage + +From the repository root (or subdirectory) that contains your Foundry config: + +```bash +kaas-cli run --mode local --test-mode forge +``` + +Run inside a **Foundry Docker image** (no local `forge` install required): + +```bash +kaas-cli run --mode container --test-mode forge +``` + +If tests live under a subdirectory (monorepo layout): + +```bash +kaas-cli run --mode container --test-mode forge --test-root packages/contracts +``` + +## Useful flags (`forge` mode) + +| Flag | Purpose | +|------|---------| +| `--foundry-version` | Image tag when **not** using `--foundry-docker-image` (default image: `ghcr.io/foundry-rs/foundry:`; tag defaults to **`stable`** if unset). | +| `--foundry-docker-image` | Full image reference (overrides version-based default). | +| `--extra-build-args` / `-eb` | Extra arguments appended to **`forge build`**. | +| `--extra-test-args` / `-et` | Extra arguments appended to **`forge test`**. | +| `--verbose` / `-v` | More CLI logging. | + +**Foundry profile:** set **`FOUNDRY_PROFILE`** in your environment before running. In **container** mode, the CLI passes **`FOUNDRY_PROFILE`** into the container (default **`default`** if unset). + +**Examples:** + +```bash +# Match a subset of tests (extra args are appended to forge test) +kaas-cli run --mode local --test-mode forge \ + --extra-test-args "--match-contract MyContractTest" + +# Pin a Foundry image tag +kaas-cli run --mode container --test-mode forge --foundry-version nightly + +# Custom image +kaas-cli run --mode container --test-mode forge \ + --foundry-docker-image ghcr.io/foundry-rs/foundry:latest +``` + +## Machine-readable report (container mode) + +After a successful **container** run, the CLI tries to copy **`foundry_test_report.json`** (JSON test output from **`forge test --json`**) and **`forge_version.txt`** to the host and merges Forge version metadata into **`foundry_test_report.json`**. Use this for CI dashboards or uploads to KaaS job artifacts. + +## Relationship to Kontrol + +- **`--test-mode kontrol`:** **`kontrol build`** / **`kontrol prove`** (and optional **`kontrol.toml`**). +- **`--test-mode forge`:** plain Foundry only — **`forge build`** / **`forge test`**. + +You can use **`forge`** mode to validate that contracts and tests pass in a **clean Foundry image** before investing time in Kontrol proofs. + +## Further reading + +- [`` `kaas-cli run` `` command]({% link guides/kaas-cli_run_command.md %}) — all modes and shared flags +- [Foundry Book — `forge test`](https://book.getfoundry.sh/reference/forge/forge-test) diff --git a/guides/kaas-cli_remote_fuzzing.md b/guides/kaas-cli_remote_fuzzing.md new file mode 100644 index 0000000..adeeb02 --- /dev/null +++ b/guides/kaas-cli_remote_fuzzing.md @@ -0,0 +1,162 @@ +--- +title: Remote fuzzing +description: kaas go test and kaas-cli run for Go and Rust fuzzing on KaaS +--- + +# Remote Fuzzing on KaaS + +KaaS supports remote fuzzing for **Go** and **Rust** projects. Fuzz jobs run on cloud compute infrastructure, allowing long-duration fuzzing without blocking your local machine. + +Each fuzz target is submitted as a separate remote job, with up to 5 targets per invocation. Results are viewable on the [KaaS dashboard](https://kaas.runtimeverification.com/app). + +## Prerequisites + +- **`kaas-cli`** installed (`pip install kaas-cli` or `uv pip install kaas-cli`). The same package provides both the **`kaas-cli`** command and the **`kaas`** command group (e.g. `kaas go test`); you do not install them separately. +- A valid KaaS token ([create one here](https://kaas.runtimeverification.com/app/profile/keys)) +- A vault connected to your GitHub repository ([setup guide]({% link overview/kaas/kaas-web_setup.md %})) + +## `kaas go test` Command + +The `kaas go test` command provides a shorthand that mirrors the familiar `go test -fuzz` syntax. It submits Go fuzz tests to run remotely on KaaS infrastructure. + +### Basic Usage + +```bash +kaas go test -fuzz='^FuzzMyFunction$' ./path/to/pkg/ +``` + +### Multiple Targets + +Comma-separated targets each start a separate parallel job: + +```bash +kaas go test -fuzz='^FuzzTransfer$,^FuzzMint$' ./path/to/pkg/ +``` + +### Available Flags + +| Flag | Description | Default | +|------|-------------|---------| +| `--fuzz`, `-fuzz` | Comma-separated fuzz target patterns (required) | — | +| `--commit` | Pin a specific git commit hash | HEAD | +| `--fuzztime` | Go-style duration of at least `1m` (`'1m'`, `'5m'`, `'1h'`), converted to execution timeout | — | +| `--execution-timeout` | Execution timeout in minutes (mutually exclusive with `--fuzztime`) | 480 | +| `--vault-spec`, `-vs` | Vault specification in `org/vault` format | from config | +| `--token`, `-t` | Personal access key | from config | +| `--branch`, `-b` | Repository branch | `main` | +| `--go-version` | Go version | `latest` | +| `--go-build-directory` | Go build directory/pattern | `./...` | +| `--go-module-root` | Repo-relative directory containing `go.mod` (e.g. `src` for `golang/go`); optional, matches web **Go Module Root** | — | +| `--url`, `-u` | Server URL | `https://kaas.runtimeverification.com/` | +| `--watch`, `-w` | Watch job execution status | `false` | + +> **Info.** **`-fuzz` and `--fuzz` are equivalent** (short and long flag for the same option), matching Go’s usual `-flag` style and Click’s long options. Examples below use `-fuzz`; either form works. +> +> **`--fuzztime` and `--execution-timeout` are mutually exclusive.** Use `--fuzztime` for Go-style durations of at least `1m` (e.g. `5m`) or `--execution-timeout` for raw minutes. + +### Example with All Options + +```bash +kaas go test \ + -fuzz='^FuzzParseTransaction$' \ + ./pkg/parser/ \ + --commit abc123def \ + --fuzztime 2h \ + --vault-spec myorg/myrepo \ + --token "$KAAS_TOKEN" \ + --branch feature/my-branch \ + --go-version 1.23.8 +``` + +For a **`golang/go`** checkout, the main module is under **`src/`**. Use **`--go-module-root src`** and paths **relative to `src/`** for **`./pkg/parser`** and **`--go-build-directory`** (e.g. **`./html/template`**, not **`./src/html/template`**). + +## `kaas-cli run` with Go/Rust Fuzzing + +For more explicit control or Rust fuzzing, use the full `kaas-cli run` command. + +### Go Fuzzing + +`kaas-cli run` uses **`--test-root`** / **`-tr`** for the package path (relative to the repository root), **`--fuzz-targets`** (comma-separated, up to five remote jobs per invocation), and **`--execution-timeout`** in **minutes** (there is no `--fuzztime` on this command; use `kaas go test` if you prefer Go-style durations). + +```bash +kaas-cli run \ + --mode remote \ + --test-mode go \ + --vault-spec org/vault \ + --token "$KAAS_TOKEN" \ + --branch main \ + --test-root ./pkg/parser \ + --fuzz-targets "^FuzzTransfer$,^FuzzMint$" \ + --go-version 1.23.8 \ + --go-build-directory "./pkg/parser" \ + --execution-timeout 120 +``` + +### Rust Fuzzing + +Rust fuzzing supports `libfuzzer`, `afl`, and `hongfuzz` engines. + +```bash +kaas-cli run \ + --mode remote \ + --test-mode rust \ + --vault-spec org/vault \ + --token "$KAAS_TOKEN" \ + --branch main \ + --fuzz-targets "fuzz_transfer,fuzz_mint" \ + --rust-version stable \ + --rust-build-directory "." \ + --rust-fuzz-engine libfuzzer +``` + +### Rust-Specific Flags + +| Flag | Description | Default | +|------|-------------|---------| +| `--rust-version` | Rust toolchain version | `latest` | +| `--rust-build-directory` | Project directory containing `Cargo.toml` | `.` | +| `--rust-fuzz-engine` | Fuzzing engine: `libfuzzer`, `afl`, `hongfuzz` | `libfuzzer` | +| `--rust-fuzz-args` | Extra arguments passed to the fuzz engine | — | +| `--execution-timeout` | Timeout in minutes | `480` | + +## Configuration File (`.kaas-cli.toml`) + +The `kaas go test` command supports persistent configuration via a `.kaas-cli.toml` file in your project root. If no config exists, the CLI will interactively prompt you to create one. + +CLI flags always override config values. The file is automatically added to `.gitignore`. + +```toml +[default] +vault_spec = "org/vault" +token = "your-token" +branch = "main" +url = "https://kaas.runtimeverification.com/" + +[go] +go_version = "latest" +go_build_directory = "./..." +go_module_root = "" # optional, e.g. "src" for golang/go +execution_timeout = 480 +``` + +> **Warning.** The `.kaas-cli.toml` file contains your API token. It is automatically added to `.gitignore` to prevent accidental commits. + +## Viewing Results + +After submitting a fuzz job, the CLI outputs a dashboard URL for each job: + +``` +Started 2 go fuzz job(s): + [1] target: ^FuzzTransfer$ + jobId: abc123 + url: https://kaas.runtimeverification.com/app/organization/org/vault/job/abc123/dashboard + commit: def456 + [2] target: ^FuzzMint$ + jobId: xyz789 + url: https://kaas.runtimeverification.com/app/organization/org/vault/job/xyz789/dashboard + commit: def456 +``` + +Job statuses: `pending` → `running` → `success` / `failure` / `error` + +You can also view all jobs for a vault on the KaaS dashboard under your organization's compute tab. diff --git a/guides/kaas-cli_run_command.md b/guides/kaas-cli_run_command.md index 7ff94b4..dec195e 100644 --- a/guides/kaas-cli_run_command.md +++ b/guides/kaas-cli_run_command.md @@ -1,7 +1,12 @@ +--- +title: "`kaas-cli run` command" +description: Local, container, and remote test execution with kaas-cli +--- + # **`kaas-cli run` Command Documentation** ## **Description:** -The `kaas-cli run` command executes Kontrol proofs either locally, within a Docker container, or remotely on KaaS infrastructure. Kontrol is an open-source formal verification tool for Ethereum smart contracts, maintained by Runtime Verification ([Kontrol GitHub repository](https://github.com/runtimeverification/kontrol)). +The `kaas-cli run` command executes tests either locally, within a Docker container, or remotely on KaaS infrastructure. It supports multiple test modes including Kontrol (formal verification), Forge, Go fuzzing, and Rust fuzzing. ## **Requirements:** To run your tests you will need: @@ -11,9 +16,33 @@ OR OR - Docker must be installed locally. See [Docker documentation](https://docs.docker.com/get-docker/) for installation instructions. -- You must have at minimum a `foundry.toml` file at the root of you TEST directory. -- A `kontrol.toml` file is optional, but if present, it will be used to run the tests using specific configuraiton options passed to kontrol. - - `kontrol.toml` is a kontrol specific configuration file that can be used to specify additional options for the proof run, and manage what kontrol does or does not do. +**For Kontrol/Forge modes:** +- You must have at minimum a `foundry.toml` file at the root of your test directory. +- A `kontrol.toml` file is optional, but if present, it will be used to run the tests using specific configuration options passed to kontrol. + +**For Go/Rust fuzzing modes (remote only):** +- A valid **vault specification** and **token** are required. +- **`--branch`** is optional and defaults to `main` when omitted (same as other remote job types). +- Go fuzz tests must follow Go's `testing.F` convention (`FuzzXxx(f *testing.F)`). +- Rust fuzz tests require `cargo-fuzz` with a supported engine (libfuzzer, afl, hongfuzz). + +## **Test Modes:** + +`kaas-cli run` supports the following test modes via `--test-mode`: + +- **kontrol** (default): local, container, or remote execution +- **forge**: local or container execution only (**remote `forge` is not implemented** in the CLI; managed CI may still run **`--mode container --test-mode forge`** on KaaS workers). See [Foundry (`forge test`) with kaas-cli]({% link guides/kaas-cli_forge_test.md %}). +- **go**: remote execution only — runs Go fuzz tests +- **rust**: remote execution only — runs Rust fuzz tests + +Mode-specific flags: + +| Mode | Flags | +|------|-------| +| kontrol | `--build-only`, `--prove-only-profile`, `--kontrol-version`, `--kontrol-docker-image`, `--extra-build-args`, `--extra-prove-args` | +| forge | `--foundry-version`, `--foundry-docker-image`, `--extra-build-args`, `--extra-test-args` | +| go | `--fuzz-targets`, `--go-version`, `--go-build-directory`, `--execution-timeout` | +| rust | `--fuzz-targets`, `--rust-version`, `--rust-build-directory`, `--rust-fuzz-engine`, `--rust-fuzz-args`, `--execution-timeout` | ## **Usage:** @@ -22,7 +51,7 @@ kaas-cli run [OPTIONS] ``` Kaas CLI will attempt to run the tests within the current working directory. So long as a foundry.toml file is present, it will be used to run the tests. If no foundry.toml file is present, it will exit. -If a kontrol.toml file is present, it will be used to run the tests using specific configuraiton options passed to kontrol. +If a kontrol.toml file is present, it will be used to run the tests using specific configuration options passed to kontrol. If your execution directory for tests are within a subdirectory, either `cd` to that directory or use the `--test-root` flag to specify the path to the tests. @@ -35,11 +64,13 @@ If your execution directory for tests are within a subdirectory, either `cd` to **Key Options:** -- `--mode, -m`: Specifies the execution mode. Accepted values are `local`, `remote`, or `container`. +- `--mode, -m`: Specifies the execution mode. Accepted values are `local`, `remote`, or `container`. Behavior depends on `--test-mode` (default `kontrol`). - - **local**: Runs Kontrol proofs directly on the host machine. Requires Kontrol to be installed locally, see [Kontrol documentation](https://docs.runtimeverification.com/kontrol/overview/readme/installations) for installation instructions. - - **container**: Executes proofs inside a Docker container on the host machine, ensuring a consistent and isolated environment. - - **remote**: Submits proofs to KaaS remote compute infrastructure, requiring authentication and a valid vault specification. + - **local**: Runs tests on the host machine. For `--test-mode kontrol`, Kontrol must be installed locally; see [Kontrol documentation](https://docs.runtimeverification.com/kontrol/overview/readme/installations). + - **container**: Runs tests inside a Docker container on the host for a consistent environment (Kontrol in the image for kontrol mode, Foundry image for forge mode, etc.). + - **remote**: Runs tests on KaaS remote infrastructure; requires authentication and a valid vault specification (`--vault-spec`, `--token`). + +- `--test-mode, -tm`: Specifies the test runtime. Accepted values are `kontrol`, `forge`, `go`, `rust`. Default is `kontrol`. - `--watch, -w`: Monitors the job execution status. If set, waits until the job is completed, applicable in all modes. @@ -55,7 +86,7 @@ If your execution directory for tests are within a subdirectory, either `cd` to - `--vault-spec, -vs`: Required in `remote` mode. Specifies the vault in `/` format. -- `--token, -t`: A personal access key for authentication against the remote server. If not provided, you must authenticate using [environment variables](https://docs.runtimeverification.com/kaas/guides/kaas-cli_connecting-using-tokens#authentication-using-environment-variables) or [device flow authentication](https://docs.runtimeverification.com/kaas/guides/kaas-cli_connecting-using-device-flow). +- `--token, -t`: A personal access key for authentication against the remote server. If not provided, you must authenticate using [environment variables]({% link guides/kaas-cli_connecting-using-tokens.md %}#authentication-using-environment-variables) or [device flow authentication]({% link guides/kaas-cli_connecting-using-device-flow.md %}). - `--branch, -b`: (Optional) Specifies a Git branch for remote runs, aiding in reproducible CI/CD workflows. @@ -63,17 +94,21 @@ If your execution directory for tests are within a subdirectory, either `cd` to - `--extra-build-args, -eb`: Additional arguments passed directly to `kontrol build`. For available options, consult the [Kontrol Build Options](https://docs.runtimeverification.com/kontrol/glossary/kontrol-build-options) documentation. +- `--fuzz-targets`: (go/rust) Comma-separated list of fuzz targets (max 5). Each target starts a separate remote job. + +- `--execution-timeout`: (go/rust) Execution timeout in minutes. Default is 480 (8 hours). + ## **Execution Flow:** 1. **Local Mode:** - Calls `kontrol build` and `kontrol prove` directly on the host. Kontrol must be installed beforehand. If Kontrol is not found, the CLI will provide installation guidance ([Kontrol Documentation]( https://docs.runtimeverification.com/kontrol/overview/readme/installations)). + For **`--test-mode kontrol`**, calls `kontrol build` and `kontrol prove` on the host (Kontrol must be installed). For **`forge`**, runs Foundry tests locally. If Kontrol is not found in kontrol mode, the CLI surfaces installation guidance ([Kontrol documentation](https://docs.runtimeverification.com/kontrol/overview/readme/installations)). 2. **Container Mode:** - Runs on the host machine. Uses a Docker container to run `kontrol build` and `kontrol prove`. This ensures an isolated environment with Kontrol installed without modifying the host system. + Runs the selected test mode inside Docker on the host (e.g. Kontrol or Foundry in the configured image) without changing the host install. 3. **Remote Mode:** - Uses KaasClient to run proofs on the remote KaaS infrastructure. Requires `--vault-spec` and `--token`. If `--watch` is set, the CLI monitors the job until completion. + Submits work to KaaS. Requires `--vault-spec` and `--token`. If `--watch` is set, the CLI waits for completion where supported. For **Go** and **Rust** fuzzing, the CLI checks fuzzing capacity before submitting jobs. ## **Error Handling and Output:** @@ -87,8 +122,41 @@ ___ kaas-cli run --mode local --extra-build-args "--verbose" --extra-prove-args "--xml-test-report" ``` -**Example (Remote Mode):** +**Example (Remote Mode - Kontrol):** ```bash kaas-cli run --mode remote --vault-spec /: --token --watch ``` + +**Example (Remote Mode - Go Fuzzing):** + +```bash +kaas-cli run \ + --mode remote \ + --test-mode go \ + --vault-spec org/vault \ + --token "$KAAS_TOKEN" \ + --branch main \ + --fuzz-targets "^FuzzTransfer$,^FuzzMint$" \ + --go-version 1.23.8 \ + --go-build-directory "./..." +``` + +**Example (Remote Mode - Rust Fuzzing):** + +```bash +kaas-cli run \ + --mode remote \ + --test-mode rust \ + --vault-spec org/vault \ + --token "$KAAS_TOKEN" \ + --branch main \ + --fuzz-targets "fuzz_transfer,fuzz_mint" \ + --rust-version stable \ + --rust-build-directory "." \ + --rust-fuzz-engine libfuzzer +``` + +For the `kaas go test` shorthand and Go fuzzing details, see [Remote Fuzzing]({% link guides/kaas-cli_remote_fuzzing.md %}). + +For **`forge build` / `forge test`**, flags, Docker image selection, and **`foundry_test_report.json`**, see [Foundry (`forge test`) with kaas-cli]({% link guides/kaas-cli_forge_test.md %}). diff --git a/guides/kaas-cli_tagging-best-practices.md b/guides/kaas-cli_tagging-best-practices.md index 6433c7f..8ad6bc9 100644 --- a/guides/kaas-cli_tagging-best-practices.md +++ b/guides/kaas-cli_tagging-best-practices.md @@ -1,10 +1,11 @@ --- -description: Best Practices for Tagging KCFG Files +title: KCFG tagging +description: Tags, list-caches, download, and the web UI --- # KCFG Tagging Best Practices -After successfully [setting up and logging into the CLI](/guides/kaas-cli_connecting-using-tokens.md), you can view and download all previous versions of artifacts. +After successfully [setting up and logging into the CLI]({% link guides/kaas-cli_connecting-using-tokens.md %}), you can view and download all previous versions of artifacts. ### CLI @@ -28,15 +29,15 @@ kaas-cli download /: The webpage provides a list of available versions. To access this information, navigate to your "Dashboard" and click the eye button next to your preferred project. -
+*In the Dashboard, open a project and use the **eye** icon next to it to see the list of cached versions for that vault.* You will be redirected to a page with all available caches within the vault. -
+*That page lists each tagged cache; pick the version you need.* -Click the "Download" button to see the CLI command or download it in the browser. +Click the **Download** button to copy the suggested `kaas-cli download …` command or download the artifact in the browser. -
+*The download control shows the CLI command and any in-browser download option.* ## Options for Tagging diff --git a/guides/kaas_setting-up-ci.md b/guides/kaas_setting-up-ci.md index fcbb8c1..fdede86 100644 --- a/guides/kaas_setting-up-ci.md +++ b/guides/kaas_setting-up-ci.md @@ -1,4 +1,9 @@ -# Basic Github Workflow Setup for KaaS +--- +title: KaaS in CI +description: Example GitHub Actions workflow for KaaS +--- + +# Basic GitHub workflow setup for KaaS ```YAML --- @@ -39,7 +44,7 @@ # This mode will run proofs on Runtime Verification Servers using dedicated hardware built for proof execution. # A kontrol.toml and foundry.tom file are still requried to be present in the root of the test directory. - # Github App installation of "KaaS Storage & Compute" is required to use this mode to support access to test source code. + # GitHub App installation (Runtime Verification app: https://github.com/apps/runtime-verification-inc) is required for remote mode so KaaS can clone private repository source. - name: 'Run KaaS in Remote Mode' shell: bash run: | diff --git a/index.md b/index.md new file mode 100644 index 0000000..f229ced --- /dev/null +++ b/index.md @@ -0,0 +1,28 @@ +--- +title: KaaS +description: K as a Service — documentation home +permalink: / +--- + +# KaaS + +## Get started + +Introducing **KaaS** (**K** as a Service), a cloud-based solution designed to enhance the [**K** framework](https://kframework.org/) experience. **KaaS** is engineered to introduce new features, streamline operations, and foster collaboration among teams. By leveraging caching proofs and remote computation, it eliminates redundant processes, saving your team precious time. + +**KaaS** integrates seamlessly with continuous integration (CI) systems, allowing developers to pull the latest cached results and bypass repetitive computations. It is a strong fit for internal teams that want centralized, shared computational results. + +For data management, **KaaS** uses secure storage. User access is protected through project keys and organization membership. The **KaaS CLI** supports cache management and local, containerized, or remote proof execution. + +Cloud compute lets you offload heavy work to Runtime Verification infrastructure (including remote Kontrol and fuzzing workflows). + +With **KaaS**, the goal is to make the **K** framework more approachable and to streamline verification workflows for teams. + +## Next steps + +- [Organizations, Vaults & GitHub App]({% link overview/kaas/kaas-web_setup.md %}) — sign in, install the [GitHub App](https://github.com/apps/runtime-verification-inc), manage orgs and vaults, tokens +- [KaaS CLI installation]({% link overview/kaas/kaas-cli_installation.md %}) + +## Publish + +This site is built with **Jekyll** and deployed with **GitHub Actions** to **GitHub Pages**. After you enable Pages (source: GitHub Actions) and add a [custom domain](https://docs.github.com/en/pages/configuring-a-custom-domain-for-your-github-pages-site) if needed, the workflow on `main` will publish automatically. diff --git a/overview/kaas/kaas-cli_installation.md b/overview/kaas/kaas-cli_installation.md index 0050f0d..c97bd5f 100644 --- a/overview/kaas/kaas-cli_installation.md +++ b/overview/kaas/kaas-cli_installation.md @@ -1,3 +1,8 @@ +--- +title: KaaS CLI Installation +description: Install kaas-cli and local requirements +--- + # KaaS CLI Tool Installation Follow these step-by-step instructions to set up **KaaS** components, which include the web interface and command-line interface (CLI) tool. diff --git a/overview/kaas/kaas-web_setup.md b/overview/kaas/kaas-web_setup.md index 995eb95..f6815e3 100644 --- a/overview/kaas/kaas-web_setup.md +++ b/overview/kaas/kaas-web_setup.md @@ -1,124 +1,192 @@ -# Getting Started with KaaS --- +title: Organizations, Vaults & GitHub App +description: KaaS web app setup, organizations, vaults, and GitHub App installation +--- + +# KaaS Web: Organizations, Vaults & GitHub App + +This guide describes what the [KaaS web application](https://kaas.runtimeverification.com) does today, how **organizations** and **vaults** fit together, and the **recommended GitHub App** setup for private repositories and remote compute. + +--- + +## What you can do in KaaS -**Welcome to KaaS!** -This guide will help you navigate through the initial setup process, including signing up, creating your first organization, and setting up a vault. Follow these steps to get started: +| Area | What it is | Typical use | +|------|------------|-------------| +| **Vaults & caches** | A vault is a workspace tied to a project (often a GitHub repo). **Caches** store versioned proof artifacts (KCFG and related outputs) with tags. | Browse results in the UI, upload/download via [`kaas-cli`]({% link overview/kaas/kaas-cli_installation.md %}). | +| **Remote compute** | Jobs run on Runtime Verification infrastructure (e.g. Kontrol proofs, **Go/Rust fuzzing**). | Submit from the **Compute** tab or from the CLI (`kaas-cli run`, `kaas go test`). Requires a **vault spec** (`org/vault`) and **access token**. | +| **Local / container runs** | Proof workflows on your machine or in Docker. | [`kaas-cli run`]({% link guides/kaas-cli_run_command.md %}) in `local` or `container` mode; no GitHub App required for basic local use. | -## Step 1: Sign Up +**GitHub integration** is **required** for KaaS to clone **private** repositories when running **remote** jobs. It is **not** required only to use the CLI to **upload or download** cached artifacts to a vault you can already access. -1. **Access the KaaS Web App:** +--- - Open your web browser and navigate to the [KaaS web application](https://kaas.runtimeverification.com). +## Step 1: Sign up and sign in -2. **Create an Account:** +1. Open [KaaS](https://kaas.runtimeverification.com). +2. Choose **Login**. +3. **Sign in with GitHub (recommended)** — you are redirected to GitHub and back to the KaaS app. This is the smoothest path if you will use the GitHub App and remote compute. +4. **Email and password** — register, verify your email, then sign in. - - Click on the **Login** button on the homepage. +*Sign-in options on the KaaS homepage: **Login**, then **Sign in with GitHub** or email/password as described above.* - **Two Login Options:** - - **Login with Github (Recommended)** - - Click on the **Login with Github** button. - - You will be redirected to the Github login page. - - After logging in, you will be redirected back to KaaS Dashboard. +--- - - **Email/Password:** - - Fill in your details, including your email address and a secure password. - - Submit the form to create your account. - - Check your email inbox for a verification email from KaaS. - - ![Signin Page](/.gitbook/assets/SignInPage.png) - *Screenshot of the sign-in page with fields for email and password.* +## Step 2: Recommended setup — install the GitHub App -## Step 2: Create Your First Organization +For **private** repos and **remote** Kontrol or fuzz jobs, install Runtime Verification’s GitHub App on the GitHub **organization or user account** that owns those repositories. -1. **Log In to Your Account:** +**Install the app:** [github.com/apps/runtime-verification-inc](https://github.com/apps/runtime-verification-inc) - Use your credentials to log in to the KaaS web app. +During installation on GitHub you will: -2. **Navigate to Organizations:** - On first login you will be presented with a blank canvas. +1. Choose which **GitHub account or organization** the app is installed on. +2. Choose **all repositories** or only **selected** ones (you can change this later in GitHub’s app settings). - ![Blank Canvas](/.gitbook/assets/BlankCanvas.png) +After installation, return to KaaS. Newly linked installations are picked up when you open the app; if an organization does not appear yet, use **Refresh Organization List** on the Organizations page (or close and reopen the **Create Organization** / onboarding flow and complete the GitHub steps again). - If someone in your Github organization has already installed the ["Runtime Verification Inc." Github app](https://github.com/apps/runtime-verification-inc) to your organization. - It will already be listed on login. +**Onboarding in the app (summary):** -### After first login +1. From **Organizations**, choose **Get Started** or **Create Organization**. +2. Under **GitHub Integration Options**, choose **Install GitHub App** (connect GitHub). +3. Use **Install GitHub App** to open GitHub, complete installation, then **Continue** in the modal. +4. When GitHub organizations are linked to your user, they appear as **GitHub organizations** in the list (see below). - #### Add a Github Connected Organization. +> **Info.** Log into the **same GitHub account** that has access to the repositories you need. The onboarding copy in the app reminds you of this before you leave for GitHub. - Watch a brief tutorial video adding an organization using the Github App integration feature. - - +--- - {% embed url="https://app.screencast.com/JpRDbeTHhgRqs/e" %} +## Step 3: Organizations - **Additional Notes on Github Connected Organizations:** - - Github integration is required for remote compute execution. - - Github integration is NOT required for storing kcfgs to a vault. - - When selecting 'Add Organization' if your organization does not show up within a few seconds, Click "Install Github App" and make sure the app is installed for the organization. - - If your repository is not showing up in the list of repositories, Check the to baner message and follow the instructions. +### Types of organizations - **Troubleshooting Github Organization not showing:** - - If your organization is not showing on your hompage go back to 'Add Organization' - - From the Homepage. Click on 'Import from Github'. Top Right Corner of screen. - - Find your organization in the list and click on the link icon to the left of your organization name. - ![Link Organization](/.gitbook/assets/KaaS_Link_Organization_Icon.png) - *Screenshot of the Link Organization Icon.* +| Type | How it appears | Name pattern | +|------|----------------|--------------| +| **GitHub-linked** | Label: *GitHub Organization* | Matches the GitHub **login** (user or org), e.g. `mycompany`. **Does not** start with `@`. | +| **User-managed** | Label: *User-managed Organization* | **Must start with `@`**, e.g. `@my-team`. Use this if you want an organization **without** tying it to a GitHub org first. | - #### Create a Non Github Organization: +### Managing the organization list - - Click on the **Create New Organization** button. Top Right of screen. - - Enter the name of your organization. Must Start with '@' - - Click **Create** +Open **Organizations** in the app (`/app`). You can: -## Step 3: Set Up Your First Vault +- **Search** organizations by name. +- **Filter** by *All*, *GitHub Organizations*, or *User-managed Organizations*. +- Switch **grid** or **list** view. +- **Refresh** to reload organizations and GitHub installation data. -1. **Access the Vaults Tab:** +To add another **user-managed** organization: **Create Organization** → choose **Without GitHub Integration** → enter a name that **starts with `@`** (letters, digits, `_`, `-`, `.`). - Click on an Organization. Navigate to the **Vaults** tab. - ![Vaults Tab](/.gitbook/assets/VaultsTab.png) - *Screenshot of the Vaults tab.* +If you already installed the GitHub App but a GitHub org is missing, confirm the app is installed for that org on GitHub, grant access to the right repositories, then **Refresh Organization List** in KaaS. -2. **Connect a Github Repository as a KaaS Vault:** +*Organizations list empty state: prompts you to connect GitHub or create an organization.* - - Click on the **Connect Vault** button. - ![Connect Vault Button](/.gitbook/assets/KaaS_Connect_Vault_Button.png) - *Screenshot of the Connect Vault Button Found under the Vaults Tab.* - - Select the repository you want to Connect a Vault to. And click link **Connect Icon**. - ![Connect Vault Icon](/.gitbook/assets/ConnectVaultIcon.png) - *Screenshot of the Connect Vault Icon.* -
-
+#### Tutorial video (GitHub-connected organization) - **Troubleshooting Github Repo not showing in Organization List:** +[Open video on Screencast](https://app.screencast.com/JpRDbeTHhgRqs/e) - - If your repository is not showing up in the list of repositories, Check the to banner message and follow the instructions. - ![Github Repo not showing](/.gitbook/assets/AddVault_MissingGithubRepo.png) + +--- -3. **Adding a New Vault by Connecting a Github Repository:** +## Step 4: Vaults - A Tutorial on adding a new Github Connected Repository as a KaaS Vault and running a Kontrol Compute Job - - +A **vault** belongs to exactly one organization. The CLI and API refer to it as **`organization-name/vault-name`** (vault spec). - {% embed url="https://app.screencast.com/w6Bh2tD4hvu4E/e" %} +### Opening the Vaults tab - **Adding a Non Github Connected Vault:** - - From Organization > Vault Tab - - Click **Create Vault** - - Enter a Name. It must start with '@' - - Click **Create** button. +1. Click an **organization**. +2. Open the **Vaults** tab. -## Questions? +*Inside an organization, open the **Vaults** tab to see vaults for that org.* -If you have any questions or need further assistance, please refer to our support documentation or contact our support team. -[contact@runtimeverification.com](mailto:contact@runtimeverification.com) -[Join our Discord](https://discord.gg/UBq4J8NE) -[Find us on Twitter](https://twitter.com/rv_inc) +### Creating a vault (current UI) +Use the control to **create or add a vault** (for example **Add vault** / **Create a New Vault**). A modal offers: -# Next Steps -[Tagging Best Practices](/guides/tagging-best-practices.md) +1. **Connect GitHub Repository** (shown for **GitHub-linked** organizations) + - Uses your **GitHub App** installation. + - Pick from repositories the app can access (**private** and **public**). + - **Best for** your own orgs/repos where the app is installed. -You are now ready to start using KaaS to manage your projects efficiently. If you have any questions or need further assistance, please refer to our support documentation or contact our support team. \ No newline at end of file +2. **Connect Public Repository** (always available) + - Enter a **public** GitHub repository URL. + - **Best for** public repos that are **not** in your app installation. + +For **user-managed** organizations (`@my-org`), the modal only offers **Connect Public Repository** — private repos need a **GitHub-linked** organization with the GitHub App installed. + +### Vault naming rules (important) + +| Organization type | Vault name rule | +|-------------------|-----------------| +| **GitHub-linked** | Vault name **must start with `@`**, followed by allowed characters (letters, digits, `_`, `-`, `.`). | +| **User-managed** (`@org`) | Vault name **must not** start with `@`; use letters, digits, `_`, `-`, `.` only. | + +These rules match the forms in the KaaS web app. Use the exact **`org/vault`** pair shown in the UI when you pass `--vault-spec` to the CLI. + +### If a repository does not appear + +- Confirm the **GitHub App** is installed on the correct GitHub org/user and that the repo is included (all or selected). +- Read any **banner** at the top of the page for next steps. + +*If a repository is missing from the picker, check the GitHub App installation and repository access; the UI may show a banner with next steps.* + +#### Tutorial video (vault + compute) + +[Open video on Screencast](https://app.screencast.com/w6Bh2tD4hvu4E/e) + + + +--- + +## Step 5: Inside an organization + +Organization pages use tabs (some depend on your **plan** or **role**): + +| Tab | Purpose | +|-----|---------| +| **Overview** | Summary of the organization. | +| **Vaults** | List vaults; open a vault for caches and settings. | +| **Users** | Members and access. | +| **Compute** | Remote jobs for this org (when available for your account). | +| **Notifications** | Notification settings (eligible accounts). | +| **Credits / Subscription / Usage** | Billing and usage (typically **admin** views). | + +--- + +## Step 6: Inside a vault + +| Tab | Purpose | +|-----|---------| +| **Caches** | Versioned cached proof runs; open a cache for reports and KCFG views. | +| **Compute** | Jobs tied to this vault (when your account has access). | +| **Collaborators** | Who can access this vault. | + +--- + +## Step 7: Access tokens (CLI and API) + +1. Open your **Profile** (avatar menu). +2. Go to **Access Tokens** (or [Profile → keys](https://kaas.runtimeverification.com/app/profile#tokens)). +3. Create a token and store it securely (e.g. `KAAS_TOKEN`). + +**Admin keys** (where applicable) are managed under the separate **Admin** / admin-token section of the profile ([`#admin_tokens`](https://kaas.runtimeverification.com/app/profile#admin_tokens)). + +For CLI usage patterns, see [Connecting using tokens]({% link guides/kaas-cli_connecting-using-tokens.md %}) and [Device flow]({% link guides/kaas-cli_connecting-using-device-flow.md %}). + +--- + +## Related documentation + +- [KaaS CLI installation]({% link overview/kaas/kaas-cli_installation.md %}) +- [`kaas-cli run` command]({% link guides/kaas-cli_run_command.md %}) +- [Remote fuzzing]({% link guides/kaas-cli_remote_fuzzing.md %}) +- [CI / GitHub Actions]({% link guides/kaas_setting-up-ci.md %}) +- [KCFG tagging]({% link guides/kaas-cli_tagging-best-practices.md %}) + +--- + +## Questions? + +[contact@runtimeverification.com](mailto:contact@runtimeverification.com) +[Discord](https://discord.gg/CurfmXNtbN) +[Telegram](https://t.me/rv_kontrol)