feat(spec/test): Model-based tests for part streaming #814

stojanovic00 · 2025-01-28T17:32:55Z

Document proposal part streaming quint specification
Document proposal part streaming implementation
Remove redundant state variables (=> update invariants)
Add concrete tests in quint spec
- Fix symbolinc link from mbt/test to specs
Generate and parse itf-trace

Closes: #763

* Document proposal part streaming quint specification * Document proposal part streaming implementation * Remove redundant state variables (=> update invariants) * Add concrete tests in quint spec * Fix symbolinc link from mbt/test to specs * Generate and parse itf-trace

* supplemented missing proto files to test-mempool * added Buffer parsing * all invariant checks

codecov · 2025-02-03T11:09:44Z

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 76.12%. Comparing base (fec4b6e) to head (73a4400).
Report is 2 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #814      +/-   ##
==========================================
+ Coverage   75.87%   76.12%   +0.24%     
==========================================
  Files         172      175       +3     
  Lines       14785    14905     +120     
==========================================
+ Hits        11218    11345     +127     
+ Misses       3567     3560       -7

Flag	Coverage Δ
integration	`75.87% <ø> (+0.28%)`	⬆️
mbt	`8.52% <ø> (-6.14%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Components	Coverage Δ
core	`∅ <ø> (∅)`
engine	`∅ <ø> (∅)`
app	`∅ <ø> (∅)`
starknet	`∅ <ø> (∅)`

stojanovic00 · 2025-02-03T13:44:54Z

Update and expand the documentation of the code and the spec
Extend the spec with new tests and invariants
- Fix runtime bugs and remove redundant invariants
Write in Rust the types and data structures that will be used to map the spec's state variables
Write MBT test, which generates ITF traces from the Quint spec and runs the traces as Rust tests
- Update/fix symbolic link from test/mbt to specs
Write implementation of ItfRunner for ITF traces generated from the spec
- Fix dependency issues with used crates
Integrate the new MBT tests in CI

Closes: #763

code/crates/engine/src/util/streaming.rs

code/crates/starknet/host/src/streaming.rs

code/crates/test/mempool/proto/google/protobuf/any.proto

romac

Left some minor comments, looks great otherwise! 🚀

Will do a deeper pass later today or tomorrow.

hvanz

Great work @stojanovic00! 🚀

specs/starknet/block-streaming/part_stream.qnt

code/crates/test/mbt/src/deserializers.rs

code/crates/test/mbt/src/tests/streaming.rs

code/crates/test/mbt/src/tests/streaming/runner.rs

code/crates/starknet/host/src/streaming.rs

code/crates/test/mbt/src/tests/streaming/runner.rs

hvanz · 2025-02-04T14:46:50Z

@romac Now I realize that the Starknet related specs were moved to its own directory. Should these new MBT tests be also moved to its own directory, so it will be easier to move then later to a separate repo?

* adde spec to impl type converters * extract dummy data generators to utils * delete unnecessary comments * rename test

code/crates/starknet/host/src/streaming.rs

romac · 2025-02-04T21:07:21Z

Yes, let's move that spec under the appropriate folder under specs/

* Move code, manage dependencies * Update CI/CD MBT workflow to run starknet tests

code/crates/starknet/test/mbt/src/tests/streaming.rs

* Excluded MBT tests from maelstrom starknet integration testing

hvanz

I see that now all CI tests are passing and the MBT tests was moved under the starknet crate. Thanks!

.github/workflows/coverage.yml

.github/workflows/mbt.yml

code/Cargo.toml

code/crates/starknet/host/src/streaming.rs

romac

Amazing work! Pre-approving with a few nitpicks. Looks great otherwise!

code/crates/starknet/host/src/streaming.rs

stojanovic00 · 2025-02-10T17:22:01Z

I appreciate the thorough reviews @hvanz and @romac ! I hope I have addressed all the comments.

hvanz added work in progress Work in progress mbt Model-Based Testing labels Jan 29, 2025

hvanz assigned stojanovic00 Jan 29, 2025

stojanovic00 added 2 commits January 29, 2025 14:45

quint spec: added incommingMessage state var

5870245

code: added incoming_message to the itf-parser

594073d

romac added the spec Related to specifications label Jan 30, 2025

stojanovic00 added 2 commits January 31, 2025 13:12

runner state_invariant check

7f5b007

* supplemented missing proto files to test-mempool * added Buffer parsing * all invariant checks

runner step

ff84bc5

stojanovic00 and others added 3 commits February 3, 2025 12:30

code refactor

c8c94cf

deleted unnecessary comments

c88cbf0

Merge branch 'main' into part-streaming-mbt

44b82a7

stojanovic00 marked this pull request as ready for review February 3, 2025 13:47

stojanovic00 requested review from ancazamfir, romac, cason and josef-widder as code owners February 3, 2025 13:47

hvanz self-requested a review February 3, 2025 14:03

romac reviewed Feb 3, 2025

View reviewed changes

code/crates/engine/src/util/streaming.rs Outdated Show resolved Hide resolved

romac reviewed Feb 3, 2025

View reviewed changes

code/crates/starknet/host/src/streaming.rs Outdated Show resolved Hide resolved

romac reviewed Feb 3, 2025

View reviewed changes

code/crates/starknet/host/src/streaming.rs Outdated Show resolved Hide resolved

romac reviewed Feb 3, 2025

View reviewed changes

code/crates/test/mempool/proto/google/protobuf/any.proto Show resolved Hide resolved

romac reviewed Feb 3, 2025

View reviewed changes

romac added code Code/implementation related and removed work in progress Work in progress labels Feb 3, 2025

use derive(Debug) instead of derive_where(Debug)

2dc9e42

hvanz reviewed Feb 4, 2025

View reviewed changes

itf runner: initialize actual state using expected state

096457e

* adde spec to impl type converters * extract dummy data generators to utils * delete unnecessary comments * rename test

stojanovic00 commented Feb 4, 2025

View reviewed changes

code/crates/starknet/host/src/streaming.rs Show resolved Hide resolved

romac changed the title ~~feat(spec/test): part streaming mbt - itf-trace parsing~~ feat(spec/test): Model-based tests for part streaming Feb 4, 2025

stojanovic00 added 4 commits February 5, 2025 09:38

runner: updated state invariant check

fa23c02

testing with random traces

3e911ca

runner: updated state invariant

9ead704

Move starkent MBT to separate dir

1ba6412

* Move code, manage dependencies * Update CI/CD MBT workflow to run starknet tests

stojanovic00 commented Feb 6, 2025

View reviewed changes

code/crates/starknet/test/mbt/src/tests/streaming.rs Outdated Show resolved Hide resolved

stojanovic00 and others added 7 commits February 10, 2025 10:48

Separated starknet utils, updated workflow

8692256

Fixed maelstrom command

ab2da9e

workflow run command fix

3aeee08

Fixed CI/CD, removed questions from code

ae99e5a

* Excluded MBT tests from maelstrom starknet integration testing

Nextest multiline fix

e070ff4

Merge branch 'informalsystems:main' into part-streaming-mbt

c8ae7ae

Adapted tests to latest P2P protos

130cf66

hvanz approved these changes Feb 10, 2025

View reviewed changes