🥮 mooncakes.io
    Sign in

    typesafe-sdk-moonbit

    Community MoonBit SDK for TypeSafe System One (Jev): typed Noul/Choice/Score questions, formally verified confidence gates and retry policy, and network-free testing.

    typesafe
    jev
    system-one
    ai
    sdk
    Download zip
    Version
    0.2.0
    License
    MIT
    Repository
    Last updated
    9 hours ago
    Downloads
    14

    No dependencies

    #typesafe-sdk-moonbit

    CI License: MIT

    Community MoonBit SDK for the TypeSafe System One API (Jev) — typed Noul / Choice / Score questions, formally verified confidence gates and retry policy, and network-free testing.

    Independent community project. Not affiliated with or endorsed by TypeSafe AI.

    #Why this SDK exists

    Every System One integration eventually hand-writes the same three pieces of policy code: confidence gates, token budgets, and retry backoff. This SDK proves them instead of hoping:

    • moon prove (Why3 + Z3) discharges every decision core's contract — 6 goals, 0 timeouts, including budget dominance: an exhausted token budget blocks the decision at any confidence level, and fail-open never silently blocks while fail-closed never green-lights.
    • Gate math uses integer basis points (1.0 = 10000 bp), keeping every verified function inside the decidable linear-integer fragment. The public API still speaks Double probabilities via to_bp / from_bp.

    Verified cores live in src/verified/verified.mbt (dependency-free and Map-free by design so the Why3 module stays decidable); gates.mbt / retry.mbt are thin enum-typed wrappers.

    #Status

    v0.2. Covered: Noul, Choice, Score, and Box (image) questions via base64 assets — the TypeSafe-Danger-Zone-Images header is sent automatically when the request carries assets; Retry-After in both delay-seconds and IMF-fixdate form (HTTP-date resolved against an injected clock; dates in the past mean retry immediately); asynchronous retries through a callback-based AsyncTransport (plus a fetch + setTimeout binding for JS targets); request encoding; response decoding; status classification; exponential backoff; scripted sync and async mock transports. Not covered: multipart part-based image assets (base64 only), the two deprecated Retry-After date formats (RFC 850, asctime), and language-level async (callbacks instead).

    #Breaking changes in 0.2 (from 0.1)

    • SystemOneRequest gained an assets field — prefer the SystemOneRequest::make builder over struct literals.
    • evaluate_once / evaluate_with_retries / classify_response take a now_secs : () -> Int clock (needed for HTTP-date Retry-After).
    • parse_retry_after takes (header, now_secs); "0" now means Some(0) (retry immediately) instead of None.
    • In delay_ms, "no directive" is now any negative value; 0 is a directive meaning zero delay.

    #Install

    Once published to mooncakes:

    moon add huanguan-Q/typesafe-sdk-moonbit

    Until then, use a git path dependency in your moon.mod import block.

    #Quick start

    // 1) Build a typed request.
    let questions : Map[String, Question] = Map([])
    questions.set(
      "billing",
      Question::NoulQ({ instructions: "Is this message about billing?", yes_when: None, no_when: None }),
    )
    let request : SystemOneRequest =::{
      model: "jev-latest",
      state: "I was charged twice for my subscription.",
      questions,
    }

    // 2) Call the API through any transport — in production a real HTTP
    //    client wrapped in `Transport`, in tests a `Transport::scripted`.
    let (transport, calls) = Transport::scripted([/* ... */])
    let config = ClientConfig::make(api_key=env_key)
    let result = evaluate_with_retries(
      config,
      transport,
      request,
      fn(ms) { sleep(ms) }, // injected timer: tests pass a recorder instead
    )

    // 3) Gate the answer with verified policy.
    match result {
      Ok(response) =>
        match response.answers.get("billing") {
          Some(Answer::NoulA(probability)) => {
            let verdict = noul_gate(to_bp(probability), 9000, 1000)
            let decision = decide(
              to_bp(probability),
              9000,                    // confidence threshold: 0.9
              response.usage.input_tokens,
              10000,                   // token budget for this workflow
            )
            // verdict / decision drive routing, escalation, or a hard stop.
          }
          _ => ()
        }
      Err(SdkError::RateLimited(retry_after)) => () // classified, retry-aware
      Err(_) => ()
    }

    Run the no-network demo: moon run cmd/main.

    #JS targets (browser / Node / Deno / workers)

    // import "huanguan-Q/typesafe-sdk-moonbit/src/fetch"
    // check/build with: moon check --target js
    evaluate_async(config, request, fn(result) { /* callback */ })

    Shipping an API key to a browser exposes it to every user; proxy through your own backend in production web apps.

    #Verified properties

    FunctionTheorem (all discharged by Z3)
    decide_codeBlocked ⟺ over budget; Proceed ⟺ in budget ∧ confidence ≥ threshold; Escalate ⟺ in budget ∧ below threshold. Budget dominates any confidence.
    noul_gate_codeEach verdict code ⟺ its probability band.
    on_failure_codeBlocked ⟺ fail-closed; never Proceed — a transport failure never yields a green light.
    should_retryExactly attempts_done < max_retries.
    exp_delayResult stays within [d, 2·max]; overflow-safe for max ≤ 2³⁰−1.
    delay_msAny directive (≥ 0, including 0 = immediate) is honored exactly; without one the delay stays within [base, max].

    Reproduce: moon prove → expect 1 of 1 packages proved, 6 goals proved (22 tests, library coverage > 90%). Full chain: moon check && moon test && moon build && moon prove.

    #Network-free testing

    Transport::scripted answers from a list (last entry repeats) and records every request — the whole SDK, including retry timing and headers, is tested without sockets. See typesafe-sdk-moonbit_test.mbt (16 tests).

    #Data egress

    • Calling the real API sends your state and question texts — and, for box questions, the base64 image bytes in assets — to https://api.typesafe.ai over HTTPS, authorized by your API key sent as a bearer header.
    • The SDK itself makes no other network calls and includes no telemetry.
    • Everything in this repository's tests and demo runs offline against scripted responses.

    Keep API keys out of client-side code and out of version control; read them from your environment or secret store.

    #License

    MIT. Not affiliated with TypeSafe AI; TypeSafe and Jev are trademarks of their respective owners.

    Answer

    source
    pub(all) enum Answer {
      NoulA(Double)
      ChoiceA(String, Double, Map[String, Double])
      ScoreA(Double, Double, Map[String, String], Map[String, Double])
      BoxA(BoxCoords, Double?)
    } derive(
    Debug    )

    A model answer. Its shape matches the question it was created from.

    Answer::to_repr

    source

    AsyncTransport

    source
    pub(all) struct AsyncTransport {
      deliver : (HttpRequest, (Result[HttpResponse, TransportError]) -> Unit) -> Unit
    }

    Asynchronous transport: deliver takes a completion callback, so non-blocking HTTP clients (fetch, XHR, worker messaging) adapt without blocking a thread.

    AsyncTransport::scripted

    source

    Build a scripted async transport for network-free tests: responses are consumed in order and the last one repeats, with every request recorded.

    BoxCoords

    source
    pub(all) struct BoxCoords {
      top : Double
      bottom : Double
      left : Double
      right : Double
    } derive(
    Debug    )

    Box edges as fractions of image height/width, 0 to 1. Vertical from the top, horizontal from the left.

    BoxCoords::to_repr

    source

    BoxQuestion

    source
    pub(all) struct BoxQuestion {
      instructions : String
    } derive(
    Debug    )

    Box question: locate what the instructions describe in an image asset referenced by placeholder. Answers are normalized edge coordinates.

    BoxQuestion::to_repr

    source

    ChoiceQuestion

    source
    pub(all) struct ChoiceQuestion {
      instructions : String
      options : Map[String, String]
    } derive(
    Debug    )

    Choice question: pick one named option. The answer carries the selected option, a confidence value, and the full probability distribution.

    ChoiceQuestion::to_repr

    source

    ClientConfig

    source
    pub(all) struct ClientConfig {
      api_key : String
      model : String
      base_url : String
      retry : RetryPolicy
    } derive(
    Debug    )

    Client configuration. Keep api_key server-side in production web apps; shipping it to a browser exposes it to users.

    ClientConfig::make

    source
    fn ClientConfig::make(api_key~ : String, model? : String, base_url? : String, retry? : RetryPolicy) -> ClientConfig

    Create a config with defaults: jev-latest, https://api.typesafe.ai, and the default retry policy.

    ClientConfig::to_repr

    source

    Decision

    source
    pub(all) enum Decision {
      Proceed
      Escalate
      Blocked
    } derive(Eq, 
    Debug    )

    Combined decision: confidence threshold plus token budget plus policy.

    Decision::equal

    source
    fn Decision::equal(Decision, Decision) -> Bool

    Decision::not_equal

    source
    fn Decision::not_equal(x : Decision, y : Decision) -> Bool

    Decision::to_repr

    source

    FailPolicy

    source
    pub(all) enum FailPolicy {
      FailOpen
      FailClosed
    } derive(Eq, 
    Debug    )

    What to do when the transport or API fails outright. FailOpen lets the action continue under human review; FailClosed stops it.

    FailPolicy::equal

    source
    fn FailPolicy::equal(FailPolicy, FailPolicy) -> Bool

    FailPolicy::not_equal

    source
    fn FailPolicy::not_equal(x : FailPolicy, y : FailPolicy) -> Bool

    FailPolicy::to_repr

    source

    GateVerdict

    source
    pub(all) enum GateVerdict {
      Proceed
      Escalate
      Reject
    } derive(Eq, 
    Debug    )

    Verdict of a standalone gate evaluation.

    GateVerdict::equal

    source
    fn GateVerdict::equal(GateVerdict, GateVerdict) -> Bool

    GateVerdict::not_equal

    source
    fn GateVerdict::not_equal(x : GateVerdict, y : GateVerdict) -> Bool

    GateVerdict::to_repr

    source

    HttpRequest

    source
    pub(all) struct HttpRequest {
      url : String
      http_method : String
      headers : Map[String, String]
      body : String
    } derive(
    Debug    )

    An outbound HTTP request. Header keys are expected to be lowercased.

    HttpRequest::to_repr

    source

    HttpResponse

    source
    pub(all) struct HttpResponse {
      status : Int
      headers : Map[String, String]
      body : String
    } derive(
    Debug    )

    An HTTP response. Header keys should be lowercased by the transport so lookups like retry-after are case-insensitive.

    HttpResponse::ok_json

    source
    fn HttpResponse::ok_json(body : String) -> HttpResponse

    200 OK with a JSON body.

    HttpResponse::rate_limited

    source
    fn HttpResponse::rate_limited(retry_after_secs : String) -> HttpResponse

    429 Too Many Requests with a Retry-After header in seconds.

    HttpResponse::rate_limited_raw

    source
    fn HttpResponse::rate_limited_raw(retry_after : String) -> HttpResponse

    429 Too Many Requests with an arbitrary Retry-After header value (delay-seconds or IMF-fixdate form).

    HttpResponse::server_error

    source
    fn HttpResponse::server_error(status : Int) -> HttpResponse

    A 5xx server error with the given status.

    HttpResponse::to_repr

    source

    ImageAsset

    source
    pub(all) struct ImageAsset {
      format : String
      data_base64 : String
    } derive(
    Debug    )

    An image asset, keyed by an opaque placeholder you reference from state or question text. Base64 form only: multipart part-based assets are not supported in v0.2. Image data is sent to the API (see README data egress).

    ImageAsset::to_repr

    source

    NoulQuestion

    source
    pub(all) struct NoulQuestion {
      instructions : String
      yes_when : String?
      no_when : String?
    } derive(
    Debug    )

    Noul question: a yes/no judgment. The model answers with the probability of yes in [0, 1].

    NoulQuestion::to_repr

    source

    Question

    source
    pub(all) enum Question {
      NoulQ(NoulQuestion)
      ChoiceQ(ChoiceQuestion)
      ScoreQ(ScoreQuestion)
      BoxQ(BoxQuestion)
    } derive(
    Debug    )

    A question value. Box questions locate a region in an image asset and require the TypeSafe-Danger-Zone-Images header, which the client sends automatically when the request carries assets.

    Question::to_repr

    source

    RetryPolicy

    source
    pub(all) struct RetryPolicy {
      max_retries : Int
      base_delay_ms : Int
      max_delay_ms : Int
    } derive(
    Debug    )

    Retry configuration. max_retries counts retries after the first attempt.

    RetryPolicy::defaults

    source
    fn RetryPolicy::defaults() -> RetryPolicy

    Sensible defaults: 2 retries, 500 ms base delay, 30 s cap.

    RetryPolicy::to_repr

    source

    ScoreQuestion

    source
    pub(all) struct ScoreQuestion {
      instructions : String
      levels : Array[String]
    } derive(
    Debug    )

    Score question: rate against an ordered rubric. Level position determines its score starting at zero; the answer is the probability-weighted expected score (may fall between levels).

    ScoreQuestion::to_repr

    source

    SdkError

    source
    pub(all) enum SdkError {
      Network(String)
      RateLimited(Int?)
      Server(Int, String)
      InvalidRequest(Int, String)
      Decode(String)
    } derive(
    Debug    )

    SDK-level error after transport, HTTP status classification, and decoding.

    SdkError::to_repr

    source

    SystemOneRequest

    source
    pub(all) struct SystemOneRequest {
      model : String
      state : String
      questions : Map[String, Question]
      assets : Map[String, ImageAsset]
    } derive(
    Debug    )

    System One request: the model alias, the shared state, the named question set, and optional image assets. Question names are yours; the response reuses them.

    SystemOneRequest::make

    source
    fn SystemOneRequest::make(model~ : String, state~ : String, questions~ : Map[String, Question]) -> SystemOneRequest

    Build a request with no image assets.

    SystemOneRequest::to_repr

    source

    SystemOneResponse

    source
    pub(all) struct SystemOneResponse {
      model : String
      answers : Map[String, Answer]
      usage : Usage
    } derive(
    Debug    )

    System One response: the model that answered, per-question answers, and token usage for the whole request.

    SystemOneResponse::to_repr

    source

    Transport

    source
    pub(all) struct Transport {
      deliver : (HttpRequest) -> Result[HttpResponse, TransportError]
    }

    Pluggable HTTP transport. Wrap any client into the deliver closure.

    Transport::scripted

    source
    fn Transport::scripted(responses : Array[Result[HttpResponse, TransportError]]) -> (Transport, Array[HttpRequest])

    Build a scripted transport for network-free tests: responses are consumed in order and the last one repeats. Returns the transport together with a call log recording every request it saw.

    TransportError

    source
    pub(all) enum TransportError {
      NetworkFailure(String)
    } derive(
    Debug    )

    Transport-level failure: DNS, connection, timeout, and similar errors that carry no HTTP status.

    TransportError::to_repr

    source

    Usage

    source
    pub(all) struct Usage {
      input_tokens : Int
      output_tokens : Int
    } derive(
    Debug    )

    Token usage reported by the API. Input tokens are billable; output tokens are currently free of charge.

    Usage::to_repr

    source

    build_http_request

    source
    fn build_http_request(config : ClientConfig, request : SystemOneRequest) -> HttpRequest

    Build the outbound HTTP request for a System One call: bearer auth, JSON content type, and the TypeSafe-Danger-Zone-Images header whenever the request carries image assets.

    classify_response

    source
    fn classify_response(response : HttpResponse, now_secs : Int) -> Result[SystemOneResponse, SdkError]

    Classify an HTTP response into a decoded SystemOneResponse or an SdkError: 200 decodes, 429 extracts Retry-After (seconds or HTTP-date, resolved against now_secs), 5xx is retryable, other statuses are invalid requests.

    days_from_civil

    source
    fn days_from_civil(year : Int, month : Int, day : Int) -> Int

    Days since 1970-01-01 for a civil (proleptic Gregorian) date — Howard Hinnant's days_from_civil, valid for years >= 1. Pure integer arithmetic, runtime-tested against known epochs.

    decide

    source
    fn decide(confidence_bp : Int, threshold_bp : Int, tokens_used : Int, token_budget : Int) -> Decision

    Combined decision from an answer's confidence and the caller's token budget, in basis points. See decide_code for the verified properties.

    decide_code

    source
    fn decide_code(confidence_bp : Int, threshold_bp : Int, tokens_used : Int, token_budget : Int) -> Int

    Verified core of decide: 0 = Proceed, 1 = Escalate, 2 = Blocked. The contract (including budget dominance) is discharged by Z3 in the src/verified package.

    decode_response

    source
    fn decode_response(body : String) -> Result[SystemOneResponse, SdkError]

    Decode a System One response body. Answer names are matched back to the question names you chose; unknown shapes surface as SdkError::Decode.

    delay_ms

    source
    fn delay_ms(base_delay_ms : Int, max_delay_ms : Int, attempt : Int, retry_after_secs : Int) -> Int

    Delay in milliseconds before the next retry.

    A Retry-After directive (retry_after_secs >= 0, where 0 means retry immediately) is honored exactly: retry_after_secs * 1000 ms, even when it exceeds max_delay_ms. Without a directive (negative value), the delay is exponential backoff from base_delay_ms, capped at max_delay_ms. The three theorems are discharged by Z3 in the src/verified package.

    encode_request_to_string

    source
    fn encode_request_to_string(request : SystemOneRequest) -> String

    Encode a request to its JSON wire form.

    evaluate_once

    source
    fn evaluate_once(config : ClientConfig, transport : Transport, request : SystemOneRequest, now_secs : () -> Int) -> Result[SystemOneResponse, SdkError]

    Perform exactly one evaluate call through a blocking transport.

    evaluate_with_retries

    source
    fn evaluate_with_retries(config : ClientConfig, transport : Transport, request : SystemOneRequest, sleep_ms : (Int) -> Unit, now_secs : () -> Int) -> Result[SystemOneResponse, SdkError]

    Evaluate with retries over a blocking transport. sleep_ms and now_secs are injected so tests run with zero waiting, a fixed clock, and full observability; a real app passes its own timer and clock. Retries follow the verified policy: a Retry-After directive (seconds or HTTP-date) is honored exactly, otherwise exponential backoff capped at max_delay_ms.

    evaluate_with_retries_async

    source
    fn evaluate_with_retries_async(config : ClientConfig, transport : AsyncTransport, request : SystemOneRequest, sleep_async : (Int, () -> Unit) -> Unit, now_secs : () -> Int, on_done : (Result[SystemOneResponse, SdkError]) -> Unit) -> Unit

    Evaluate with retries over an asynchronous transport. Completion is delivered to on_done; sleep_async(ms, wake) schedules the retry delay (tests pass an immediate scheduler); now_secs resolves HTTP-date Retry-After headers. The retry policy is the same verified core as the blocking path.

    from_bp

    source
    fn from_bp(bp : Int) -> Double

    Convert basis points back to a probability, clamped to [0, 1].

    is_retryable

    source
    fn is_retryable(err : SdkError) -> Bool

    Whether an SdkError is transient and worth retrying: network failures, 429 rate limits, and 5xx server errors. Validation and decode errors are not retryable.

    noul_gate

    source
    fn noul_gate(noul_bp : Int, high_bp : Int, low_bp : Int) -> GateVerdict

    Two-threshold gate for Noul (probability-of-yes) answers, in basis points. At or above high_bp → Proceed; at or below low_bp → Reject; strictly between → Escalate (uncertain band).

    noul_gate_code

    source
    fn noul_gate_code(noul_bp : Int, high_bp : Int, low_bp : Int) -> Int

    Verified core of noul_gate: 0 = Proceed, 1 = Escalate, 2 = Reject. The contract is discharged by Z3 in the src/verified package.

    on_failure_code

    source
    fn on_failure_code(fail_closed : Bool) -> Int

    Verified core of on_transport_failure: 1 = Escalate, 2 = Blocked. The contract is discharged by Z3 in the src/verified package.

    on_transport_failure

    source
    fn on_transport_failure(policy : FailPolicy) -> Decision

    Decision to take when the transport or API failed and no answer exists. FailOpen escalates to human review; FailClosed blocks.

    parse_http_date_secs

    source
    fn parse_http_date_secs(raw : String) -> Int?

    Parse an IMF-fixdate — Wed, 21 Oct 2015 07:28:00 GMT, a fixed-width 29-character format — into seconds since the Unix epoch. The two deprecated date formats (RFC 850, asctime) are not accepted.

    parse_retry_after

    source
    fn parse_retry_after(header : String?, now_secs : Int) -> Int?

    Parse a Retry-After response header (RFC 9110 §10.2.3). Accepts both forms: delay-seconds ("120"; "0" means retry immediately) and IMF-fixdate ("Wed, 21 Oct 2015 07:28:00 GMT"), resolved against now_secs — a date already in the past yields Some(0), never a negative delay. Returns None when the header is absent or unparseable.

    retry_allowed

    source
    fn retry_allowed(policy : RetryPolicy, attempts_done : Int) -> Bool

    Convenience wrapper: policy-aware should_retry.

    should_retry

    source
    fn should_retry(attempts_done : Int, max_retries : Int) -> Bool

    Whether another retry is allowed after attempts_done attempts. The contract is discharged by Z3 in the src/verified package.

    to_bp

    source
    fn to_bp(probability : Double) -> Int

    Convert a probability in [0, 1] to basis points, rounding to nearest. Values outside [0, 1] are clamped.

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io