9dd7faa3e3
A pipeline example that composes EVERY methodology-layer standard into a
single certified release — the thesis "vibe coding you can take to an
auditor" made executable:
spec-coverage : 2/2 clauses · complete=true (joule-code-spec)
review : two-stage, independent → approved (joule-code-review)
contract : postcondition PROVED via z3 + frame (joulecontract-proof
in-footprint → gate green + joule-code-joulecontract)
attested-build: verified
→ ✓ CERTIFIED · every clause traces to a proof, an approval, a metered build
The contract gate is the honest composition of its two halves: the formal
postcondition ("if debits==credits then net==0") discharged through z3 over
the JouleProof cascade (a real machine-checked proof, ~1.3 J), AND the frame
checked structurally (the ops' edits stayed in the declared footprint) —
because a frame is a footprint obligation, not a proof goal. Both, or the
gate is red.
Then the other terminal state: pull the independent reviewer (the author
reviews their own op) and separation-of-duties voids it → the same release
is REFUSED, naming [review]. Two outcomes, no third.
The cross-standard deps (joulecontract, proof) are dev-only, so a downstream
consumer of joule-code-release stays light. Runnable:
`cargo run -p joule-code-release --example pipeline` (needs z3 for the
contract gate; without it the postcondition is honestly unproved and the
release refuses — never a faked pass).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
28 lines
1.2 KiB
TOML
28 lines
1.2 KiB
TOML
[package]
|
|
name = "joule-code-release"
|
|
version.workspace = true
|
|
edition.workspace = true
|
|
license.workspace = true
|
|
repository.workspace = true
|
|
rust-version.workspace = true
|
|
|
|
[dependencies]
|
|
joule-code-schema = { workspace = true }
|
|
joule-code-spec = { workspace = true }
|
|
joule-code-review = { workspace = true }
|
|
ed25519-dalek = { workspace = true }
|
|
serde = { workspace = true }
|
|
thiserror = { workspace = true }
|
|
|
|
[dev-dependencies]
|
|
joule-code-cargo = { workspace = true }
|
|
# The end-to-end pipeline example composes every methodology-layer standard:
|
|
# spec + ops + reviews (above) plus the contract (structural frame check and a
|
|
# real z3 postcondition discharge). All dev-only, so a downstream consumer of
|
|
# joule-code-release stays light.
|
|
joule-code-joulecontract = { path = "../joule-code-joulecontract" }
|
|
joulecontract-schema = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-schema" }
|
|
joulecontract-proof = { path = "../../../../joulecontract/joulecontract-rs/crates/joulecontract-proof" }
|
|
proof-cascade = { path = "../../../../proof/proof-rs/crates/proof-cascade" }
|
|
proof-schema = { path = "../../../../proof/proof-rs/crates/proof-schema" }
|
|
proof-solvers = { path = "../../../../proof/proof-rs/crates/proof-solvers" }
|