Standard library
Every function below is written in Sabline, in stdlib/, and read onto this page by the compiler itself, contracts included. A violated requires is a compile error at your call site.
aws.vel #
Requests signed with Signature Version 4, in Sabline, to S3 and STS. The secret key stays a Secret: the signature is one hmac_sha256_chain call, which the audit lists as a declassification with the reason "hmac signature". Grant the region's hosts, clock and declassify; example: examples/ops/aws_buckets.vel.
fn aws.credentials_from_env(region: Text) -> AwsCredentials uses declassify, env
fn aws.signature(creds: AwsCredentials, service: Text, amz_date: Text, method: Text, path: Text, query: List of Text, headers: List of Text, payload_hash: Text) -> Text uses declassify
fn aws.authorization(creds: AwsCredentials, service: Text, amz_date: Text, signed: Text, headers: List of Text) -> Text
fn aws.send(creds: AwsCredentials, service: Text, host: Text, method: Text, path: Text, query: List of Text, body: Text, content_type: Text) -> AwsReply or fail uses clock, declassify, net
fn aws.expect_ok(reply: AwsReply) -> AwsReply or fail
fn aws.s3_host(creds: AwsCredentials) -> Text
fn aws.s3_list_buckets(creds: AwsCredentials) -> List of Text or fail uses clock, declassify, net
fn aws.s3_list_objects(creds: AwsCredentials, bucket: Text, prefix: Text, most_pages: Int) -> List of Text or fail uses clock, declassify, net
fn aws.s3_get_object(creds: AwsCredentials, bucket: Text, key: Text) -> Text or fail uses clock, declassify, net
fn aws.s3_put_object(creds: AwsCredentials, bucket: Text, key: Text, text: Text) -> Int or fail uses clock, declassify, net
fn aws.s3_delete_object(creds: AwsCredentials, bucket: Text, key: Text) -> Int or fail uses clock, declassify, net
fn aws.sts_caller_identity(creds: AwsCredentials) -> Text or fail uses clock, declassify, net
fn aws.no_query() -> List of Text
fn aws.canonical_path(path: Text) -> Text
fn aws.header_names(headers: List of Text) -> Text
fn aws.joined(parts: List of Text, with: Text) -> Text
fn aws.take(text: Text, n: Int) -> Text
fn aws.two(n: Int) -> Text
fn aws.amz_date_of(epoch: Int) -> Text
fn aws.xml_values(body: Text, tag: Text) -> List of Text
fn aws.first_value(body: Text, tag: Text) -> Text
fn aws.swapped(text: Text, old: Text, new: Text) -> Text
fn aws.unescaped(text: Text) -> Text
azure.vel #
Azure Resource Manager over REST: GET, PUT, PATCH and DELETE on management.azure.com, paging, ARM's error shape. The bearer token is the caller's, a Secret of Text. Grant net:management.azure.com:443 and declassify; example: examples/ops/azure_groups.vel.
fn azure.send(token: Secret of Text, method: Text, path: Text, body: Text, attempts: Int) -> AzureReply or fail uses declassify, net
fn azure.next_path(body: Text) -> Text
fn azure.expect_ok(reply: AzureReply) -> AzureReply or fail
fn azure.error_of(reply: AzureReply) -> Text
fn azure.read(token: Secret of Text, path: Text) -> AzureReply or fail uses declassify, net
fn azure.put_resource(token: Secret of Text, path: Text, body: Text) -> AzureReply or fail uses declassify, net
fn azure.patch_resource(token: Secret of Text, path: Text, body: Text) -> AzureReply or fail uses declassify, net
fn azure.delete_resource(token: Secret of Text, path: Text) -> AzureReply or fail uses declassify, net
fn azure.list(token: Secret of Text, path: Text, most_pages: Int) -> List of Text or fail uses declassify, net
fn azure.resource_groups(token: Secret of Text, subscription: Text) -> List of Text or fail uses declassify, net
fn azure.worth_retrying(status: Int) -> Bool
fn azure.items(body: Text, path: Text) -> List of Text or fail
fn azure.after_prefix(text: Text, prefix: Text) -> Text or fail
fn azure.no_leading_slash(path: Text) -> Text
csv.vel #
fn csv.fields(line: Text) -> List of Text
ensures length(result) >= 1
fn csv.quoted_field(value: Text) -> Text
fn csv.line_of(values: List of Text) -> Text
fn csv.column(line: Text, at: Int) -> Text or fail
fn csv.column_int(line: Text, at: Int) -> Int or fail
fn csv.rows_of(text: Text) -> List of Text
ensures length(result) >= 1
dates.vel #
fn dates.days_in(year: Int, month: Int) -> Int
requires month >= 1
requires month <= 12
ensures result >= 28
ensures result <= 31
fn dates.make(year: Int, month: Int, day: Int) -> Date or fail
fn dates.parse(text: Text) -> Date or fail
fn dates.text_of(d: Date) -> Text
fn dates.before(a: Date, b: Date) -> Bool
fn dates.same(a: Date, b: Date) -> Bool
fn dates.next_day(d: Date) -> Date or fail
requires d.month >= 1
requires d.month <= 12
fn dates.today() -> Date or fail uses ffi
db.vel #
fn db.open(path: Text) -> Handle or fail uses ffi
fn db.run(conn: Handle, sql: Text) -> Text or fail uses ffi
fn db.commit(conn: Handle) or fail uses ffi
fn db.rows_json(conn: Handle, sql: Text) -> Text or fail uses ffi
fn db.count(conn: Handle, table: Text) -> Int or fail uses ffi
ensures result >= 0
fn db.close(conn: Handle) uses ffi
env_tools.vel #
fn env_tools.setting(name: Text, fallback: Text) -> Secret of Text uses env
fn env_tools.public_setting(name: Text, fallback: Text) -> Text uses declassify, env
fn env_tools.number_setting(name: Text, fallback: Int) -> Int uses declassify, env
fn env_tools.succeed() uses io
fn env_tools.give_up(why: Text) uses io
github.vel #
The GitHub REST API: repositories, issues, pull requests, check runs, releases and file contents, with paging, and the rate limit as a failure that says when it resets. Grant net:api.github.com:443 and declassify; example: examples/ops/github_issues.vel.
fn github.send(token: Secret of Text, method: Text, path: Text, body: Text, attempts: Int) -> GithubReply or fail uses declassify, net
fn github.expect_ok(reply: GithubReply) -> GithubReply or fail
fn github.message_of(reply: GithubReply) -> Text
fn github.read(token: Secret of Text, path: Text) -> GithubReply or fail uses declassify, net
fn github.list(token: Secret of Text, path: Text, most_pages: Int) -> List of Text or fail uses declassify, net
fn github.repo(token: Secret of Text, owner: Text, name: Text) -> Text or fail uses declassify, net
fn github.repos_of(token: Secret of Text, owner: Text) -> List of Text or fail uses declassify, net
fn github.issues(token: Secret of Text, owner: Text, name: Text, state: Text) -> List of Text or fail uses declassify, net
fn github.create_issue(token: Secret of Text, owner: Text, name: Text, title: Text, body: Text) -> Text or fail uses declassify, net
fn github.create_comment(token: Secret of Text, owner: Text, name: Text, number: Int, body: Text) -> Text or fail uses declassify, net
fn github.pulls(token: Secret of Text, owner: Text, name: Text, state: Text) -> List of Text or fail uses declassify, net
fn github.pull(token: Secret of Text, owner: Text, name: Text, number: Int) -> Text or fail uses declassify, net
fn github.check_runs(token: Secret of Text, owner: Text, name: Text, ref: Text) -> List of Text or fail uses declassify, net
fn github.releases(token: Secret of Text, owner: Text, name: Text) -> List of Text or fail uses declassify, net
fn github.latest_release(token: Secret of Text, owner: Text, name: Text) -> Text or fail uses declassify, net
fn github.file_text(token: Secret of Text, owner: Text, name: Text, path: Text, ref: Text) -> Text or fail uses declassify, net
fn github.header_int(raw: Text, name: Text, lowered: Text) -> Int
fn github.next_path(raw: Text) -> Text
fn github.items(body: Text, path: Text) -> List of Text or fail
fn github.after_prefix(text: Text, prefix: Text) -> Text or fail
fn github.no_leading_slash(path: Text) -> Text
http.vel #
fn http.get(url: Text) -> Text or fail uses net
fn http.status(url: Text) -> Int or fail uses net
ensures result >= 0
fn http.ok(url: Text) -> Bool or fail uses net
fn http.send(url: Text, body: Text) -> Text or fail uses net
fn http.get_json(url: Text, path: Text) -> Text or fail uses net
fn http.call(method: Text, url: Text, body: Text, headers: Text) -> Answer or fail uses net
fn http.body_of(answer: Answer) -> Text
fn http.code_of(answer: Answer) -> Int
fn http.header_of(answer: Answer, name: Text) -> Text or fail
fn http.get_with(url: Text, headers: Text) -> Text or fail uses net
fn http.post_json(url: Text, body: Text) -> Text or fail uses net
k8s.vel #
The Kubernetes API over REST: list, get and watch-once for the core resources, the in-cluster service-account token read as a Secret. It reads; every function that changes the cluster begins write_. Grant your API server's host and declassify; example: examples/ops/k8s_pods.vel.
fn k8s.cluster(server: Text, token: Secret of Text) -> K8sCluster
fn k8s.in_cluster() -> K8sCluster or fail uses fs
fn k8s.in_cluster_namespace() -> Text or fail uses fs
fn k8s.first_line(text: Secret of Text) -> Secret of Text
fn k8s.send(c: K8sCluster, method: Text, path: Text, body: Text, content_type: Text, attempts: Int) -> K8sReply or fail uses declassify, net
fn k8s.expect_ok(reply: K8sReply) -> K8sReply or fail
fn k8s.status_of(reply: K8sReply) -> Text
fn k8s.read(c: K8sCluster, path: Text) -> Text or fail uses declassify, net
fn k8s.list(c: K8sCluster, path: Text, most_pages: Int) -> List of Text or fail uses declassify, net
fn k8s.namespaces(c: K8sCluster) -> List of Text or fail uses declassify, net
fn k8s.nodes(c: K8sCluster) -> List of Text or fail uses declassify, net
fn k8s.pods(c: K8sCluster, namespace: Text) -> List of Text or fail uses declassify, net
fn k8s.pod(c: K8sCluster, namespace: Text, name: Text) -> Text or fail uses declassify, net
fn k8s.services(c: K8sCluster, namespace: Text) -> List of Text or fail uses declassify, net
fn k8s.configmaps(c: K8sCluster, namespace: Text) -> List of Text or fail uses declassify, net
fn k8s.events(c: K8sCluster, namespace: Text) -> List of Text or fail uses declassify, net
fn k8s.deployments(c: K8sCluster, namespace: Text) -> List of Text or fail uses declassify, net
fn k8s.deployment(c: K8sCluster, namespace: Text, name: Text) -> Text or fail uses declassify, net
fn k8s.watch_once(c: K8sCluster, path: Text, resource_version: Text, seconds: Int) -> List of Text or fail uses declassify, net
fn k8s.write_create(c: K8sCluster, path: Text, body: Text) -> Text or fail uses declassify, net
fn k8s.write_patch(c: K8sCluster, path: Text, merge_patch: Text) -> Text or fail uses declassify, net
fn k8s.write_delete(c: K8sCluster, path: Text) -> Text or fail uses declassify, net
fn k8s.write_scale(c: K8sCluster, namespace: Text, name: Text, replicas: Int) -> Text or fail uses declassify, net
log.vel #
fn log.info(message: Text) uses io
fn log.warn(message: Text) uses io
fn log.error(message: Text) uses io
fn log.field(name: Text, value: Text) -> Text
fn log.event(name: Text, details: Text) uses io
fn log.die(message: Text) uses io
fn log.fail_with(message: Text) uses io
money.vel #
fn money.not_negative(m: Money of C) -> Bool for any C
fn money.not_positive(m: Money of C) -> Bool for any C
fn money.split(amount: Money of C, ways: Int) -> List of Money of C for any C
requires ways > 0
ensures length(result) == ways
ensures units_of(result) == units_of(amount)
ensures units_of(amount) < 0 or all_of(result, not_negative)
ensures units_of(amount) > 0 or all_of(result, not_positive)
rest.vel #
What a program that talks to a REST API needs beside http.vel: a request asked again within a bound, JSON bodies, headers from a map, the items of a JSON list (8.5).
fn rest.call(method: Text, url: Text, body: Text, headers: Text) -> RestAnswer or fail uses net
fn rest.header_of(answer: RestAnswer, name: Text) -> Text or fail
fn rest.header_map(of: Map of Text to Text) -> Text
fn rest.call_json(method: Text, url: Text, body: Text, extra: Map of Text to Text) -> RestAnswer or fail uses net
fn rest.worth_retrying(code: Int) -> Bool
fn rest.succeeded(answer: RestAnswer) -> Bool
fn rest.call_retrying(method: Text, url: Text, body: Text, headers: Text, attempts: Int) -> RestAnswer or fail uses net
fn rest.items(body: Text, path: Text) -> List of Text or fail
fn rest.after_prefix(text: Text, prefix: Text) -> Text or fail
fn rest.no_leading_slash(path: Text) -> Text
std.vel #
fn first(xs: List of T) -> T for any T
requires length(xs) > 0
fn last(xs: List of T) -> T for any T
requires length(xs) > 0
fn reverse(xs: List of T) -> List of T for any T
fn index_of(xs: List of T, item: T) -> Int for any T
fn contains_item(xs: List of T, item: T) -> Bool for any T
fn apply_to_each(xs: List of T, f: fn(T) -> T) -> List of T for any T
fn keep_if(xs: List of T, keep: fn(T) -> Bool) -> List of T for any T
fn count_where(xs: List of T, keep: fn(T) -> Bool) -> Int for any T
fn sum_of(xs: List of Int) -> Int
fn max_of(xs: List of Int) -> Int
requires length(xs) > 0
ensures contains_item(xs, result)
fn min_of(xs: List of Int) -> Int
requires length(xs) > 0
ensures contains_item(xs, result)
fn is_sorted(xs: List of Int) -> Bool
fn insert_sorted(xs: List of Int, v: Int) -> List of Int
fn sort(xs: List of Int) -> List of Int
ensures length(result) == length(xs)
ensures is_sorted(result)
fn insert_by(xs: List of T, v: T, key: fn(T) -> Int) -> List of T for any T
fn sort_by(xs: List of T, key: fn(T) -> Int) -> List of T for any T
ensures length(result) == length(xs)
fn join(xs: List of Text, sep: Text) -> Text
fn range_list(a: Int, b: Int) -> List of Int
fn map_to(xs: List of T, f: fn(T) -> R) -> List of R for any T, R
ensures length(result) == length(xs)
time.vel #
fn time.today() -> Text or fail uses ffi
fn time.clock_text() -> Text or fail uses ffi
fn time.seconds() -> Int uses clock
fn time.day_of(when: Text) -> Text or fail
fn time.year_of(date: Text) -> Int or fail
fn time.month_of(date: Text) -> Int or fail
fn time.day_number(date: Text) -> Int or fail
Built-in functions #
| Name | Effects | Takes | Gives |
|---|---|---|---|
add_or_fail or fail | pure | Int, Int | Int |
all_of | pure | Any, Any | Bool |
any_of | pure | Any, Any | Bool |
args | io | List of Text | |
ask | io | Text | Text |
base64_decode or fail | pure | Text | Text |
base64_encode | pure | Text | Text |
chars | pure | Text | List of Text |
code_at | pure | Text, Int | Int |
contains | pure | Text, Text | Bool |
declassify | declassify | Secret of T, Text | T |
div_or_fail or fail | pure | Int, Int | Int |
divide_or_fail or fail | pure | Money of C, Int, Text | Money of C |
env | env | Text, Text | Secret of Text |
exit_with | io | Int | Unit |
fetch or fail | net | Text | Text |
fetch_status or fail | net | Text | Int |
file_exists | fs | Text | Bool |
format | pure | Any | Text |
get | pure | Any, Any | Any |
get_or | pure | Any, Any, Any | Any |
has | pure | Any, Any | Bool |
hex_decode or fail | pure | Text | Text |
hex_encode | pure | Text | Text |
hmac_sha256 | declassify | Secret of Text, Text | Text |
hmac_sha256_chain | declassify | Secret of Text, List of Text | Text |
json_float or fail | pure | Text, Text | Float |
json_get or fail | pure | Text, Text | Text |
json_has | pure | Text, Text | Bool |
json_int or fail | pure | Text, Text | Int |
json_len or fail | pure | Text, Text | Int |
json_of | pure | Any | Text |
keys | pure | Any | Any |
length | pure | Any | Int |
log | io | Any | Unit |
lower | pure | Text | Text |
mod_or_fail or fail | pure | Int, Int | Int |
money | pure | Int, Text | Money of that currency |
mul_or_fail or fail | pure | Int, Int | Int |
now | clock | Int | |
parse_money or fail | pure | Text, Text | Money of that currency |
percent_of | pure | Money of C, Int, Int, Text | Money of C |
pop or fail | pure | Any | Any |
post or fail | net | Text, Text | Text |
print | io | Any | Unit |
push | pure | Any, Any | Any |
put | pure | Any, Any, Any | Any |
py or fail | ffi | Text, Text, List of Text | Text |
py_close | ffi | Handle | Unit |
py_do or fail | ffi | Handle, Text, Text | Text |
py_field or fail | ffi | Handle, Text | Text |
py_float or fail | ffi | Text, Text, List of Text | Float |
py_int or fail | ffi | Text, Text, List of Text | Int |
py_json or fail | ffi | Text, Text, Text | Text |
py_new or fail | ffi | Text, Text, Text | Handle |
random | rand | Int | Int |
read_file or fail | fs | Text | Text |
read_file_secret or fail | fs | Text | Secret of Text |
read_line | io | Text | |
request or fail | net | Text, Text, Text, Text | Text |
round | pure | Float | Int |
set_at or fail | pure | Any, Int, Any | Any |
sha256 | pure | Text | Text |
slice or fail | pure | Any, Int, Int | Any |
split | pure | Text, Text | List of Text |
sub_or_fail or fail | pure | Int, Int | Int |
text_of | pure | Money of C | Text |
to_float | pure | Int | Float |
to_int or fail | pure | Text | Int |
to_text | pure | Any | Text |
tool or fail | tool | Text, Text | Text |
tool_secret or fail | tool | Text, Text | Secret of Text |
units_of | pure | Money of C, or List of Money of C | Int |
upper | pure | Text | Text |
url_encode | pure | Text | Text |
with_units | pure | Money of C, Int | Money of C |
write_file | fs | Text, Any | Unit |
get on a map can also fail (missing key); get_or never fails.