Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).

### Changed

- Require the runtime witness to retain the exact Edict-authored
`GreetingCreated { key, message }` result identity and canonical bytes through
generic Echo evaluation and to compare the applied, fresh-host, and
WAL-recovered result records exactly.
- Distinguished producer-satisfied review findings from stale or
unreproducible findings, bounded operator-authorized remediation without
resetting the autonomous budget, and made disposition-only closure
Expand Down
6 changes: 5 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,11 @@ The structured witness proves:
- one scheduler-selected Action in one atomic Tick;
- decided-Tick recovery of Action, Tick, state, outcome, and Receipt by
reopening that persisted WAL in another fresh host;
- successful greeting state derived from typed input;
- the exact package-declared
`examples.hello_echo@1.GreetingCreated { key, message }` result as canonical
evidence, including independent equality of the applied, fresh-host, and
WAL-recovered generic result records without native reconstruction;
- successful greeting state derived from the same typed input;
- package-declared `causal.cell@1.AlreadyExists` obstruction on duplicate
creation, with equal canonical application-state roots and typed target-value
digests independently demonstrating no hidden mutation;
Expand Down
16 changes: 11 additions & 5 deletions docs/roadmap.md
Original file line number Diff line number Diff line change
Expand Up @@ -70,20 +70,26 @@ Prove the existing compiler and runtime seam without external effects:
5. obstruct duplicate submission while exposing equal before/after
application-state roots and typed target-value digests;
6. refuse an altered pre-Tick basis; and
7. prove replay equivalence.
7. prove replay equivalence; and
8. retain the exact compiler-authored typed application result through
independent verification, scheduler evaluation, and WAL recovery.

Roadmap A ends when the standalone witness passes without a runtime fake,
native application callback, handwritten package, or host-checkout path.

The standalone witness now covers all seven steps with one Action in one Tick.
The standalone witness now covers all eight steps with one Action in one Tick.
The generic runner reopens one persisted WAL for pending and decided recovery;
the external suite separately proves byte-identical deterministic reruns from
the same empty-WAL basis. Duplicate no-mutation proof compares Echo-produced
graph-only application-state roots and typed target-value digests; it does not
mistake the legitimately extended WAL, Tick history, or Receipt evidence for
application mutation. This is a singleton scheduler proof, not a claim that the
permanent multi-Action Tick model is complete. Roadmap A.1 begins only after the
runtime witness lands on `main`.
application mutation. The application result remains the exact canonical
`GreetingCreated { key, message }` value declared by Edict; Echo reports and
recovers generic typed bytes without application-specific reconstruction. The
external suite independently requires the applied, fresh-host, and
WAL-recovered result records to be exactly equal. This is a singleton scheduler
proof, not a claim that the permanent multi-Action Tick model is complete.
Roadmap A.1 begins only after the runtime witness lands on `main`.

## Roadmap A.1 — Hello Effect

Expand Down
36 changes: 34 additions & 2 deletions tests/runtime.sh
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,9 @@ mkdir -p "$runtime_root"
package_file=.build/application/executable-operation-package.cbor
verification_report_file=.build/application/verification-report.cbor
lawpack_manifest_file=vendor/causal-cell/manifest.cbor
expected_package_sha256=67dc6d23e223e78b6aa774a2f57c86db2eff4981ea793975d39c66f731f02fd1
expected_verification_report_sha256=8a5153b4ec25ebe979f0ceab373d03969e30a64d7973b3a83e3c84877c5aa564
typed_result_fixtures=tests/typed-result-fixtures.json
expected_package_sha256=3665d692cdd120f116f18067f2fd583e841448d057b5e35515f57264f853d0f6
expected_verification_report_sha256=2541c8263d95fdad52f4f5a3bbfed48fdefd9f20969156c3c3fd56be912b66dd
expected_lawpack_manifest_sha256=7bb901c984a92ed50795f8b5f7efe8d0648124574fa82250c6373a30e94333c9

