diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-30 19:13:27 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | 496271f86e9dc6df1b23a189d6b8fd2a82db33aa (patch) | |
| tree | 1b531bac09c49efb594642ea85d398f7893f8494 /src/PushButtonSynthesis/SmallExamples.v | |
| parent | cd1d339aa57c09abc716ef30a5a153ac5aadb563 (diff) | |
Add autogenerated docstrings to synthesized code
We now stringify the correctness conditions to generate docstrings for
the synthesized code.
Closes #512
Time commitment: about 6 hours
Diffstat (limited to 'src/PushButtonSynthesis/SmallExamples.v')
| -rw-r--r-- | src/PushButtonSynthesis/SmallExamples.v | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v index 09f361356..daa50c9e9 100644 --- a/src/PushButtonSynthesis/SmallExamples.v +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -43,53 +43,59 @@ Compute Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_mulx_u64" [] + true "fiat_" "fiat_mulx_u64" true None [64; 128] ltac:(let r := Reify (Arithmetic.mulx 64) in exact r) + (fun _ _ => []) (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u64" [] + true "fiat_" "fiat_addcarryx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u51" [] + true "fiat_" "fiat_addcarryx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u64" [] + true "fiat_" "fiat_subborrowx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u51" [] + true "fiat_" "fiat_subborrowx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_cmovznz64" [] + true "fiat_" "fiat_cmovznz64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.cmovznz 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1])%zrange). |