ZK-SecreC Documentation

2024.09

Module Date

Function date

pub fn date [ $S, @D, N : Nat ] ( year : uint[N] $S @D, month : uint[N] $S @D, day : uint[N] $S @D ) -> Date[$S, @D, N] $pre @public

A Date object with given year, month and day.

Function date_assert_eq

pub fn date_assert_eq [ @D, N : Nat ] ( x : Date[$post, @D, N] $pre @public, y : Date[$post, @D, N] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that given two Date objects have equal values.

Function date_assert_ge

pub fn date_assert_ge [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first given date is later than or equal to the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_assert_gt

pub fn date_assert_gt [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first given date is later than the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_assert_le

pub fn date_assert_le [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first given date is earlier than or equal to the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_assert_lt

pub fn date_assert_lt [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first given date is earlier than the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_eq

pub fn date_eq [ $S, @D, N : Nat ] ( xd : Date[$S, @D, N] $pre @public, yd : Date[$S, @D, N] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test of equality of the values of given two Date objects.

Function date_ge3

pub fn date_ge3 [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first given date is later than or equal to the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_gt3

pub fn date_gt3 [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first given date is later than the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_le3

pub fn date_le3 [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first given date is earlier than or equal to the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_lt3

pub fn date_lt3 [ N : Nat ] ( xd : Date[$post, @prover, N] $pre @public, yd : Date[$post, @prover, N] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first given date is earlier than the second one. The third argument must be a SizeAsserter object suitable for comparing Date objects. Assumes that the given Date objects encode correct dates.

Function date_sizeasserter_new

pub fn date_sizeasserter_new [ N : Nat, $S, @D ] () -> SizeAsserter[N, $S, @D] $pre @public
where
  Field[N]

A new SizeAsserter object suitable for comparing Date objects.

Function date_to_post

pub fn date_to_post [ @D, N : Nat ] ( d : Date[$pre, @D, N] $pre @public ) -> Date[$post, @D, N] $pre @public
where
  Field[N]

Conversion of the given Date object in the stage $pre to the stage $post.

Function date_to_pre

pub fn date_to_pre [ @D, N : Nat ] ( d : Date[$post, @D, N] $pre @public ) -> Date[$pre, @D, N] $pre @public
where
  Field[N]

Conversion of the given Date object in the stage $post to the stage $pre.

Function date_to_prover

pub fn date_to_prover [ $S, @D, N : Nat ] ( d : Date[$S, @D, N] $pre @public ) -> Date[$S, @prover, N] $pre @public

Conversion of the given Date object to the domain @prover.

Function date_to_string

pub fn date_to_string [ @D, N : Nat ] ( date : Date[$pre, @D, N] $pre @public ) -> string $pre @D

The string representation of the given Date object (for debugging). In general, the result is not ISO-8601 since zeros are not added in front of one-digit months and dates.

Function is_full_date

pub fn is_full_date [ $S, @D, N : Nat ] ( str : String[$S, @D, N] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the given String object encodes a full date in the ISO 8601 format.

Function parse_full_date

pub fn parse_full_date [ $S, @D, N : Nat ] ( full_date : String[$S, @D, N] $pre @public ) -> Date[$S, @D, N] $pre @public

The Date object encoding the date in the given String object. Assumes that the given String object encodes a correct full date in the ISO 8601 format.