Skip to content

Commit

Permalink
Make test_comp_bisim complete in slightly less time
Browse files Browse the repository at this point in the history
Locally, this shaves off about 10 seconds from the overall verification time,
and it should make this test case finish more reliably within the CI's time
limits.
  • Loading branch information
RyanGlScott committed Feb 1, 2024
1 parent 6b1740b commit 1324ec2
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions intTests/test_comp_bisim/cryptol/spec.cry
Original file line number Diff line number Diff line change
Expand Up @@ -6,19 +6,19 @@ type input = feedback_input 16
type output = feedback_output 16

// add10 spec
type add10_state = feedback_state 16 8
type add10_state = feedback_state 16 4
add10_spec : (add10_state, input) -> (add10_state, output)
add10_spec = feedback_spec`{n=10} f
where f x = x + 10

// pow4 spec
type pow4_state = feedback_state 16 8
type pow4_state = feedback_state 16 3
pow4_spec : (pow4_state, input) -> (pow4_state, output)
pow4_spec = feedback_spec`{n=2} f
where f x = x ^^ 4

// comp spec
type comp_spec_state = feedback_state 16 8
type comp_spec_state = feedback_state 16 4
comp_spec : (comp_spec_state, input) -> (comp_spec_state, output)
comp_spec = feedback_spec `{n=13} f
where f x = (x ^^ 4) + 10

0 comments on commit 1324ec2

Please sign in to comment.