Using Assertions

Our SDKs permit you to conveniently define test properties through writing assertions inline in your code. If you cannot use the SDK, you can still use our assertions framework by writing JSONL messages to $ANTITHESIS_OUTPUT_DIR/sdk.jsonl. These assertions will be recognized by our platform, which will evaluate the assertions and record the results in our reports.

You must emit JSONL messages. Each individual message must be a single line of JSON that terminates in a newline character. However, the examples show JSON messages spread across multiple lines purely for readability. This will not work in practice. Each message must be a single line.

You must write two messages in JSONL format per assertion: one for assertion declaration in the catalog at startup, and another for assertion evaluation when encountered during execution. An example of two such JSONL messages follows: the first declares a Sometimes Assertion at startup and the second later notes that the assertion has been encountered. Since you will be using your language of choice, the example is written in pseudocode and will differ from your implementation.

Assertion declaration: at program startup

fn startup (){
    # The SDK directory is $ANTITHESIS_OUTPUT_DIR/sdk.jsonl
    # but this only has meaning in bash
    output_path = getenv($ANTITHESIS_OUTPUT_DIR) + '/sdk.jsonl'
    sdk_capture_file = open(output_dir)

    # Create the declaration message
    # Most fields need to have the same value as in the evaluation below
    declaration = 
    {
        "antithesis_assert": {
            "hit": false,
            "must_hit": true,
            "assert_type": "sometimes",
            "display_type": "Sometimes",
            "message": "Server sometimes is leader",
            "condition": false,
            "id": "Server sometimes is leader",
            "location": {
                "class": "main",
                "function": "main",
                "file": "/src/glitch-grid/go/control.go",
                "begin_line": 239,
                "begin_column": 0
            },
            "details": null}
        }

    # Antithesis needs JSON to be on a single-line
    leader_assertion_declare = toJSON(declaration, newlines=FALSE)

    # Write the JSONL to the output dir
    sdk_capture_file.write(leader_assertion_declare)
    # The assertion has now been declared

    [More catalog declarations]
    # Keep writing other JSONL to the catalog here
    [Other startup code]
    ...
}

Assertion evaluation: during runtime

fn main(){
    startup()
    ...
    [Project code]
    # We would like to invoke the assertion at this point in the code.
    # We will test if the server is the leader.
    # We do not know if the test condition is true yet and we do not know the details yet.
    # Create the evaluation message
    evaluation =
    {
        "antithesis_assert": {
            "hit": true,
            "must_hit": true,
            "assert_type": "sometimes",
            "display_type": "Sometimes",
            "message": "Server sometimes is leader",
            "condition": null,
            "id": "Server sometimes is leader",
            "location": {
                "class": "main",
                "function": "main",
                "file": "/src/glitch-grid/go/control.go",
                "begin_line": 239,
                "begin_column": 0
            },
            "details": null
        }
    }

    # Imagine we have a method that returns true if the server is the leader
    evaluation.antithesis_assert.condition = server.isLeader()

    # You should only record the first true evaluation and
    # the first false evaluation of an assertion (see below)
    [code to check if assertion evaluation is redundant]
    # Suppose the assertion is not redundant so the message should be written

    # Get further details for logging with imaginary methods
    evaluation.antithesis_assert.details.priority_number = server.getPriorityNumber()
    evaluation.antithesis_assert.details.leader_start_time = server.getLeaderStartTime()


    # We have already opened the SDK capture file earlier
    # Antithesis needs JSON to be on a single line
    leader_assertion_evaluate = toJSON(evaluation, newlines=FALSE)
    sdk_capture_file.write(leader_assertion_evaluate)
    # The assertion will be evaluated when this is written.
    [Further project code]
    ...
}

The evaluation message might look like the following after details and condition are added:

{
    "antithesis_assert": {
        "hit": true,
        "must_hit": true,
        "assert_type": "sometimes",
        "display_type": "Sometimes",
        "message": "Server sometimes is leader",
        "condition": true,
        "id": "Server sometimes is leader",
        "location": {
            "class": "main",
            "function": "main",
            "file": "/src/glitch-grid/go/control.go",
            "begin_line": 239,
            "begin_column": 0
        },
        "details": {"priority_number": 0, "leader_start_time": "2024-03-09 10:30:05.008" }
    }
}

Syntax

A given assertion has the top-level key antithesis_assert, which has the the fields found below.

`hit`

Boolean. Indicates whether the assertion has been encountered yet or not. The declaration value is always different from the evaluation value: For declarations it is always false and for evaluations it is always true.

`must_hit`

Boolean. Indicates whether not hitting the assertion represents failure. It varies between different assertion functions: the combination of must_hit and assert_type determine what specific assertion function you are calling. The declaration value is always the same as the evaluation value.

`assert_type`

