@@ -179,11 +179,11 @@ We commit the `DeploymentSummary.sol` and `DeploymentSummaryCode.sol` contracts,
...
@@ -179,11 +179,11 @@ We commit the `DeploymentSummary.sol` and `DeploymentSummaryCode.sol` contracts,
### Kontrol Proof Execution using KaaS (Kontrol as a Service) & CI Integration
### Kontrol Proof Execution using KaaS (Kontrol as a Service) & CI Integration
To execute compute intensive Symbolic Kontrol proofs in a CI pipeline, we leverage KaaS (Kontrol as a Service) & CircleCI.
To execute compute intensive Symbolic Kontrol proofs in a CI pipeline, we leverage KaaS (Kontrol as a Service) & CircleCI.
On each execution a status is returned to the commit checks the execution was run from. The checks for a commit provides a "Details" link to the execution KCFG arrtifacts and kontrol proof summary results. See below for further infromation on how to fetch these artifacts from the summary using the Github API.
On each execution a status is returned to the commit checks the execution was run from. The checks for a commit provides a "Details" link to the execution KCFG artifacts and kontrol proof summary results. See below for further information on how to fetch these artifacts from the summary using the Github API.
A high level overview of the CI Setup is defined in CircleCI and configured within [.circleci/config.yml](../../../../.circleci/config.yml). The CirlceCI flow calls on the Github API to execute Kontrol test proofs utilzing the [test scripts](scripts/run-kontrol.sh) in this repo. CircleCI is configured with a Github fine-grained token provided by Runtime Verification to leverage better machines than available in CircleCI to run Kontrol proofs. The token needed is stored in the CircleCI project as a secret.
A high level overview of the CI Setup is defined in CircleCI and configured within [.circleci/config.yml](../../../../.circleci/config.yml). The CirlceCI flow calls on the Github API to execute Kontrol test proofs utilizing the [test scripts](scripts/run-kontrol.sh) in this repo. CircleCI is configured with a Github fine-grained token provided by Runtime Verification to leverage better machines than available in CircleCI to run Kontrol proofs. The token needed is stored in the CircleCI project as a secret.
The proofs can be run manually using the Github Fine-grained token and providing the appropriate parameters outlind in the below Github API call.
The proofs can be run manually using the Github Fine-grained token and providing the appropriate parameters outlined in the below Github API call.
```bash
```bash
curl -X POST \
curl -X POST \
-H"Accept: application/vnd.github+json"\
-H"Accept: application/vnd.github+json"\
...
@@ -200,7 +200,7 @@ The proofs can be run manually using the Github Fine-grained token and providing
...
@@ -200,7 +200,7 @@ The proofs can be run manually using the Github Fine-grained token and providing
}
}
}'
}'
```
```
NOTE: Making this call manually and providng a sha will overrite an existing statuses sha commit. It will not remove the history from RV's end but will be removed from the commit checks table in a PR or in the commit statuses.
NOTE: Making this call manually and providing a sha will override an existing statuses sha commit. It will not remove the history from RV's end but will be removed from the commit checks table in a PR or in the commit statuses.
Parameters to be replaced are:
Parameters to be replaced are:
-**RV_COMPUTE_TOKEN**: The token used to authenticate to the KaaS service.
-**RV_COMPUTE_TOKEN**: The token used to authenticate to the KaaS service.
