swh:1:snp:a009335c9ad61a15b4ffe398f445dd601942b68c
Tip revision: c954ae072cb4f5771be44af344daf96e8a2c578f authored by Antoine Séré on 25 April 2022, 14:53:39 UTC
Hakyber jasmin eclib
Hakyber jasmin eclib
Tip revision: c954ae0
StdRing.ec
(* -------------------------------------------------------------------- *)
require import Bool Int Real.
require (*--*) Ring.
(* -------------------------------------------------------------------- *)
instance ring with int
op rzero = CoreInt.zero
op rone = CoreInt.one
op add = CoreInt.add
op opp = CoreInt.opp
op mul = CoreInt.mul
op expr = Ring.IntID.exp
proof oner_neq0 by smt()
proof addr0 by smt()
proof addrA by smt()
proof addrC by smt()
proof addrN by smt()
proof mulr1 by smt()
proof mulrA by smt()
proof mulrC by smt()
proof mulrDl by smt()
proof expr0 by smt(Ring.IntID.expr0)
proof exprS by smt(Ring.IntID.exprS).
op bid (b:bool) = b.
instance bring with bool
op rzero = false
op rone = true
op add = Bool.( ^^ )
op mul = (/\)
op opp = bid
proof oner_neq0 by smt()
proof addr0 by smt()
proof addrA by smt()
proof addrC by smt()
proof addrK by smt()
proof mulr1 by smt()
proof mulrA by smt()
proof mulrC by smt()
proof mulrDl by smt()
proof mulrK by smt()
proof oppr_id by smt().