String, one of "always", "sometimes", or "reachability". It varies between different assertion functions: the combination of must_hit and assert_type determine what specific assertion function you are calling. The declaration value is always the same as the evaluation value.

`display_type`

String. Customizes the name of assertion types displayed in the details section of Antithesis reports. Users should generally use the Antithesis defaults, which this documentation consistently uses. The declaration value is always the same as the evaluation value.

`message`

String. A human-readable message that becomes the name of the corresponding test property. The declaration value is always the same as the evaluation value.

`condition`

Boolean. The result of evaluating the desired test condition. This is not normally hardcoded, but is rather evaluated at runtime. The declaration value might be different from the evaluation value: For declarations it is always false, and for evaluations it might be either true or false.

Assertions of assert_type: "reachability" do not have a test condition. Arbitrarily, this field is hardcoded to true for reachable function evaluation messages and false for unreachable function evaluation messages.

`id`

String. The identifier used to aggregate assertions. Antithesis generates one test property per unique id. This test property either passes or fails, which depends upon the evaluation of every assertion that shares its id. Different assertions in different parts of the code should have different id’s, but the same assertion should always have the same id even if it is moved to a different file. Antithesis uses message as id and customers should generally do the same. The declaration value is always the same as the evaluation value.

`location.class`

String. The class of the code in which the assertion is being called. If this field is not relevant for your language, use an empty string. The declaration value is always the same as the evaluation value.

`location.function`

String. The function in which the assertion is being called. If this field is not relevant for your language, use an empty string. The declaration value is always the same as the evaluation value.

`location.file`

String. The file in which the assertion is being called. The declaration value is always the same as the evaluation value.

`location.begin_line`

Integer. The line number of the assertion call. The declaration value is always the same as the evaluation value.

`location.begin_column`

Integer. The column number of the assertion call. If this field is not relevant for your language, use 0. The declaration value is always the same as the evaluation value.

`details`

Either JSON or null. Optional additional information provided by the user for the purpose of providing context for assertion failures. The declaration value might be different from the evaluation value: For declarations it is always null, and for evaluations it might be either null or the details you wish to log in JSON format. Note that details must not terminate with a newline, because the entire message must ultimately be JSONL.

Assertion declaration

A single assertion is declared by writing a JSONL message to $ANTITHESIS_OUTPUT_DIR/sdk.jsonl at startup. The collection of all such assertion declarations is called the assertion catalog.

The assertion catalog initializes the assertions. Many types of assertions are supposed to fail if they are never reached: Antithesis must be informed that that these assertions exist so it can mark them as failing if they are never encountered. The catalog should be written at program startup, to ensure that Antithesis is informed of all assertions before it (potentially) begins encountering them.

The assertion catalog is necessary for assertions to function correctly. However, Antithesis will attempt to evaluate every assertion it encounters even if the assertion wasn’t previously declared.

Assertions declarations use the same format as assertion evaluations (below). However, in declarations some fields must be set to specific values. The Syntax and Assertion Evaluation sections contain all the necessary information, and this section provides the same information more conveniently. The following are the initialization values for a function declaration:

The fields "id", "message", and "location" are the same both at declaration and at evaluation. These depend upon your program and are not given here.
The fields that must be set verbatim in declarations are different for different Assertion functions. These fields are given in the table below. Each row is a different Assertion function and the values its fields must take.

	hit	must_hit	assert_type	display_type	condition	details
Always	`false`	`true`	`"always"`	`Always`	`false`	`null`
AlwaysOrUnreachable	`false`	`false`	`"always"`	`AlwaysOrUnreachable`	`false`	`null`
Sometimes	`false`	`true`	`"sometimes"`	`Sometimes`	`false`	`null`
Unreachable	`false`	`false`	`"reachability"`	`Unreachable`	`false`	`null`
Reachable	`false`	`true`	`"reachability"`	`Reachable`	`false`	`null`

Assertion evaluation

An assertion is evaluated by writing a JSONL message to $ANTITHESIS_OUTPUT_DIR/sdk.jsonl at runtime. The result of a test property only depends upon if there is at least one true evaluation of the assertion and if there is at least one false evaluation of the assertion. There is no benefit to sending more than one true evaluation or more than one false evaluation. In your code, you should ensure that your evaluation message is not redundant before writing it.

The complete assertion schema is provided for reference or for validation.

Details of each assertion function follow.

Always

An Always assertion function asserts that a given condition is true every time the assertion is encountered and that it is encountered at least once. The corresponding test property will be viewable in the Antithesis SDK: Always group of your triage report.

You should have already declared the assertion in the catalog during startup. When you reach the point where you want to evaluate the assertion, emit a JSON message similar to the example below. The field details may either be null or may give details in JSON format. Note that details must not terminate with a newline, because the entire message must ultimately be JSONL.

To set condition you should evaluate the desired test condition in your language of choice and store the results in this field.