Skip to content

Add Flux specifications to path/bstr/hash/time - #438

Merged
tautschnig merged 7 commits into
model-checking:mainfrom
flux-rs:verify-time-rs
Sep 9, 2025
Merged

Add Flux specifications to path/bstr/hash/time#438
tautschnig merged 7 commits into
model-checking:mainfrom
flux-rs:verify-time-rs

Conversation

@nilehmann

@nilehmannnilehmann commented Aug 1, 2025•
edited
Loading

Copy link
Copy Markdown

This PR adds flux specifications for checking the following modules in core

  • pat
  • bstr
  • hash
  • time

In particular, it verifies that Nanoseconds is correctly used with values within the range.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@nilehmann
nilehmann requested a review from a team as a code ownerAugust 1, 2025 00:51
tautschnig
tautschnig reviewed Aug 1, 2025
View reviewed changes

@tautschnigtautschnig left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given I'm not intimately familiar with Flux some of the annotations introduced in this PR are not entirely clear to me, see detailed comments. Please include some comments. Thank you!

Comment threadlibrary/core/src/ascii/ascii_char.rs
Comment threadlibrary/core/src/num/niche_types.rs Outdated
Comment threadlibrary/core/src/pat.rs
tautschnig
tautschnig approved these changes Aug 1, 2025
View reviewed changes
Comment threadlibrary/core/src/ascii/ascii_char.rs
@nilehmann
nilehmannforce-pushed the verify-time-rs branch 3 times, most recently from a6a7882 to d3ba4ebCompareAugust 6, 2025 19:41
carolynzech
carolynzech approved these changes Aug 13, 2025
View reviewed changes

@carolynzechcarolynzech left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

Comment threadlibrary/core/src/pat.rs
auto-merge was automatically disabled August 22, 2025 16:16

Head branch was pushed to by a user without write access

@nilehmannnilehmann removed their assignment Sep 9, 2025
@nilehmann

nilehmann commented Sep 9, 2025

Copy link
Copy Markdown
Author

@tautschnig, sorry for the delay, but Flux is green again! After the toolchain update, we had to add a couple of extra specs included in 0375ccd

@tautschnig
tautschnig added this pull request to the merge queueSep 9, 2025
Merged via the queue into model-checking:main with commit 398ff24Sep 9, 2025
26 checks passed
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnigtautschnigtautschnig approved these changes
+2 more reviewers
@ranjitjhalaranjitjhalaranjitjhala left review comments
@carolynzechcarolynzechcarolynzech approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

@thanhnguyen-awsthanhnguyen-aws

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@nilehmann@tautschnig@ranjitjhala@carolynzech@thanhnguyen-aws