sha256_file() {
Expand Down Expand Up @@ -55,6 +56,12 @@ assert_common_witness() {
--arg lawpack_manifest_sha256 "$lawpack_manifest_sha256" \
'
.operation == "examples.hello_echo@1.createGreeting"
and .applicationResult.projectionIdentity
== "791fb36bb4d42273eb558ce4d03d68d90a678d15891fb9cbe4ad8a20bb56fa82"
and .applicationResult.outputType
== "examples.hello_echo@1.GreetingCreated"
and (.applicationResult.canonicalBytesHex | test("^([0-9a-f]{2})+$"))
and (.applicationResult.resultIdentity | test("^[0-9a-f]{64}$"))
Comment thread
flyingrobots marked this conversation as resolved.
Comment thread
coderabbitai[bot] marked this conversation as resolved.
and .artifacts.package.algorithm == "sha256"
and .artifacts.package.digestHex == $package_sha256
and .artifacts.verificationReport.algorithm == "sha256"
Expand All @@ -69,6 +76,9 @@ assert_common_witness() {
and .recovery.stateRecovered == true
and .recovery.outcomeRecovered == true
and .recovery.receiptRecovered == true
and .recovery.applicationResultRecovered == true
and .recovery.freshHostApplicationResult == .applicationResult
and .recovery.walApplicationResult == .applicationResult
and .recovery.mutatedInitialStateRefusal == "echo-operation-execution-mismatch/action-basis"
and .duplicate.obstruction == "causal.cell@1.AlreadyExists"
and (.duplicate.applicationStateRootBefore | test("^[0-9a-f]{64}$"))
Expand All @@ -94,10 +104,23 @@ assert_common_witness() {
' "$witness" >/dev/null
}

assert_typed_result() {
witness=$1
case_name=$2
expected_result=$(jq -e --arg case_name "$case_name" '.[$case_name]' \
"$typed_result_fixtures")
jq -e \
--argjson expected_result "$expected_result" \
'.applicationResult.canonicalBytesHex == $expected_result.canonicalBytesHex
and .applicationResult.resultIdentity == $expected_result.resultIdentity' \
"$witness" >/dev/null
}

# Golden path: exact compiler output enters the generic durable runner.
run_case golden tests/create-greeting.json
golden_witness="$runtime_root/golden/witness.json"
assert_common_witness "$golden_witness"
assert_typed_result "$golden_witness" golden
jq -e '
.causalSite.basis == "u0"
and .causalSite.nodeKey == "greeting"
Expand All @@ -110,6 +133,12 @@ jq -e '
run_case deterministic-rerun tests/create-greeting.json
cmp "$golden_witness" "$runtime_root/deterministic-rerun/witness.json"

# A stale golden result cannot satisfy another case's application-owned fixture.
if assert_typed_result "$golden_witness" property-1; then
echo "golden result unexpectedly satisfied the first property case" >&2
exit 1
fi

# The witness is portable evidence and must not disclose checkout paths.
edict_repo_root=$(CDPATH='' cd -- "$EDICT_REPO" && pwd -P)
echo_repo_root=$(CDPATH='' cd -- "$ECHO_REPO" && pwd -P)
Expand Down Expand Up @@ -159,6 +188,7 @@ jq -n --arg value "$(jq -nr '"x" * 256')" \
>"$runtime_root/maximum-input.json"
run_case maximum "$runtime_root/maximum-input.json"
assert_common_witness "$runtime_root/maximum/witness.json"
assert_typed_result "$runtime_root/maximum/witness.json" maximum
test "$(jq -r '.state.valueUtf8 | length' "$runtime_root/maximum/witness.json")" -eq 256

jq -n --arg value "$(jq -nr '"x" * 257')" \
Expand Down Expand Up @@ -197,6 +227,7 @@ do
run_case "$property_name" "$property_input"
property_witness="$runtime_root/$property_name/witness.json"
assert_common_witness "$property_witness"
assert_typed_result "$property_witness" "$property_name"
jq -e \
--arg basis "$property_name" \
--arg key "key-$property_ordinal" \
Expand All @@ -221,6 +252,7 @@ while test "$stress_ordinal" -le "$stress_count"; do
>"$stress_input"
run_case "$stress_name" "$stress_input"
assert_common_witness "$runtime_root/$stress_name/witness.json"
assert_typed_result "$runtime_root/$stress_name/witness.json" "$stress_name"
stress_ordinal=$((stress_ordinal + 1))
done

Expand Down
54 changes: 54 additions & 0 deletions tests/typed-result-fixtures.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
{
"golden": {
"canonicalBytesHex": "a2636b6579686772656574696e67676d6573736167656a48656c6c6f204563686f",
"resultIdentity": "bfc50f30e68ac57742ef0fb0ccc41506c1af4a9ecdeca32c0b934a1adccb9860"
},
"maximum": {
"canonicalBytesHex": "a2636b6579676d6178696d756d676d65737361676579010078787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878787878",
"resultIdentity": "23a35065ba12e133c9654b4b0a7fe7f672ec1670415545d252c8442dfc8e1ca3"
},
"property-1": {
"canonicalBytesHex": "a2636b6579656b65792d31676d65737361676570736565642d36393630332d616c706861",
"resultIdentity": "6837506000b2639bf7508e9dd4847393d19764dfebacb94a7a152cd50fde293e"
},
"property-2": {
"canonicalBytesHex": "a2636b6579656b65792d32676d6573736167657827736565642d36393630332d73706163657320616e642070756e6374756174696f6e3a205b5d7b7d",
"resultIdentity": "c98cd1e33957be688161806dd778c9c010ebb55d152f1ba905b313ce2b6279cf"
},
"property-3": {
"canonicalBytesHex": "a2636b6579656b65792d33676d65737361676575736565642d36393630332d756e69636f64652dcea9",
"resultIdentity": "7d35e3a66bd948a31c2cd6bfd677152be9f17c5d952e2bb164462ad4222997cc"
},
"stress-1": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d31676d6573736167656c48656c6c6f204563686f2031",
"resultIdentity": "d843deac03c618c1a5ba8062ea044e12e0c1915aff018a2947ba3643be5b7d17"
},
"stress-2": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d32676d6573736167656c48656c6c6f204563686f2032",
"resultIdentity": "ad211b1f6ba8b864543a68a7640b7f399b8d3d8c912cb852e139db94431765d3"
},
"stress-3": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d33676d6573736167656c48656c6c6f204563686f2033",
"resultIdentity": "e7b71532a260d7923427f0750963b7e1637233e98728c5ca5c9adf8bd6b5b138"
},
"stress-4": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d34676d6573736167656c48656c6c6f204563686f2034",
"resultIdentity": "a56aca24544811874ceb682c50998454c2d2778a5ea6849a0f1c2cdc293a71ac"
},
"stress-5": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d35676d6573736167656c48656c6c6f204563686f2035",
"resultIdentity": "a84d156aa97622794c2b4705ef624caf3a9b6ee652dc4a09dd8b701d21f382bd"
},
"stress-6": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d36676d6573736167656c48656c6c6f204563686f2036",
"resultIdentity": "65f87332356d98ef69a331f2aa5318bb9f3ed1b110cf9b16fcd97c1c97004411"
},
"stress-7": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d37676d6573736167656c48656c6c6f204563686f2037",
"resultIdentity": "0312fea260f2b2f33c806871274cc1499a9e2d11a9812c0f759435596337892d"
},
"stress-8": {
"canonicalBytesHex": "a2636b65796a6772656574696e672d38676d6573736167656c48656c6c6f204563686f2038",
"resultIdentity": "f20f7aa1532ca315ebda57d2ce2b0b69b023e3514e2e94941690f04ecae5a7de"
}
}